Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This adds the new implementation of the justification heuristic. It does not enable this strategy yet.
A followup PR will activate this strategy within DecisionEngine.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
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 replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.
It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.
|
|
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).
|
|
In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.
This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.
Fixes #6476. The benchmark from that issue now times out.
|
|
This is work towards properly printing shared selectors in external proofs.
|
|
|
|
|
|
Required for external proof conversions.
|
|
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.
|
|
This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.
|
|
This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.
This PR is a piece of this old one (#5657) which I am closing and splitting up.
|
|
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
|
|
|
|
This PR fixes a missing initialization that lead to a valgrind warning.
|
|
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
|
|
The function printSynthSolution declared here is going to be removed in #6521.
This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.
|
|
This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term
|
|
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.
|
|
This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
|
|
reflects that it is a macro, which we will eliminate
|
|
|
|
|
|
Fixes #6567.
|
|
After commit 6dc5b74, cvc5 was always
being almost completely rebuilt, even if there hadn't been any changes
if cvc5 was configured not to produce documentation (the default).
This was because mkoptions.py only produces the
options_generated.rst file when documentation is enabled. However, it
was unconditionally declared to be an output of the script in
CMakeLists.txt. As a result, the options (and thus most of the code
base) were rebuilt every time because the file was missing in builds
without documentation. This commit modifies the output list depending on
the configuration.
|
|
The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.
This was caught by a new regression on the soon-to-be-merged jh-new branch.
|
|
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 #6561.
Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
|
|
This also makes the relations solver use the inference manager in the standard way.
|
|
This PR adds support for handling --bitblast=eager in the new bitblast solver.
|
|
Fixes #6560.
|
|
|
|
This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.
|
|
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.
|
|
Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").
This PR also makes isConstRegExp do a non-recursive dag traversal.
|
|
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.
|
|
This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants.
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.
|
|
This fixes bugs related to the smt2 printer where we rely on stream operators for recursive printing calls for certain parts of terms.
Notice that a call to
`out << n;`
within `SmtPrinter::toStream(...)` is wrong since then recursively `n` is printed with the current output language. This means that if one were to ask to print a term in SMT2 format and the output language is not SMT2, then the above call would print `n` in a different format.
This is required to fix bugs in the LFSC proof converter, which explicitly changes the output format to SMT2.
|
|
PR changes:
Add Solver.java and relation JNI c files
Update FindJUnit to download JUnit5
Add Java unit 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.
|