| Age | Commit message (Collapse) | Author |
|---|
|
* [proof] Eliminate the side condition in er.plf
By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.
* [proof] Changed er_proof.cpp in line with signature
The new signature requires slightly different proof printing.
* [proof] clang-format er_proof.cpp
* Fix tests
* [proof] Actually delete the SC
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof
* Gate the lfsc invocation on the build system
* Properly gate the lfsc check on the build system
* gate the plf_signatures forward def on the build system
|
|
|
|
This commit enables compiler warnings for implicit fallthroughs in
switch statements that are not explicitly marked as such. The commit
introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate
that a fallthrough is intentional. The commit fixes existing warnings
and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't
be triggered easily because we rewrite `abs` to an `ite` while expanding
definitions).
To have the new macro also available in the parser, the commit changes
`src/base/check.h` to be visible to the parser (it includes
`cvc4_private_library.h` now instead of `cvc4_private.h`).
|
|
|
|
GCC < 5 does not support the move constructor of `std::fstream` (see
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details). This
commit wraps the `std::fstream` in an `std::unique_ptr` to work around
that issue.
|
|
* improved proof production statistics
This commit creates new statistics which will help us understand what is
so expensive about proof production.
There are already statistics for:
* Net time spent building/printing the LFSC proof.
* Size of the LFSC proof.
This commit adds statistics for:
* The time cost of DRAT optimization:
* net time
* tool time (drat-trim)
* clause matching time (matching core clauses with input clauses)
* Non-trivial because drat-trim can (and does) dedup and reorder
literals
* The advantage of DRAT optimization (proof/formula size before/after)
* The time cost of DRAT translation [to LRAT or ER] (net time, tool time)
* The time cost of skeleton traversal
* The time cost of printing declatations
* The time cost of printing CNF proofs
* The time cost of printing theory lemmas
* The time cost of printing final UNSAT proof.
There is a method, toStream, which is responsible for much of proof
production. The whole method was timed, but subsections were not. The
timings above consider subsections of it.
I also wanted to better understand the cost of DRAT optimization and
translation.
* [BV Proof] Optimize DRAT optimization
tldr: I made a bad data-structure/algorithm choice when implementing
part of DRAT/CNF-optimization, which consumed **a lot** of time on some
bechmarks. This commit fixes that choice.
Long Version:
Set-Keyed Maps Considered Harmful
=================================
Algorithmic Problem
-------------------
The DRAT optimization process spits out a unsatifiable core of the CNF.
The clauses in the core are all from the original formula, but their
literals may have been reordered and deduplicated. We must match the
old clauses with new ones, so we know which old clauses are in the core.
Old (BAD) Solution
------------------
Before I didn't really think about this process very much. I built a
solution in which clauses were canonically represented by hash sets of
literals, and made a hash map from canonical clauses to clause indices
into the original CNF.
Problem With Old Solution
-------------------------
In hindsight this was a bad idea. First, it required a new hash set to
be heap-allocated for every clause in the CNF. Second, the map lookups
required set-hashes (reasonable -- linear time, once) and hash-set
equality (not reasonable -- quadratic time, multiple times) on every
lookup.
New Solution
------------
The ideal solution is probably to have the map from clauses to clause
ids be something like a trie. STL doesn't have a trie, but representing
clauses as sorted, deduped vectors of literal in a tree based on
lexicographical comparison is pretty closed to this. On randomly chosen
examples it seems to be a huge improvement over the old
map-keyed-by-sets solution, and I'm in the process of running a full set
of bechmarks.
Also, we store pointers to the clauses already stored elsewhere in the
proof, instead of allocating new memory for them.
Future Work
-----------
It may also be reasonable to do a hash map of sorted, deduped, vector
clauses. I haven't tried this, yet (there's a TODO in the code).
* Update src/proof/clausal_bitvector_proof.h
Thanks andres!
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Respond to Andres' Review: better use of CodeTimer
* Removed commented code (Andres)
|
|
Previously, 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.
|
|
|
|
This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.
These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically, proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:
## DRAT Optimization
The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.
## CNF Representation
The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.
## Small Fixes to Signatures
When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.
|
|
Fixes #2989. SWIG 3 seems to have an issue properly resolving
`T::const_iterator::value_type` if that type itself is a `typedef`.
This is for example the case in the `UnsatCore` class, which `typedef`s
`const_iterator` to `std::vector<Expr>::const_iterator`. As a
workaround, this commit changes the `JavaIteratorAdapter` class to take
two template parameters, one of which is the `value_type`. The commit
also adds a compile-time assertion that `T::const_iterator::value_type`
can be converted to `value_type` to avoid nasty surprises. A nice
side-effect of this solution is that explicit `typemap`s are not
necessary anymore, so they are removed. Additionally, the commit adds a
`toString()` method for the Java API of `UnsatCore` and adds examples
that show and test the iteration over the unsat core and the statistics.
Iterating over `Statistics` now returns instances of `Statistic` instead
of `Object[]`, which is a bit cleaner and requires less glue code.
|
|
Fixes 2887.
|
|
|
|
|
|
* 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.
|
|
This commit adds a statistic that records the total size of all proofs
generated by an instance of `SmtEngine`. The commit also moves
`SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know
the complete type of `d_stats` (and the separate file for that method
didn't seem that useful). Additionally, it changes
`smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime`
that only measures the time spent in LFSC and adds a statistic
`proof::ProofManager::proofProductionTime` that measures the proof
production time separately (also works with `get-proof`/`--dump-proof`).
|
|
* 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.
|
|
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.
|
|
* [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
|
|
* 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.
|
|
* LFSC drat output
* Addressed Mathias' review
Addressing Mathias' review with the following changes:
* Added a few blank lines
* Added a unit test for LRAT output as LFSC
|
|
* Copied old DRAT data-structure files.
Next step: clean up the code, and adapt them to our current usage plans.
* Polished the DRAT class.
Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.
More explicit about whether methods handle binary or text.
Better constructor patterns
* Added implementation of textual DRAT output
* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction
* use emplace_back
* Addressing Yoni's first review
* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation
* Removed aside about std::string
* Addressed Mathias' comments
Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.
* Unit tests for binary DRAT parsing
* Added text output test
* s/white/black/ derp
|
|
* [LRAT] A C++ data structure for LRAT.
Added a data structure for storing (abstract) LRAT proofs.
The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.
Subsequent PRs will add:
* LFSC representation of LRAT
* Bitvector Proofs based on LRAT
* Enabled tests for those proofs
* Documenting LRAT constructors
* Apply suggestions from code review
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Andres' review
Consisting of
* Naming nits
* Closed fds
* Better implementation of disjoint union for LratInstruction
* DRAT -> LRAT conversion is no longer an LratProof constructor
* include reorder
* Update src/proof/lrat/lrat_proof.h
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
* ANonymous namespaces and name resolution?
* Remove inlines, fix i negation
Thanks Andres!
* Use `std::abs`
Credit to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Remove uneeded public
|
|
* [LRA proof] Recording & Printing LRA Proofs
Now we use the ArithProofRecorder to record and later print arithmetic
proofs.
If an LRA lemma can be proven by a single farkas proof, then that is
done. Otherwise, we `trust` the lemma.
I haven't **really** enabled LRA proofs yet, so `--check-proofs` still
is a no-op for LRA.
To test, do
```
lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2)
```
where `lfsccvc4` is an alias invoking `lfscc` with all the necessary
signatures. On my machine that is:
```
alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \
/home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf"
```
* Added guards to proof recording
Also reverted some small, unintentional changes.
Also had to add printing for STRING_SUBSTR??
* Responding to Yoni's review
* SimpleFarkasProof examples
* Respond to Aina's comments
* Reorder Constraint declarations
* fix build
* Moved friend declaration in Constraint
* Trichotomy example
* Lift getNumChildren invocation in PLUS case
Credits to aina for spotting it.
* Clang-format
|
|
|
|
* [LRA Proof] Storage for LRA proofs
During LRA solving the `ConstraintDatabase` contains the reasoning
behind different constraints. Combinations of constraints are
periodically used to justify lemmas (conflict clauses, propegations, ...
?). `ConstraintDatabase` is SAT context-dependent.
ArithProofRecorder will be used to store concise representations of the
proof for each lemma raised by the (LR)A theory. The (LR)A theory will
write to it, and the ArithProof class will read from it to produce LFSC
proofs.
Right now, it's pretty simplistic -- it allows for only Farkas proofs.
In future PRs I'll:
1. add logic that stores proofs therein
2. add logic that retrieves and prints proofs
3. enable LRA proof production, checking, and testing
* Document ArithProofRecorder use-sites
* Update src/proof/arith_proof_recorder.cpp
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Yoni's review
* clang-format
* Response to Mathias' review.
|
|
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
|
|
A test for PR #2737 was failing even though the PR only added dead code.
This PR fixes the issue by fixing two use-after-free bugs:
- `ResolutionBitVectorProof` has a `Context` and a
`std::unique_ptr<BVSatProof>` member. The `BVSatProof` depends on the
`Context` and tries to access it (indirectly) in its constructor but
because the context was declared after the proof, the context was
destroyed before the proof, leading to a use-after-free in a method
called from the proof's destructor. This commit reorders the two
members.
- `TLazyBitblaster` was destroyed before the `LFSCCnfProof` in
`BitVectorProof` because `SmtEngine`'s destructor first destroyed the
theory engine and then the proof manager. This lead to a use-after-free
because `LFSCCnfProof` was using the `d_nullContext` of
`TLazyBitblaster`, which got indirectly accessed in `LFSCCnfProof`'s
destructor. This commit moves the destruction of `ProofManager` above
the destruction of the theory engine.
The issues were likely introduced by #2599. They went undetected because
our nightlies' ASAN check does not use proofs due to known memory leaks
in the proof module of CVC4.
I have tested this PR up to regression level 2 with ASAN with leak
detection disabled.
|
|
* Split BitvectorProof into a sub/superclass
The superclass contains general printing knowledge.
The subclass contains CNF or Resolution-specific knowledge.
* Renames & code moves
* Nits cleaned in prep for PR
* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof
Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.
* Unique pointers, comments, and code movement.
Adjusted the distribution of code between BVP and RBVP.
Notably, put the CNF proof in BVP because it isn't
resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
BVP's pointer to a CNF proof
RBVP's pointer to a resolution proof
BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`
* clang-format
* Undo manual copyright modification
* s/superclass/base class/
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public
* Andres's Comments
Mostly cleaning up (or trying to clean up) includes.
* Cleaned up one header cycle
However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.
* Added single _s to header gaurds
* Fix Class name in debug output
Credits to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original ordering
|
|
Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.
Also added an iterator for the proof steps, and << implementations
|
|
|
|
|
|
|
|
Currently, we have an LFSCSatProof which inherits from TSatProof and
implements printing the proof. The seperation is not clean (e.g.
clauseName is used for printing only but is in TSatProof) and the
inheritance does not add any value while making dependencies more
confusing. The plan is that TSatProof becomes a self-contained part that
the MiniSat implementations generate and ProofManager prints out. This
commit is a first step in that direction. For SAT solvers with native
capabilities for producing proofs, we would simply implement a different
LFSC printer of their proof representation without changing the SAT
solver itself. The inheritance would make this awkward to deal with.
Additionally, the commit cleans up some unused functions and adjusts the
visibility of TSatProof methods and members.
|
|
|
|
Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.
|
|
|
|
|
|
|
|
This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
|
|
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
|
|
meant. (#1585)
|
|
(#1374)
|
|
|
|
|
