| Age | Commit message (Collapse) | Author |
|---|
|
Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.
Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).
|
|
Previously the binary resolution checker was:
- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.
This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).
Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
|
|
|
|
Also fixes some weird orderings in src/CMakeLists.txt
|
|
The post processor connects the two proofs in the prop engine: the refutation proof in the SAT solver and the CNF transformation proof in the CNF stream. The proof generators from theory engine in the latter are also expanded during the connection.
|
|
A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).
|
|
|
|
Tracks the refutation proof built by Minisat. See the header for extensive explanations.
This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).
|
|
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
|
|
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 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 updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.
This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
|
|
This commit fixes builds that include CryptoMiniSat after commit
8ad308b removed them. It also fixes one
of the regressions that requires unsat cores but was run when the build
was configured without them.
|
|
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).
|
|
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
|
|
This changes an initialization issue in regarding PropEngine and TheoryEngine.
In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.
The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.
|
|
Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.
|
|
|
|
|
|
|
|
|
|
Resource manager will be owned by SmtEngine in the future. This passes the resource manager cached by SmtEnginePrivate to the PropEngine created by SmtEngine instead of using the global pointer. It also makes a few preprocessing passes use the resource manager they already have access to and should use.
|
|
Towards disentangling Options / NodeManager / SmtEngine.
This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.
The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.
The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.
It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
|
|
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.
|
|
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).
|
|
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
|
|
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
|
|
This is in preparation of fixing the issue we currently have with
reset-assertions. This also removes a competition hack for QF_LRA.
|
|
This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.
|
|
This is in preparation of fixing the issue we currently have with reset-assertions.
This also removes a competition hack for QF_LRA.
|
|
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>
|
|
(#3846)
|
|
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
|
|
(#3788)
PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
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.
|
|
This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).
In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.
There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations
Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`
The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.
|
|
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`).
|
|
Fixes #971.
|
|
|
|
|
|
|
|
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
|
|
* 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)
|
|
This commit adds support for eager bit-blasting with CaDiCaL on
incremental benchmarks. Since not all CaDiCaL versions support
incremental solving, the commit adds a CMake check that checks whether
`CaDiCaL::Solver::assume()` exists.
Note: The check uses `check_cxx_source_compiles`, which is not very
elegant but I could not find a better solution (e.g.
`check_cxx_symbol_exists()` does not seem to support methods in classes
and `check_struct_has_member()` only seems to support data members).
|
|
Fixes 2887.
|
|
* SatClauseHashFunction
Added to the same file as SatLiteralHashFunction.
* clang-format
Thanks Andres!
|
|
|
|
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.
|
|
* [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
|
