| Age | Commit message (Collapse) | Author |
|---|
|
Fixes followup issues from #6604.
|
|
Fixes #6604.
Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.
|
|
Fixes #6545.
An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
|
|
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 does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
|
|
Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.
|
|
Fixes #6567.
|
|
We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
|
|
This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs.
The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first.
```
status total solved sat unsat best timeout memout error uniq disagr time_cpu memory
benchmark config
AUFDTLIRA newUnsatCoresAssumps-safe/ ee 35 4 0 4 4 7 0 23 2 0 954.0 1267.5
newUnsatCoresProofs ok 35 31 0 31 25 4 0 0 0 0 894.1 1692.9
oldUnsatCores ok 35 32 0 32 30 3 0 0 1 0 799.2 1428.5
AUFLIA newUnsatCoresAssumps-safe/ ok 11 7 0 7 7 4 0 0 7 0 532.2 7604.4
newUnsatCoresProofs ok 11 4 0 4 1 6 0 0 0 0 829.0 12459.8
oldUnsatCores ok 11 4 0 4 3 6 0 0 0 0 818.2 7764.4
AUFLIRA newUnsatCoresAssumps-safe/ to 2 0 0 0 0 2 0 0 0 0 241.6 125.6
newUnsatCoresProofs ok 2 2 0 2 1 0 0 0 0 0 54.2 45.5
oldUnsatCores ok 2 2 0 2 2 0 0 0 0 0 49.4 79.7
AUFNIRA newUnsatCoresAssumps-safe/ ok 10 5 0 5 5 5 0 0 2 0 748.4 1630.0
newUnsatCoresProofs ok 10 4 0 4 0 6 0 0 0 0 850.7 2978.8
oldUnsatCores ok 10 8 0 8 5 2 0 0 1 0 502.7 2048.5
BV newUnsatCoresAssumps-safe/ ok 7 1 1 0 1 6 0 0 1 0 734.2 2065.0
newUnsatCoresProofs ok 7 6 3 3 4 1 0 0 0 0 246.7 1023.9
oldUnsatCores ok 7 6 3 3 3 1 0 0 0 0 248.6 992.0
LIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.9 47.7
newUnsatCoresProofs ok 1 1 0 1 1 0 0 0 0 0 0.3 6.5
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 0.3 5.3
LRA newUnsatCoresAssumps-safe/ ok 5 3 0 3 3 2 0 0 3 0 450.7 260.4
newUnsatCoresProofs ok 5 2 0 2 0 3 0 0 0 0 537.8 424.5
oldUnsatCores ok 5 2 0 2 2 3 0 0 0 0 533.8 298.5
NIA newUnsatCoresAssumps-safe/ to 1 0 0 0 0 1 0 0 0 0 120.8 22.0
newUnsatCoresProofs ok 1 1 0 1 0 0 0 0 0 0 46.3 48.0
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 43.3 40.3
QF_ABV newUnsatCoresAssumps-safe/ ok 105 70 59 11 70 35 0 0 63 0 8195.5 19363.3
newUnsatCoresProofs ok 105 34 24 10 17 71 0 0 5 0 11099.5 35756.7
oldUnsatCores ok 105 37 23 14 18 69 0 0 1 0 11198.0 26878.1
QF_ANIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1631.8
newUnsatCoresProofs ok 4 4 3 1 2 0 0 0 0 0 175.1 1513.6
oldUnsatCores ok 4 4 3 1 3 0 0 0 0 0 173.8 1495.1
QF_AUFLIA newUnsatCoresAssumps-safe/ ok 35 6 1 5 6 29 0 0 3 0 3718.4 524.1
newUnsatCoresProofs ok 35 24 4 20 1 11 0 0 0 0 2357.2 36556.0
oldUnsatCores ok 35 32 5 27 29 3 0 0 5 0 1857.6 10067.7
QF_AUFNIA newUnsatCoresAssumps-safe/ ok 3 1 0 1 1 2 0 0 0 0 324.7 543.6
newUnsatCoresProofs ok 3 2 2 0 1 1 0 0 1 0 223.1 509.0
oldUnsatCores ok 3 2 1 1 1 1 0 0 0 0 268.5 484.3
QF_AX newUnsatCoresAssumps-safe/ ok 12 1 0 1 1 11 0 0 0 0 1379.2 391.3
newUnsatCoresProofs ok 12 10 0 10 0 2 0 0 0 0 528.7 7433.9
oldUnsatCores ok 12 12 0 12 11 0 0 0 1 0 343.0 2855.2
QF_BV newUnsatCoresAssumps-safe/ ok 96 56 30 26 49 39 2 0 35 0 9248.2 98058.7
newUnsatCoresProofs ok 96 37 26 11 23 52 7 0 7 0 9781.9 135924.7
oldUnsatCores ok 96 50 29 21 24 43 3 0 7 0 9155.6 107216.0
QF_IDL newUnsatCoresAssumps-safe/ ok 109 51 39 12 43 58 0 0 33 0 10427.2 50846.5
newUnsatCoresProofs ok 109 33 32 1 2 76 0 0 0 0 11692.8 108963.1
oldUnsatCores ok 109 75 55 20 64 34 0 0 26 0 10088.1 53105.6
QF_LIA newUnsatCoresAssumps-safe/ ok 306 155 111 44 138 151 0 0 119 0 25346.4 50556.0
newUnsatCoresProofs ok 306 117 95 22 49 189 0 0 0 0 27092.6 122894.9
oldUnsatCores ok 306 187 110 77 152 119 0 0 34 0 24521.0 61261.1
QF_LRA newUnsatCoresAssumps-safe/ ok 72 39 20 19 38 33 0 0 31 0 7475.3 16892.2
newUnsatCoresProofs ok 72 31 16 15 2 41 0 0 0 0 7569.3 35658.7
oldUnsatCores ok 72 41 18 23 32 31 0 0 2 0 7243.2 20593.9
QF_NIA newUnsatCoresAssumps-safe/ ok 4389 2009 1862 147 2002 903 0 0 1931 0 163975.7 280779.3
newUnsatCoresProofs ok 4389 2326 2156 170 752 792 0 0 37 0 151051.9 387779.8
oldUnsatCores ok 4389 2394 2199 195 2174 730 0 0 81 0 146419.3 259669.8
QF_NRA newUnsatCoresAssumps-safe/ ok 135 65 57 8 57 70 0 0 45 0 10195.7 24701.4
newUnsatCoresProofs ok 135 71 49 22 35 64 0 0 5 0 10825.3 32982.8
oldUnsatCores ok 135 75 54 21 51 61 0 0 9 0 10865.3 27260.9
QF_RDL newUnsatCoresAssumps-safe/ ok 7 5 1 4 5 2 0 0 1 0 564.7 958.4
newUnsatCoresProofs ok 7 1 1 0 0 6 0 0 0 0 842.0 11029.6
oldUnsatCores ok 7 6 1 5 2 1 0 0 1 0 665.8 1982.6
QF_S newUnsatCoresAssumps-safe/ ok 5 1 1 0 0 4 0 0 0 0 603.3 191.4
newUnsatCoresProofs ok 5 5 5 0 2 0 0 0 0 0 161.9 285.8
oldUnsatCores ok 5 4 4 0 3 1 0 0 0 0 225.9 219.3
QF_SLIA newUnsatCoresAssumps-safe/ ok 258 74 67 7 70 184 0 0 64 0 27245.9 20290.4
newUnsatCoresProofs ok 258 179 163 16 47 79 0 0 6 0 18996.0 33722.6
oldUnsatCores ok 258 184 162 22 149 74 0 0 9 0 18395.8 23004.3
QF_UF newUnsatCoresAssumps-safe/ ok 29 25 0 25 6 4 0 0 2 0 2362.4 7504.3
newUnsatCoresProofs ok 29 0 0 0 0 28 1 0 0 0 3508.0 124190.7
oldUnsatCores ok 29 27 0 27 23 2 0 0 4 0 1866.3 13635.1
QF_UFBV newUnsatCoresAssumps-safe/ ok 2 2 0 2 1 0 0 0 1 0 189.5 1599.3
newUnsatCoresProofs to 2 0 0 0 0 2 0 0 0 0 241.8 1818.8
oldUnsatCores ok 2 1 0 1 1 1 0 0 0 0 193.7 1500.9
QF_UFIDL newUnsatCoresAssumps-safe/ ok 9 9 0 9 7 0 0 0 4 0 697.0 1133.0
newUnsatCoresProofs to 9 0 0 0 0 9 0 0 0 0 1088.0 14652.6
oldUnsatCores ok 9 5 0 5 2 4 0 0 0 0 848.5 2079.6
QF_UFLIA newUnsatCoresAssumps-safe/ ok 1 1 0 1 0 0 0 0 0 0 117.1 76.4
newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.9 208.5
oldUnsatCores ok 1 1 0 1 1 0 0 0 0 0 110.6 127.7
QF_UFLRA newUnsatCoresAssumps-safe/ ok 7 4 1 3 0 0 3 0 0 0 266.6 55098.3
newUnsatCoresProofs mo 7 0 0 0 0 0 7 0 0 0 261.7 56000.0
oldUnsatCores ok 7 7 4 3 7 0 0 0 3 0 408.4 20933.4
QF_UFNIA newUnsatCoresAssumps-safe/ ok 48 21 19 2 21 4 0 0 20 0 592.3 880.6
newUnsatCoresProofs ok 48 27 22 5 18 4 0 0 1 0 641.4 1548.8
oldUnsatCores ok 48 26 21 5 26 7 0 0 1 0 887.5 1044.6
QF_UFNRA newUnsatCoresAssumps-safe/ ok 1 1 1 0 1 0 0 0 1 0 108.3 17.9
newUnsatCoresProofs to 1 0 0 0 0 1 0 0 0 0 120.8 19.0
oldUnsatCores to 1 0 0 0 0 1 0 0 0 0 120.8 14.7
UF newUnsatCoresAssumps-safe/ ok 21 5 0 5 5 16 0 0 5 0 2123.8 3168.7
newUnsatCoresProofs ok 21 13 0 13 6 8 0 0 0 0 1496.3 6617.8
oldUnsatCores ok 21 16 0 16 11 5 0 0 3 0 1443.3 3919.2
UFDT newUnsatCoresAssumps-safe/ ok 35 6 0 6 6 29 0 0 5 0 3777.0 4485.5
newUnsatCoresProofs ok 35 28 0 28 15 7 0 0 0 0 1416.9 4293.6
oldUnsatCores ok 35 30 0 30 26 5 0 0 1 0 1406.9 3188.5
UFDTLIA newUnsatCoresAssumps-safe/ to 4 0 0 0 0 4 0 0 0 0 483.5 1640.5
newUnsatCoresProofs ok 4 4 0 4 1 0 0 0 0 0 139.3 942.3
oldUnsatCores ok 4 4 0 4 3 0 0 0 0 0 156.4 851.8
UFDTLIRA newUnsatCoresAssumps-safe/ ok 1 1 0 1 1 0 0 0 1 0 0.0 3.1
newUnsatCoresProofs ok 1 0 0 0 0 0 0 0 0 0 0.0 3.2
oldUnsatCores ok 1 0 0 0 0 0 0 0 0 0 0.0 2.7
UFDTNIRA newUnsatCoresAssumps-safe/ ok 10 3 0 3 3 6 0 0 3 0 754.8 1386.9
newUnsatCoresProofs ok 10 7 0 7 5 3 0 0 0 0 377.0 848.8
oldUnsatCores ok 10 7 0 7 7 3 0 0 0 0 376.5 563.4
UFLIA newUnsatCoresAssumps-safe/ ok 24 8 0 8 8 16 0 0 8 0 2231.6 3179.2
newUnsatCoresProofs ok 24 14 0 14 3 10 0 0 1 0 1915.5 5131.1
oldUnsatCores ok 24 15 0 15 14 9 0 0 2 0 1857.5 3479.7
UFNIA newUnsatCoresAssumps-safe/ ok 354 183 28 155 116 133 0 0 113 0 25941.4 839089.7
newUnsatCoresProofs ok 354 107 17 90 28 107 92 0 2 0 23496.9 1020258.1
oldUnsatCores ok 354 237 19 218 233 72 0 0 66 0 19906.9 914273.0
```
|
|
Fixes #6560.
|
|
Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:
Cannot name a term in a binder (e.g., quantifiers, definitions)
To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.
The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.
|
|
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
|
|
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.
|
|
Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were
applied too aggressively. Those rewrites attempt to rewrite string
equalities between concatenations where the prefix on one side is
provably shorter than the prefix on the other side. The length of the
shorter prefix is then stripped from the longer prefix. However, cvc5
was not checking whether it was able to strip the length of the full
prefix. If cvc5 cannot strip the full length of the shorter prefix, then
the rewrite does not apply because parts of the shorter prefix would
have to be kept. This commit adds an additional condition that checks
whether the length of the full prefix was stripped.
|
|
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.
|
|
applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
|
|
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
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).
|
|
|
|
Fixes #6495.
|
|
|
|
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
|
|
Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.
|
|
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
|
|
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
|
|
simplification (#6394)
This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.
This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.
In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.
This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.
|
|
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
|
|
This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
|
|
|
|
This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.
This is work towards adding proofs for macros.
|
|
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
|
|
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
|
|
|
|
|
|
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.
These benchmarks were fixed by 3c98bb2.
|
|
Previously, the circuit propagator was not learning literals of the form (= x t) where x is Boolean, since this term was not treated as a theory literal.
This commit changes that, which improves performance significantly, since it
allows the elimination of Boolean variables, which, in turn, can make the
justification heuristic much more effective.
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
The options --check-synth-sol and --check-abducts are independent from the rest of the solver. Hence, it is not necessary to run with/without them enabled in our regressions.
This saves roughly 30-40 seconds on regression regress0-2.
|
|
Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.
|
|
Fixes #5101.
|
|
Fixes #4400.
|
