search

FormalSAT / trestle

Apache License 2.0
17 stars 2 forks source link

Persistent Partial Assignments #8

Open Vtec234 opened 8 months ago

Vtec234 commented 8 months ago

Adds a tautology checking and unit propagation module based on PPAs. The PPA module is sorry-free and can be reviewed, but depends on some sorried lemmas in AuxDefs/ToStd. I did not try cleaning up these modules.

JamesGallicchio commented 6 months ago

cayden said "everything has moved" (see #16 )

Vtec234 commented 6 months ago

Does #16 completely subsume this one? It looks like it has some #exits that 'comment out' some of the lemmas here; is the plan is to fix them later? (I am using most of them in my CRAT checker, it would be nice to move it over to LeanSAT dev.)

JamesGallicchio commented 6 months ago

Oop, I am unsure. Re-opening and will do some diffing tomorrow.