Update to latest libpoly version (#7906)

This PR updates to the latest libpoly version. It contains a bugfix and adds division and inverse operations for algebraic numbers.

api: Remove Sort::isComparableTo(). (#7903)

Since we do not support arithmetic subtyping on the API level anymore,
this function is obsolete. Consequently, this now requires that
replacement terms as arguments to Term::substitute() are of the same
sort as the replaced terms.

Avoid gcc/10.1.0 bug by moving some configuration into a namespace

Eventually there is intention to move all of cvc5::Configuration into
cvc5::configuration, this is a first step that also has the nice side-effect of
letting it build under an otherwise-buggy version of gcc/10.1.0 that was
causing issues.

Signed-off-by: Matthew Sotoudeh <sotoudeh@stanford.edu>

Start post-release for 0.0.5

Bump version to 0.0.5

Improve docs extension for examples (#7900)

We recently added automatic download links for examples in our documentation, however they assumed everything to live inside the main cvc5 repo while, e.g., the examples for the z3py compat API do not. While #7896 provided a very simple fix, it mixes different concerns (rendering of tabs vs. locating the input files, though they should coincide right now).
This PR takes a more fundamental approach by extending the current pattern mechanism to allow for explicit url specification.

Closes #7896.

Python Idomatic API: Document solver, results, utilities, and fns (#7882)

I put fns into "Core & Booleans".

Remove CDDenseSet data structure (#7890)

It was not used anywhere, and does not appear to build under, at least,
GCC/9.1.0.

Signed-off-by: Matthew Sotoudeh <sotoudeh@stanford.edu>

Fix eager string preprocessing in incremental mode (#7895)

Fixes #5780.

Issue was caused by reintroducing skolems during preprocessing that were already solved for.

Some minor improvements to the theory references (#7881)

Add regressions for array sequence solver (#7874)

This closes the seqArray branch.

Document quantifiers in idiomatic python API (#7880)

[Regressions] Add directive for disabling testers (#7892)

This commit adds a directive for regressions (`DISABLE-TESTER`) that
allows disabling a given tester for a regression. Currently, we disable
testers based on properties such as command line arguments, which can be
error prone.

Make alpha equivalence user context dependent (#7889)

Fixes #5373

Issues were occurring due to using quantified formulas in alpha equivalence that were stale.

This also removes spurious warnings from quantifier elimination (dropping the "strict" requirement, which unnecessarily warns if we are in a non-arithmetic logic).

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)