| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This commit adds methods to the string rewriter to transform a string
into a normalized string with the same length (but not the same content
necessarily). One of the use cases is normalizing the string before the
start index in an indexof operation. For example:
```
str.indexof(str.++("ABCD", x), y, 3) --->
str.indexof(str.++("AAAD", x), y, 3)
```
In addition to the helper methods, this commit adds the indexof rewrite
above.
|
|
This commit implements a workaround for computing unsat cores while
doing incremental solving to address #1349. Currently, our resolution
proofs do not handle clauses with a lower-than-assertion-level correctly
because the resolution proofs for them get removed when popping the
context but the SAT solver keeps using them. The workaround changes the
behavior of the SAT solver to add clauses always at the current level if
incremental solving and unsat cores are enabled. This makes sure that
all learned clauses are removed when we pop below the level that they
were learned at. This may degrade performance because the SAT solver has
to relearn clauses.
|
|
|
|
Currently, we may end up enabling the unconstrainedSimp pass when proofs
are enabled because the check that this pass is disabled happens before
a check for automatically enabling it. This lead to issues when running
for example on regress0/aufbv/bug00.smt with --check-proofs. This commit
moves the code for automatically enabling the pass to only be run if
proofs and unsat cores are disabled. Note: This commit is mostly a
simple code move but formatting in setDefaults was a bit off, so there
are a lot of formatting changes.
|
|
|
|
|
|
Commit 106e764a04e4099cc36d13de9cec47cbf717b6cc missed one test case.
This commit disables that test case for the competition build.
|
|
This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.
|
|
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).
|
|
|
|
If the boost program_options library is missing, CryptoMiniSat5 only
builds a cryptominisat5_simple binary and omits the cryptominisat5,
which has more command-line options. We do not use the binary anyway, so
this commit changes the cryptominisat.m4 script to look for the
cryptominisat5_simple binary, which is always generated.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 the SMT-COMP runscript, we are currently discarding output on stdout
that is not "sat" or "unsat" when using `trywith` (this is not the case
with `finishwith`). Due to this, our tests might miss cases where CVC4
fails and prints an error on stdout when using `trywith`. This commit
changes the script to print output other than "sat" or "unsat" to
stderr.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In `addClause_()`, we were checking the condition `ca[confl].size() ==
1` regardless if proofs were enabled or not, even though both branches
of the if statement only do something when proofs are enabled. This lead
to issue #1978 occurring even when not generating proofs. Note: This
commit is *not* a fix for #1978 but it makes sure that the issue does
not occur when not generating proofs/unsat cores.
|
|
|
|
|
|
|
|
|
|
|
