Disallow separation logic in incremental mode (#7888)

Fixes #5541. Fixes #5607.

Improve theory combination in the presence of real algebraic numbers (#7883)

This PR changes how we handle real algebraic numbers in theory combination and model construction.
The goal is to improve getEqualityStatus() and produce proper models more often.
We now use a RAN-aware evaluator for getEqualityStatus() and change the way how the nonlinear extension finalizes its model.

Fix non-idempotent rewrite in arrays (#7887)

Fixes #6807.

Minor cleaning of non-clausal simplification (#7886)

cppapi: Remove Datatype::hasNestedRecursion(). (#7878)

Datatypes with nested recursion are a highly experimental feature and we
currentle don't even have a decision procedure for them.

Py idiomatic API: Doc sets, datatypes, FP (#7877)

api: Add missing guard for Datatype::isFinite(). (#7879)

Properly parse arithmetic values (#7876)

This makes our parser correct for arithmetic values e.g. (- n) is parsed as a value not UMINUS when n is a numeral, as indicated in SMT-LIB. Similarly for (/ m n) and (/ (- m) n) we parse as values and not DIVISION.

This subsumes a patch for constructing array constants where this led to issues.

Track input list for atoms in difficulty manager (#7851)

This makes our support for get-difficulty faster by tracking the set of input formulas that atoms occur in, which is highly important for benchmarks with many assertions and where many lemmas are added at standard effort.

This is work towards making get-difficulty scale on a large benchmark from Certora.

Don't use python's collections.Set (#7875)

We used to use collections.Set.

Apparently this was an alias for collections.abc.Set. I can't find it
documented anywhere though, going as far back as Python 3.5. Perhaps it
was an undocumented left-over from when the collections.abc module was
split out from collections in Python 3.3?

At any rate, the alias appears broken in Python version 3.10.1.

Now we just use the builtin set type, which is what we wanted anyway,
I think.

Properly set __file__ in python bindings (#7867)

When running make docs after changing the documentation in cvc5.pxi, the html files are not updated. This PR fixes this issue.

Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de

Fix proofs for datatype purify (#7841)

Previously we were failing to produce proofs for purification lemmas (= t witness_form(t)) from datatypes.

Change default granularity of proofs to macro (#7855)

Also changes the name "off" to "macro" to be more consistent.

Reorder NodeManager class according to code guidelines. (#7873)

This only moves code, and removes some redundant inline keywords.

Add utility expr::isBooleanConnective (#7869)

Remove spurious call to applySubs (#7871)

This call is preceded by another call to `apply-subs` at the beginning of preprocessing.

This is motivated by very large input benchmarks from Cetora where this preprocessing pass can take up to 5 seconds.

Remove unused shutdown infrastructure (#7872)

Fix int blaster (#7856)

Add bag.member operator to theory of bags (#7857)

This PR adds the predicate bag.member to be analogous to predicate set.member.
The PR is motivated by converting regressions for sets to bags, which avoids defining a predicate for each set type

(define-fun bag.member ((e E) (B (Bag E))) Bool (>= (bag.count e B) 1))

[proofs] [sat] Add manager for optimized clauses and their proofs (#7824)

This utility is going to be used by both the proof cnf stream and the sat proof manager to re-add to their respective internal proofs the proof nodes that were stored for clauses saved within the SAT solver at an assertion level below the current user level.

The utility is a context notify object, which means that it can be called when the tracked context pops.

Refactor bag solver (#7770)

Adding interpolation and abduction to the python API (#7868)

This PR adds getAbduct, getAbductNext, getInterpol, and getInterpolNext to the python API.
Tests and documentation are added as well.

api: Add unit test for null case of Sort::toString(). (#7865)

api: Remove redundant check in Term::toString(). (#7866)

Update quantifiers compute elim symbols to be iterative dag traversal (#7822)

Fixes cvc5/cvc5-projects#389.

[BV] Remove non-existent `friend` class (#7864)

Add download link for examples in documentation (#7836)

This PR adds a download link to all examples in the documentation
(that are included via the examples extension). I think we should do
this, as we have text like "download the example here" at several
places already...

api: Remove redundant check in Sort::toString(). (#7863)

Remove static options from sat solver. (#7790)

This PR removes options::foo() from minisat.

Execute `(reset)` command in parse-only mode (#7862)

This commit fixes an issue where `--parse-only` would not execute
`(reset)` commands, leading to issues with symbols being defined
multiple times.

[Regressions] Support more complex scrubbers (#7819)

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()`.

Remove most uses of mkRationalNode (#7854)

Towards eliminating arithmetic subtyping.

Add support for incremental + interpolants (#7853)

Adds support for incrementality + get-interpol, including the get-interpol-next command.

Support get-abduct-next (#7850)

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.

Eliminate remaining calls to callExtendedRewrite (#7839)

Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)

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.

Disable unit tests without poly (#7844)

This PR disables the new unit tests from #7829 when poly is not available.

Connect sequences array solver to strategy in theory of strings (#7847)

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.

Eliminating some uses of const rational in arithmetic (#7846)

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.

Updates to LFSC signatures (#7840)

Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions.

Allow SyGuS subsolver to be reused in incremental mode (#7785)

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.

[Sequences/Array Solver] Minor refactoring (#7843)

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.

[proofs] Fix helper LFSC script (#7845)

api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)

[Strings] Minor fixes/improvements (#7837)

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.

Array-inspired Sequence Solver - Fixing several issues in the 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.

Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835)

Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)

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(...)`.

Minor refactoring of API for eliminating arithmetic subtypes (#7833)

Fix tracker in SubstitutionMap (#7829)

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

Remove Rewriter::rewrite from bags type enumerator (#7827)

Refactoring initialization of proofs (#7834)

Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.

Add relations.cpp, relations.py examples (#7801)

More documentation for idiomatic python API (#7798)

Arithmetic, bit-vectors, arrays.

Get getRealOrIntegerValueSign to the API (#7832)

Implement model construction for the array extension of sequences (#7815)

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.

api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831)

api: Add Solver::mkUnresolvedSort(). (#7817)

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.

Eliminate more uses of CONST_RATIONAL (#7816)

Disable unsat cores for quaternion_ds1_symm_0428.fof.smt2. (#7830)

Avoids timeout for nightly ASAN builds.

Eliminate most static calls to rewrite in quantifiers (#7823)

Fix get-model when sort constructors are present (#7828)

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.

[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf 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.

api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825)

Minor fix for print benchmark. (#7821)

Also adds benchmark that triggered this issue.

bv-to-int: use pow2 operator (#7812)

Currently, the int-blaster translates shifts using an ite whose size is the bit-width.
This PR adds an option to use the internal pow2 operator instead.

int-to-bv: fail if one of the arguments has type real (#7810)

This PR generates a failure in int-to-bv in case a real argument is detected as a child of an arithmetic operation.
fixes cvc5/cvc5-projects#348 .

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com

Add regression bags-of-bags-subtypes.smt2 (#7814)

Explicitly disallow `mkConst(Rational)` (#7818)

The Rational payload can be associated with two kinds (CONST_INTEGER
and CONST_RATIONAL), so we should never call
NodeManager::mkConst(Rational), but instead use
NodeManager::mkConstInt() and NodeManager::mkConstReal(). Currently,
calling NodeManager::mkConst(Rational) silently creates an integer
constant, which is dangerous. This commit makes it a compile-time error
instead.

Ensure match terms are exhaustive in its type rule (#7807)

Fixes cvc5/cvc5-projects#382.

Makes it so that we always fully type check match terms before they are rewritten, which guards potential unsoundness.

api: Fix smt-lib code blocks and math in C++ docs. (#7795)

Add trace to see inferences in final proof (#7813)

Adds -t im-pf to see which inferences occur in the final proof. Must be used with proofs and --proof-annotate.

Eliminate static calls to rewrite in strings (#7803)

Fix cvc5-projects issue 358 (#7804)

This PR fixes issue cvc5/cvc5-projects#358 which is caused by unregistered terms in the equality engine of bags

Add a random Sygus enumerator. (#7782)

This PR adds a Sygus enumerator that generates random terms from a grammar. The size of the terms generated by the enumerator approximates a geometric distribution and can be configured with an option.

Make some undocumented options regular/expert (#7805)

We have some options that are currently "undocumented" for no good reason.
This PR makes them regular or expert options.

Fix issues with tracing builds (#7809)

This PR fixes two issues that were revealed when analyzing decreased performance on trace-enabled builds.
hasIntegerModel() turns out to be a rather expensive method and should thus not be called in a Trace output.
Furthermore, the implementation of Rational::isIntegral() was generally bad because it used getDenominator() (which returns a copy of the denominator as an Integer) instead of directly checking the underlying denominator with equality for zero.

Add switches to toggle eager and inclusion solvers (#7784)

Connecting the core array solver in strings (#7800)

This PR takes most of the remaining changes from the seqArray branch apart from the extension to model construction.

Notably it connects the core array solver to the array solver in strings.

Minor fix for sygus unsat query generator (#7811)

Throw exception for getting value of non-well-founded datatype (#7806)

Fixes cvc5/cvc5-projects#383

Eliminate use of rewrite, CONST_RATIONAL in ArithMSum (#7808)

api: Add note to Solver::mkDatatypeSorts. (#7799)

Distinguishing more uses of CONST_RATIONAL (#7802)

Towards eliminating subtyping Int/Real.

A more efficient implementation for bag.card operator (#7797)

This PR provides a fold like implementation for bag.card operator that does not depends on higher order logic, although it still requires finite model finding.

Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

Fixes and additions for API for parametric datatypes (#7760)

Update Relations.java (#7796)

Improve nonlinear solver (#7787)

This PR does two things:

we remove splitting on shared values
we add variable elimination for the cad-based solver, exploiting equalities present in the input.

Integrate new int-blaster (#7781)

This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.

Tests are updated and added, as well as other minor changes.

Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345
cvc5/cvc5-projects#344
cvc5/cvc5-projects#343

@mpreiner FYI

Fix cvc5-projects issues  #358 and #375 (#7743)

api: Use 'note' constructs for API documentation. (#7794)

This uses '@note' for notes in the C++ API documentation, '.. note::'
for Python, and '@apiNote' for Java.

Reorganize declareDatatype unit tests. (#7767)

Refactor and fixes related to getSpecializedConstructorTerm (#7774)

Fixes cvc5/cvc5-projects#381.

Array-inspired Sequence Solver - Adding the ArrayCoreSolver class and options (#7723)

This pull request adding the ArrayCoreSolver class and the options to turn on the array-inspired sequence solver.

Eliminate more static rewrites (#7786)

This PR eliminates almost all remaining static rewrites from the arithmetic theory.

Some cleanup around trace and debug (#7792)

Some minor cleanup in our output routines. While ScopedDebug and ScopedTrace are never used at all (and don't seem to make much sense considering how we use Debug and Trace), IndentedScope may be useful in some more places.

Mute `define-fun` command generated for named terms. (#7788)

Kind 2 uses print-success option to track cvc5's status after each command. When I added implicit define-fun commands for each named term (needed for raw-benchmark), cvc5 started printing spurious ; success messages. This change ended up crashing Kind 2's driver for cvc5. This PR fixes this issue by muting the results of those implicit define-fun commands.

Allow for wildcards in `-t` (#7791)

This PR extends -t to allow for wildcards: -t nl-ext-*. Internally, these wildcards are replaced by .* and fed into std::regex.

[proofs] Make LazyCDProofChain extend CDProof (#7726)

This commit makes LazyCDProofChain behave more similarly to LazyCDProof, in that it is an object that not only builds a proof to a fact based on lazy steps but also on regular steps that may already have for it.

The motivation for this commit is the upcoming handling of context-dependent proofs in incremental mode, which benefits from a more uniform behavior between CDProof, LazyCDProof and LazyCDProofChain (with the latter two both extending CDProof).