| Age | Commit message (Collapse) | Author |
|---|
|
* Extended Resolution Signature
While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form
new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:
1. Introducing a **fresh** variable, defined in the form above
2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
clauses in the form of two clauses, and a cnf with $$ n $$ clauses
3. An axiom for unrolling the proof of the cnf into proofs of the
original clauses.
* Addressing Yoni's comments
1. Added a new (trivial) test
2. Improved a bunch of documentation
* Update proofs/signatures/er.plf
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Removed references to RATs from the signature
There are still a few references in the header comment.
* Aside on continuations
* Scrap the elision annotations
|
|
* LRAT signature
Added an LRAT signature. It is almost entirely side-conditions, but it
works.
There is also a collection of tests for it. You can run them by invoking
```
lfscc smt.plf sat.plf lrat.plf lrat_test.plf
```
* Update proofs/signatures/lrat.plf per Yoni's suggestion.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Yoni's comments.
* Removed unused varaibles
Some tests declared `var`s which were unused.
Now they don't.
|
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
