Age | Commit message (Collapse) | Author |
|
|
|
This reverts commit 5b47d4cd09ba93b40ac303d8825a5a2593e97fa7.
See branches starter-*-inc instead
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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()`.
|
|
Towards eliminating arithmetic subtyping.
|
|
Adds support for incrementality + get-interpol, including the get-interpol-next command.
|
|
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.
|
|
|
|
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.
|
|
This PR disables the new unit tests from #7829 when poly is not available.
|
|
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.
|
|
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.
|
|
Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions.
|
|
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.
|
|
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.
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
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(...)`.
|
|
|
|
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
|
|
|
|
Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.
|
|
|
|
Arithmetic, bit-vectors, arrays.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
Avoids timeout for nightly ASAN builds.
|
|
|
|
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.
|
|
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.
|
|
|