summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2022-01-11Remove the rest of my CDHashMapsstarter-bellman-incincremental-no-hashmapMatthew Sotoudeh
2022-01-11This seems to be the best of the past few commitsincremental-current-bestincremental-adj-for-dirtyMatthew Sotoudeh
2022-01-11Just the dirty bit and CSEMatthew Sotoudeh
2022-01-11Revert "Try storing adjacency list"Matthew Sotoudeh
This reverts commit 44c0f0c949ca315710ad415bb173b45b856ca2d3.
2022-01-11Try storing adjacency listMatthew Sotoudeh
2022-01-11Try #1 for dirty nodesMatthew Sotoudeh
2022-01-10Use integer where easy toMatthew Sotoudeh
2022-01-10Avoid hash tablesMatthew Sotoudeh
2022-01-10Fix bug with incremental solverMatthew Sotoudeh
2022-01-07Propagate facts only at decision levelsMatthew Sotoudeh
2022-01-07Update rewriterMatthew Sotoudeh
2022-01-07Incremental Bellman-Ford implementation, seems to work fastMatthew Sotoudeh
2022-01-07Buggy incremental Floyd-WarshallMatthew Sotoudeh
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback