summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2021-05-25address commentsAndres Noetzli
2021-05-24documentationAndres Noetzli
2021-05-24fix testsAndres Noetzli
2021-05-24one moreAndres Noetzli
2021-05-24correct typesAndres Noetzli
2021-05-24missing fileAndres Noetzli
2021-05-24More precise includes of `Node` constant classesAndres Noetzli
2021-05-24Implementation of the new justification heuristic (#6465)Andrew Reynolds
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.
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
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").
2021-05-24Fix re-elim length requirement for symbolic RE memberships (#6609)Andrew Reynolds
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.
2021-05-24Fix instance of no rewrite in extended rewriter (#6610)Andrew Reynolds
Fixes #6545. An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.
2021-05-24Better formalization of regular expression unfolding skolems (#6602)Andrew Reynolds
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.
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
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).
2021-05-21Fix and refactor relevant domain (#6528)Andrew Reynolds
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.
2021-05-21Formalize shared selectors as skolem functions (#6591)Andrew Reynolds
This is work towards properly printing shared selectors in external proofs.
2021-05-21Minor simplification to boolean proof checker (#6590)Andrew Reynolds
2021-05-21(proof-new) Minor documentation sync (#6592)Andrew Reynolds
2021-05-21Add utility to get all types occurring in a term (#6588)Andrew Reynolds
Required for external proof conversions.
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
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.
2021-05-21Support braced-init-lists with `mkNode()` (#6580)Andres Noetzli
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.
2021-05-21Use scikit-build CMake files for pycvc5 (#6543)makaimann
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.
2021-05-21Move option names out of struct (#6554)Gereon Kremer
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Properly initialize. (#6586)Gereon Kremer
This PR fixes a missing initialization that lead to a valgrind warning.
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
2021-05-20Avoid using printSynthSolution in the python API and examples (#6564)yoni206
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.
2021-05-20Minor improvements to the API (#6585)Gereon Kremer
This PR does some minor improvements to the API: - remove getConstSequenceElements(), use getSequenceValue() instead - improve documentation for Term
2021-05-20Fix echo printing. (#6573)Aina Niemetz
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.
2021-05-20Add more getters for api::Term (#6496)Gereon Kremer
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.
2021-05-20Expand arith's farkas lemma rule as a macro (#6577)Alex Ozdemir
reflects that it is a macro, which we will eliminate
2021-05-19Remove unused methods from `NodeManager` (#6578)Andres Noetzli
2021-05-19Correctly handle negated assertions for assumption-based unsat cores. (#6579)Mathias Preiner
2021-05-19Pass empty vector when constructing re empty, fixes rewrite (#6576)Andrew Reynolds
Fixes #6567.
2021-05-19Make output list of `mkoptions.py` more accurate (#6572)Andres Noetzli
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.
2021-05-19Make strings emp inference an unhandled inference for proofs (#6575)Andrew Reynolds
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.
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
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 ```
2021-05-19Fix strings rewriter for non-standard re range (#6570)Andrew Reynolds
Fixes #6561. Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
This also makes the relations solver use the inference manager in the standard way.
2021-05-19bv: Add support for --bitblast=eager. (#6516)Mathias Preiner
This PR adds support for handling --bitblast=eager in the new bitblast solver.
2021-05-19Fix positive contains indexof rewrites for empty string second argument (#6566)Andrew Reynolds
Fixes #6560.
2021-05-19Remove accidental print (#6568)Gereon Kremer
2021-05-19Generate command line options for sphinx docs (#6555)Gereon Kremer
This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.
2021-05-19Improve handling of `:named` attributes (#6549)Andres Noetzli
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.
2021-05-19Fix handling of non-standard re.range terms (#6563)Andrew Reynolds
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.
2021-05-18Loop over terms to reconstruct instead of obligations. (#6504)Abdalrhman Mohamed
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.
2021-05-18Fix `collectEmptyEqs()` in string utils (#6562)Andres Noetzli
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.
2021-05-18(proof-new) Miscellaneous updates to strings from proof-new (#6557)Andrew Reynolds
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.
2021-05-18Fix smt2 printing (#6558)Andrew Reynolds
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.
2021-05-18Add Solver.java to the Java API (#6196)mudathirmahgoub
PR changes: Add Solver.java and relation JNI c files Update FindJUnit to download JUnit5 Add Java unit tests
2021-05-17Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)Andres Noetzli
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback