Age | Commit message (Collapse) | Author | |
---|---|---|---|
2022-01-11 | Remove the rest of my CDHashMapsstarter-bellman-incincremental-no-hashmap | Matthew Sotoudeh | |
2022-01-11 | This seems to be the best of the past few commitsincremental-current-bestincremental-adj-for-dirty | Matthew Sotoudeh | |
2022-01-11 | Just the dirty bit and CSE | Matthew Sotoudeh | |
2022-01-11 | Revert "Try storing adjacency list" | Matthew Sotoudeh | |
This reverts commit 44c0f0c949ca315710ad415bb173b45b856ca2d3. | |||
2022-01-11 | Try storing adjacency list | Matthew Sotoudeh | |
2022-01-11 | Try #1 for dirty nodes | Matthew Sotoudeh | |
2022-01-10 | Use integer where easy to | Matthew Sotoudeh | |
2022-01-10 | Avoid hash tables | Matthew Sotoudeh | |
2022-01-10 | Fix bug with incremental solver | Matthew Sotoudeh | |
2022-01-07 | Propagate facts only at decision levels | Matthew Sotoudeh | |
2022-01-07 | Update rewriter | Matthew Sotoudeh | |
2022-01-07 | Incremental Bellman-Ford implementation, seems to work fast | Matthew Sotoudeh | |
2022-01-07 | Buggy incremental Floyd-Warshall | Matthew Sotoudeh | |
2022-01-06 | Working on incremental solving | Matthew Sotoudeh | |
2022-01-06 | Floyd-Warshall is better | Matthew Sotoudeh | |
2022-01-06 | Check in some scripts | Matthew Sotoudeh | |
2022-01-06 | Bellman-Ford don't try to return as many cycles | Matthew Sotoudeh | |
2022-01-05 | Timeouts on the new cycle-finding | Matthew Sotoudeh | |
2022-01-05 | Better cycle finding | Matthew Sotoudeh | |
2022-01-04 | Switch to Bellman-Ford, extract the negative cycle, use as conflict | Matthew Sotoudeh | |
2022-01-04 | Use skolem var instead of constant | Matthew Sotoudeh | |
2022-01-04 | Support asserts like (= x 5) | Matthew Sotoudeh | |
2022-01-03 | Some formatting, remove sanitizers | Matthew Sotoudeh | |
2022-01-03 | Initial working | Matthew Sotoudeh | |
2022-01-03 | Update project | Andres Noetzli | |
2022-01-03 | Add instructions for cluster runs | Andres Noetzli | |
2022-01-03 | IDL solver starter project | Andres 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-22 | Remove most uses of mkRationalNode (#7854) | Andrew Reynolds | |
Towards eliminating arithmetic subtyping. | |||
2021-12-22 | Add support for incremental + interpolants (#7853) | Andrew Reynolds | |
Adds support for incrementality + get-interpol, including the get-interpol-next command. | |||
2021-12-21 | Support 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-21 | Eliminate remaining calls to callExtendedRewrite (#7839) | Andrew Reynolds | |
2021-12-21 | Rewrite (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-21 | Disable unit tests without poly (#7844) | Gereon Kremer | |
This PR disables the new unit tests from #7829 when poly is not available. | |||
2021-12-20 | Connect 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-20 | Eliminating 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-20 | Updates 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-20 | Allow 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-17 | api: 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-17 | Array-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-17 | Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835) | Andrew Reynolds | |
2021-12-17 | Fix 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-17 | Minor refactoring of API for eliminating arithmetic subtypes (#7833) | Andrew Reynolds | |
2021-12-17 | Fix 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-17 | Remove Rewriter::rewrite from bags type enumerator (#7827) | mudathirmahgoub | |
2021-12-17 | Refactoring 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-17 | Add relations.cpp, relations.py examples (#7801) | mudathirmahgoub | |