summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2022-01-07Fix the rewriterstarterProjectMatthew Sotoudeh
2022-01-07Revert "Working on incremental solving"Matthew Sotoudeh
This reverts commit 5b47d4cd09ba93b40ac303d8825a5a2593e97fa7. See branches starter-*-inc instead
2022-01-06Working on incremental solvingMatthew Sotoudeh
2022-01-06Floyd-Warshall is betterMatthew Sotoudeh
2022-01-06Check in some scriptsMatthew Sotoudeh
2022-01-06Bellman-Ford don't try to return as many cyclesMatthew Sotoudeh
2022-01-05Timeouts on the new cycle-findingMatthew Sotoudeh
2022-01-05Better cycle findingMatthew Sotoudeh
2022-01-04Switch to Bellman-Ford, extract the negative cycle, use as conflictMatthew Sotoudeh
2022-01-04Use skolem var instead of constantMatthew Sotoudeh
2022-01-04Support asserts like (= x 5)Matthew Sotoudeh
2022-01-03Some formatting, remove sanitizersMatthew Sotoudeh
2022-01-03Initial workingMatthew Sotoudeh
2022-01-03Update projectAndres Noetzli
2022-01-03Add instructions for cluster runsAndres Noetzli
2022-01-03IDL solver starter projectAndres Noetzli
2021-12-23[Regressions] Support more complex scrubbers (#7819)Andres Noetzli
Currently, we only support single commands in our `SCRUBBER` directives for regression tests. This commit adds support for executing more complex commands, including pipes. It also updates the regression script to use the more modern, higher-level `subprocess.run()` instead of `subprocess.Popen()`.
2021-12-22Remove most uses of mkRationalNode (#7854)Andrew Reynolds
Towards eliminating arithmetic subtyping.
2021-12-22Add support for incremental + interpolants (#7853)Andrew Reynolds
Adds support for incrementality + get-interpol, including the get-interpol-next command.
2021-12-21Support get-abduct-next (#7850)Andrew Reynolds
Adds support for incremental abduction, adds regression for using push/pop in combination with get-abduct, and a use of get-abduct-next. Adds this method to C++, java API. Interpolation/abduction not yet supported in Python API, I'm waiting for @yoni206 to add this; getAbductNext will be added to Python API in followup PR.
2021-12-21Eliminate remaining calls to callExtendedRewrite (#7839)Andrew Reynolds
2021-12-21Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)yoni206
Fixes https://github.com/cvc5/cvc5-projects/issues/371. Fixes https://github.com/cvc5/cvc5-projects/issues/339. Fixes https://github.com/cvc5/cvc5-projects/issues/333. Variants of the tests in the above issues are added to this PR. In them, we expect to get an exception because the constant is too big.
2021-12-21Disable unit tests without poly (#7844)Gereon Kremer
This PR disables the new unit tests from #7829 when poly is not available.
2021-12-20Connect sequences array solver to strategy in theory of strings (#7847)Andrew Reynolds
Also corrects an issue with model construction, where SEQ_NTH should be assignable in addition to SEQ_NTH_TOTAL. seqArray branch (which has regressions) can be merged to master after this PR.
2021-12-20Eliminating some uses of const rational in arithmetic (#7846)Andrew Reynolds
Note that there are several nested dependencies in arithmetic for constructing constants Constant::mkConstant ---> mkRationalNode ---> mkConst(CONST_RATIONAL, r) This starts to disambiguate these calls.
2021-12-20Updates to LFSC signatures (#7840)Andrew Reynolds
Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions.
2021-12-20Allow SyGuS subsolver to be reused in incremental mode (#7785)Andrew Reynolds
This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next. By default, the SyGuS subsolver will generate a new solution for each successive check-synth. This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case. This completes our support for incremental SyGuS.
2021-12-20[Sequences/Array Solver] Minor refactoring (#7843)Andres Noetzli
This commit performs a minor refactoring of our array core solver. It adds more comments and avoids sending the STRINGS_ARRAY_NTH_TERM_FROM_UPDATE lemma more than once in a given user context.
2021-12-20[proofs] Fix helper LFSC script (#7845)Haniel Barbosa
2021-12-17api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)Aina Niemetz
2021-12-17[Strings] Minor fixes/improvements (#7837)Andres Noetzli
This is a quick follow-up for PR #7815. My comments didn't make it in before the PR was merged, so this commit fixes some of the minor issues I found.
2021-12-17Array-inspired Sequence Solver - Fixing several issues in the ↵Ying Sheng
ArrayCoreSolver class and options (#7820) This commit fixes several issues in the ArrayCoreSolver class and the options: 1. Add range checking for an update rule. 2. Assign different inference ids to different rules. 3. small syntax optimizations.
2021-12-17Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835)Andrew Reynolds
2021-12-17Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)Andres Noetzli
Fixes https://github.com/cvc5/cvc5-projects/issues/390. This commit fixes two issues with the rewrite: (1) the rewrite should only apply if the update is of size 1 and (2) the `str.rev(...)` should be removed inside the `str.update(...)`.
2021-12-17Minor refactoring of API for eliminating arithmetic subtypes (#7833)Andrew Reynolds
2021-12-17Fix tracker in SubstitutionMap (#7829)Gereon Kremer
This PR fixes a subtle issue in #7787 where the rhs (instead of the lhs) of the applied substitution was inserted into the tracker. Fixes cvc5/cvc5-projects#388
2021-12-17Remove Rewriter::rewrite from bags type enumerator (#7827)mudathirmahgoub
2021-12-17Refactoring initialization of proofs (#7834)Andrew Reynolds
Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.
2021-12-17Add relations.cpp, relations.py examples (#7801)mudathirmahgoub
2021-12-17More documentation for idiomatic python API (#7798)Alex Ozdemir
Arithmetic, bit-vectors, arrays.
2021-12-17Get getRealOrIntegerValueSign to the API (#7832)Andrew Reynolds
2021-12-17Implement model construction for the array extension of sequences (#7815)Andrew Reynolds
The array solver is still not usable, the only remaining changes from seqArray are to connect the array solver to the strings theory solver via the strategy + the regressions.
2021-12-16api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831)Aina Niemetz
2021-12-17api: Add Solver::mkUnresolvedSort(). (#7817)Aina Niemetz
This adds a function to create unresolved sorts for mutually recursive datatpes. This function creates an uninterpreted sort if the arity of the unresolved sort is 0, and a sort constructor sort otherwise.
2021-12-17Eliminate more uses of CONST_RATIONAL (#7816)Andrew Reynolds
2021-12-16Disable unsat cores for quaternion_ds1_symm_0428.fof.smt2. (#7830)Mathias Preiner
Avoids timeout for nightly ASAN builds.
2021-12-16Eliminate most static calls to rewrite in quantifiers (#7823)Andrew Reynolds
2021-12-16Fix get-model when sort constructors are present (#7828)Andrew Reynolds
Fixes a spurious error on kind benchmarks. Note that we don't properly handle instantiated sort constructors currently, which I believe need to be handled as declared sorts when calling getModel.
2021-12-16[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf ↵Haniel Barbosa
Stream (#7826) These will be necessary for upcoming changes to the SAT proof manager and Proof Cnf Stream to handle incremental proofs when optimizing the level of SAT clauses.
2021-12-16api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback