| Age | Commit message (Collapse) | Author |
|---|
|
* Bugfix: LFSC clause equality
My implementation of clause equality had an undocumented assumption that
the clauses didn't have any duplicate literals. Now that assumption is
gone, and the tests suite has been expanded.
* Added an empty clause test
* Typo fix: Yoni
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Yoni's comments
* Remove a duplicate clause_eq test.
* Add an ordering clause_eq test.
* Improve the documentation of clause_eq.
|
|
* 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
|
|
* DRAT signature
Added the DRAT signature to CVC4.
We'll need this in order to compare three BV proof pipelines:
1. DRAT -> Resolution -> Check
2. DRAT -> LRAT -> Check
3. DRAT -> Check (this one!)
Tested the signature using the attached test file. i.e. running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Added type annotations for tests
* Respond to Yoni's review
* Apply Yoni's suggestions from code review
Documentation polish
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Whoops, missed a spot or two
|
|
* [LRAT] signature robust against duplicate literals
The LRAT signature previously had complex, surprising, and occasionally
incorrect behavior when given clauses with duplicate literals.
Now it does not. Now clauses have true set semantics, and clauses with
duplicate literals are treated identically to those without.
* Test with logically = but structurally != clauses.
|
|
* 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.
|
