| Age | Commit message (Collapse) | Author |
|---|
|
Previosuly, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.
|
|
|
|
There was a problem in which if a DRAT proof failed to meet the
specifified requirements in the final addition of the empty clause.
Specifically, the empty clause would not be an AT, and then resolution
search would trigger and fail because the empty clause can't resolve
with stuff. Now we just return false, causing operational DRAT checking
to start.
|
|
Also, removed unneeded (and sometimes violated) assertions.
|
|
Previously, tautologies caused a failure if they were encountered during
unit propegation.
Important Fact: Tautologies cannot imply anything during unit
propegation, because they can never reduce to unit clauses modulo a
partial assignmnet.
In LRAT proofs the checker is instructed to look at clauses in a certain
order, and each of those clauses must be unit (or bottom) for the proof
to check.
In DRAT, the checker needs to look for the unit clauses on its own.
The natural way to combine functionality is to write a function which
checks whether some clause is unit. (e.g. returns true/false). We have
such a function, `check_unit_and_maybe_mark` (which also does some other
stuff, but we'll just consider the checking here).
The question then arises, what should the function do if the clause is
TAUT? From the LRAT perspective, it's fine if the function fails, but
from the DRAT perspective, failing would be bad, because the correct
behavior would be to just return "not a unit clause", and go check other
clauses.
We were failing, and now we're returning "not a unit"
|
|
std::ostream::clear actually modifiers the error bits...
|
|
* Required some changes to our C++ API for drat2er.
|
|
* Using the `Maybe` class for the return of `detectTrivialTautology`.
* Removing a spurious `= 0`.
|
|
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
|
|
* ErProof class with LFSC output
* Created a TraceCheckProof class
* parsable from text
* Created an ErProof class
* constructible from a TraceCheckProof
* writable as LFSC
* A bunch of unit tests
* Reponded to Mathias's first set of comments.
Credits to Mathias for many of the fixes!
* Responed to Andres's first set, fixed tests
I accidentally deleted a "!" last time, causing stuff to fail.
* Use Configuration::isAssertionBuild
* Clarified comment
* Responded to Andres's 2nd review
* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.
|
|
This commit changes CVC4 to use a string stream instead of a temporary
files for proof checking. Note: This change requires a version of LFSC
that supports checking streams (see
https://github.com/CVC4/LFSC/pull/14).
Tested: `make check` passed, changing `holds` to `xholds` in the proof
produced by proof_manager.cpp makes the proofs fail.
|
|
The option `DerivePointerAlignment` tries to automatically determine the
pointer alignment used by the input. In our case, we would eventually
like the code base to be consistent throughtout, so this commit disables
that option.
|
|
|
|
|
|
|
|
CVC4 was not deleting temporary proof files when crashing or being
terminated externally. This commit uses an early `unlink()` to remove
the files as soon as CVC4 terminates.
|
|
|
|
|
|
|
|
`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
|
|
|
|
This required fixing the OpTerm handling for mkTerm functions in the API.
|
|
Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.
|
|
* Extended DRAT signature to operational DRAT
The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.
The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).
You can run the new AND old DRAT tests by running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Apply suggestions from code review (Yoni)
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
|
|
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.
|
|
|
|
|
|
|
|
`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.
|
|
|
|
|
|
* [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.
|
