| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.
|
|
|
|
|
|
This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.
|
|
`TLazyBitblaster::setProofLog()` was defined even though the method was
not virtual before PR #2808 and `TBitblaster` was implementing the same
method. After that PR, which made the method virtual, GCC complained
about a missing `override` keyword for `setProofLog()`. However, the
method should have been removed (see
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247299617)).
This commit removes the function definition.
|
|
|
|
|
|
Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.
However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.
At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.
|
|
|
|
PR #2786 introduced a pure virtual method `TBitblaster::getSatSolver()`.
`AigBitblaster` was missing the implementation of that method. This
commit adds an implementation that simply returns the underlying SAT
solver. Note: The method is currently only used for proofs and CVC4 does
not support proofs in combination with ABC. To make this explicit, the
commit also adds a check in `SmtEngine::setDefaults()` that makes sure
that we are not trying to produce proofs with `--bitblast-aig` (before
the commit, we just crashed with an assertion failure/null pointer
dereference).
|
|
This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.
|
|
|
|
* 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
|
|
|
|
When configuring CVC4 with `--static`, we change
`CMAKE_FIND_LIBRARY_SUFFIXES` to prefer static libraries (`*.a`) over
shared ones. However, instead of prepending `.a` to the list of
`CMAKE_FIND_LIBRARY_SUFFIXES`, we created a single element with `.a` and
the previous list.
Output of `message("${CMAKE_FIND_LIBRARY_SUFFIXES}")` before the change:
```
.a .tbd;.dylib;.so;.a
```
After the change:
```
.a;.tbd;.dylib;.so;.a
```
On macOS, both the static and the shared library of GMP are available
(when installed via homebrew) and before the change, CMake would pick the
shared library when compiling with `--static --no-static-binary`. This
commit fixes that issue.
|
|
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
|
|
|
|
|
|
|
|
|
|
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
|
|
* [DRAT] ClausalBitvectorProof
Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)
It fits into the `BitvectorProof` class hierarchy like this:
```
BitvectorProof
/ \
/ \
ClausalBitvectorProof ResolutionBitvectorProof
```
This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
* CnfStream
* SatSolver (specifically the BvSatSolver)
* CnfProof
* TheoryProof
* TheoryBV
* Both bitblasters
And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.
This means that references to and interactions with (R)BVP were
pervasive.
Nevertheless, an SMT developer must persist.
The change summary:
* Create a subclass of BVP, called ClausalBitvectorProof, which has
most methods stubbed out.
* Make a some modifications to BVP and ResolutionBitvectorProof as the
natural division of labor between the different classes becomes
clear.
* Go through all the components in the first list and try to figure
out which kind of BVP they should **actually** be interacting with,
and how. Make tweaks accordingly.
* Add a hook from CryptoMinisat which pipes the produced DRAT proof
into the new ClausalBitvectorProof.
* Add a debug statement to ClausalBitvectorProof which parses and
prints that DRAT proof, for testing purposes.
Test:
* `make check` to verify that we didn't break any old stuff, including
lazy BB, and eager BB when using bvminisat.
* `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
-d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
1. It crashed with "Unimplemented"
2. Right before that it prints out the (textual) DRAT proof.
* Remove 2 unneeded methods
* Missed a rename
* Typos
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments
* Reorder members of TBitblaster
|
|
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
|
|
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
|
|
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
|
|
|
|
|
|
|
|
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
|
|
* Print LFSC proofs of CNF formulas
* Unit Test for clause printing
* Added SAT input proof printing unit test
* Fixed cnf_holds reference. Proofs of CMap_holds
There were references to clauses_hold, which should have been references
to cnf_holds.
Also added a function for printing a value of type CMap_holds, and a
test for this function.
|
