| Age | Commit message (Collapse) | Author |
|---|
|
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.
The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.
Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
|
|
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
|
|
This includes 4 changes:
Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.
This PR is also contingent on the performance tests for proof-new on SMT-LIB.
|
|
This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.
|
|
Before terms in assertions that are not sent to the SAT solver could be collected by the old proof code as atoms and thus expected to have a corresponding SAT variable. This commit fixes this by making the atom collection from assertions more conservative.
|
|
Fixes #2846. One of the challenges of the Java bindings is that the
garbage collector can delete unused objects at any time in any order.
This is an issue with CVC4's API because we require all `Expr`s to be
deleted before the corresponding `ExprManager`. In the past, we were
using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of
`ExprManager`. The problem is that we can have multiple instances of the
wrapper that internally all refer to the same `ExprManager`. This commit
implements a different approach where the Java wrappers hold an explicit
reference to the `ExprManager`. The commit also removes some unused or
unimportant API bits from the bindings.
|
|
|
|
Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.
The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.
The regression test is an extension of the example in #4151 and covers
both issues.
|
|
Done by:
Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.
|
|
|
|
I'll remove the error later
|
|
Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
Switches arith_proof.cpp from th_lra to th_lira.
Changes:
Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.
|
|
|
|
|
|
Also, missed an armType use.
|
|
* Add function for tightening literals
The function tightens a literal if it can be tightened, and prints a
proof of the result.
* Include a #include
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
|
|
|
`TheoryProofEngine` now uses the `expectedType` optional argument.
* When printing terms, it sets this for theories that it dispatches too
* It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
* It is mindful of `expectedType` when using the let map.
I also moved to hpp function implementations into the cpp.
|
|
* expectedType in proof-printing code
To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.
This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.
Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.
* TypeNode, Don't mix default args & virtual
* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
be dynamically overriden during a dynamic dispatch.
* Since we don't want them to be overidable anyway, we use two
functions: one that is non-virtual and has a default, the other that
is virtual but has no default. The former just calls the latter.
* clang-format after signature changes
|
|
* Bugfix: convert ifte arms to formulas for printing
We have two kinds of ITEs in our LFSC proofs:
* ite: for sort-typed expressions
* ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.
Fixed now.
* Test the lifting of ITEs from arithmetic.
This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.
It used to fail, but now passes.
* clang-format
* Typos.
* Add test to CMake
* Set --check-proofs in test
* Address Yoni
* Expand printsAsBool documentation
* Assert ITE typing soundness
* Assert a subtype relation for ITEs, not equality
* Update src/proof/arith_proof.h
Thanks Yoni!
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
* [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
|
