Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
Fixes cases of satisfiable unsat cores when proofs are enabled.
Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.
|
|
Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.
|
|
This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.
|
|
Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.
The benchmarks from the 2 issues timeout, a regression is added for the projects issue.
|
|
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
Fixes followup issues from #6604.
|
|
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.
|
|
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
```
|
|
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.
|
|
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 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 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 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.
|
|
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 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.
|
|
|
|
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.
|
|
|
|
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.
These benchmarks were fixed by 3c98bb2.
|
|
Fixes #5101.
|
|
Fixes #4400.
|
|
|
|
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
|
|
Fixes benchmarks 2 and 3 from #5848.
|
|
Fixes #5942.
This benchmark was fixed by recent changes to ppRewrite.
|
|
Fixes #4370.
|
|
Fixes #4179.
|
|
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
|
|
|
|
Fixes #4328.
|
|
We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.
Fixes #5705.
|
|
Fixes the first benchmark from #6203.
|
|
This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.
This fixes the second benchmark from #6203.
This PR also improves our traces for checking models in strings.
|
|
|
|
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
|
|
|
|
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
|
|
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.
Fixes #6132.
|
|
String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode.
This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered.
The PR also simplifies our policies for when string terms are registered slightly.
Fixes #6072.
|