| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
|
|
splitting (#2424)
|
|
|
|
|
|
|
|
|
|
This is work towards #2305.
With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.
|
|
|
|
|
|
|
|
|
|
|
|
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
|
|
|
|
|
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
|
|
|
|
|
|
|
|
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.
|
|
|
|
The issue is not triggered anymore after PR #2059 but the test case is
good to have for changes in MiniSat code.
|
|
|
|
Some quick background: CVC4 has two primary contexts: the assertion
context (which corresponds to the push/pops issued by the user) and the
decision/SAT context (which corresponds to the push/pops done by the
user and each decision made by MiniSat.
Before 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77, we had an additonal
push/pop when doing the actual solving. With these removed, it could
happen that we get a wrong result when doing incremental solving:
```
...
; check-sat call returns sat, the decision level in the SAT solver is
; non-zero at this point
(check-sat)
; Solver::addClause_() determines that we cannot add the clause to the
; SAT solver directly because the decision level is non-zero (i.e. the
; clause is treated like a theory lemma), thus it is added to the lemmas
; list.
(assert false)
; The solver stores some information about the current state, including
; the value of the "ok" flag in Solver, which indicates whether the
; current constraints are unsatisfiable. Note that "ok" is true at this
; point.
(push)
; Now, in Solver::updateLemmas(), we add clauses from the lemmas list.
; The problem is that empty clauses (which "false" is after removing "false"
; literals) and unit clauses are not added like normal clauses. Instead,
; the empty clause, essentially just results in the "ok" flag being set to
; false (unit clauses are added to the decision trail).
(check-sat)
; Here, the solver restores the information stored during
; (push), including the "ok" flag, which is now true again.
(pop)
; At this point, the solver has "forgotten" about (assert false) since
; the "ok" flag is back to true and it answers sat.
(check-sat)
```
There are multiple ways to look at the problem and to fix it:
- One could argue that an input assertion should always be added
directly to the clauses in the SAT solver, i.e. the solver should
always be at decision level 0 when we are adding input clauses. The
advantage of this is that it is relatively easy to implement,
corresponds to what the original MiniSat code does (it calls
Solver::cancelUntil(0) after solving), and is no worse than what we had
before commit 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (push/pop do a
strict superset of what resetting the decision at the current assertion
level does). The disadvantage is that we might throw away some useful work.
- One could argue that is fine that (assert false) is treated like a
theory lemma. The advantage being that it might result in more efficient
solving and the disadvantage being that it is much trickier to
implement.
Unfortunately, it is not quite clear from the code what the original
intention was but we decided to implement the first solution. This
commit exposes a method in MiniSat to reset the decisions at the current
assertion level. We call this method from SmtEngine after solving.
Resetting the decisions directly after solving while we are still in
MiniSat does not work because it causes issues with datastructures in
the SMT solver that use the decision context (e.g.
TheoryEngine::d_incomplete seems to be reset too early, resulting in us
answering sat instead of unknown).
|
|
|
|
This commit adds supprt for the `REQUIRES` directive in our regression
benchmarks. This directive can be used to enable certain benchmarks only
if CVC4 has been configured with certain features enabled.
|
|
Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
|
|
|
|
|
|
|
|
|
|
|
|
In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.
|
|
|
|
This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).
|
|
|
|
* Fix file extension
* Update Makefile
|
|
|
|
|
|
|
|
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.
|
|
|
|
|
