| Age | Commit message (Collapse) | Author |
|---|
|
This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.
It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.
It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
|
|
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
|
|
This moves regression test that exceed the time limit of their
respective level to the appropriate level. It further updates the
guidelines in the README with information on how to properly categorize
regression tests into levels (with time limits).
Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and
is now sat (Z3 agrees).
|
|
|
|
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
|
|
We need to add to the current proof, regardless of whether we have used the factor skolem previously.
Fixes bugs found by @HanielB on SMT-LIB runs.
|
|
This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.
This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.
One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.
|
|
This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.
It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).
|
|
Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.
For example, with a 1-bit granularity, you might learn a lemma like:
((_ iand 4) x y), value = 1
actual (2, 3) = 2
bv-value = #b0001
bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
(and (and true
(= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
(= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
; BITWISE_REFINE
which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.
|
|
This PR makes it so that extended arithmetic operators are not expanded during expand definitions. Instead they are eliminated at theory preprocessing, which occurs as the last step of preprocessing.
The motivation for this is three fold:
(1) Some quantified LIA benchmarks lead to CVC4 failing to eliminate div functions from quantifier instantiation, this leads to spurious logic failures. A regression is included, which now is correctly solved.
(2) We should allow better rewriting and preprocessing for extended arithmetic functions, especially for div/mod which is important for many users of QF_NIA.
(3) More generally,Theory::expandDefinitions will be deleted. All functionalities in expandDefinitions should move to Theory::ppRewrite.
This changes impacts many benchmarks that involve non-linear and quantifiers:
Many benchmarks (as expected) give a warning during check-models since (/ n 0) cannot be evaluated. I've added -q to disable these warnings. Fully addressing this is part of an agenda to improve our support for --check-models.
Several fuzzing benchmarks involving NL+quantifiers now time out. However, several can be solved by --sygus-inst, which is now the preferred instantiation strategy for NL+quantifiers.
2 other non-linear regressions time out, which are disabled in this PR.
one sygus-inference benchmark (regress1/sygus/issue3498.smt2), now correctly times out (previously it did not timeout since the preprocessor was unable to apply sygus-inference and resorted to normal methods, now sygus-inference can apply but as expected times out).
Fixes #5237.
|
|
Fixes a bug in incremental with non-linear where the built model flag would still be true on the first call to check in a 2nd call to check-sat in incremental mode. This occurs when we are under the same SAT context when the model was built (likely level 0) on the subsequent check-sat call.
Fixes #5372
|
|
This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.
|
|
There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)
This PR implements (2).
The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
|
|
arithmetic (#4930)
This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
|
|
In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.
|
|
|
|
This option only marginally helped and will be difficult to support with the new proof infrastructure.
|
|
This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.
The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.
As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.
This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.
Also notice that --rewrite-divk is effectively now enabled by default always.
Fixes #4484, fixes #4486, fixes #4481.
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
Fixes #3955.
Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.
This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.
A block of code changed indentation in this commit.
|
|
Fixes #3803.
When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.
|
|
Fixes #3647.
Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.
This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.
|
|
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
|
|
Fixes two issues in regressions, fixes regress1.
|
|
|
|
|
|
transcendentals (#3577)
|
|
|
|
solver (#3525)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(#1742)
|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
NonLinearExtension (#1633)
|
|
Also adds parsing support for PI in smt2 with syntax "real.pi".
|
|
|
|
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
|
