Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
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).
|
|
|
|
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.
|
|
* [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
|
|
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.
|
|
|
|
Adds missing override keywords.
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
|
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
|
|
|
|
|
|
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
|
|
signature. Add regressions.
|
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
|
|
|
|
|
|
comment in LFSC
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Nodes---useful for debugging.
* language-dependent Node::toString()
* some minor proof-related cleanup
|
|
- can now output LFSC checkable resolution proofs
- added configuration option --enable-proof
- added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.
|