Refactor atom rewriting to be RAN-aware (#7928)

This PR starts refactoring the arithmetic rewriter by making rewriting of atoms aware of real algebraic numbers.
It also is slightly more aggressive now, directly rewriting relational operators where lhs = rhs in the preRewrite stage.

Refactor rewriteMinus (#7932)

Refactors rewriteMinus to be generally simpler and explicitly rely on rewriting addition.
Note that rewriteMinus would almost never be called in post rewrite anyway, as it would rewrite to addition in pre rewrite.

Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)

This prevents the SyGuS subsolver from having a different configuration of dt-share-sel than the main SyGuS solver. Having this mismatch can lead to incorrect synthesis results.

Fixes #7925.

Always enable RAN, but disable its implementation without poly (#7910)

This PR makes sure that the RealAlgebraicNumber class is always visible, but its implementation is only enabled when libpoly is available. This allows us to use this class in more places of cvc5.

Add mkRealAlgebraicNumber (#7923)

This PR adds the convenience function NodeManager::mkRealAlgebraicNumber().

Always use partial function for sqrt (#7926)

Fixes the behavior reported in #7924.

Eliminate use of subtyping from results of quantifier elimination (#7885)

Fixes #7870.

Notice this node converter is potentially unnecessary if we ever get rid of arithmetic subtyping.

Adds a kind to hold RealAlgebraicNumber constants (#7908)

This PR adds a new kind that holds RealAlgebraicNumber constants. As it can not be a constant in the sense of isConst(), it is wrapped within an operator, similar to IAND or CARDINALITY_CONSTRAINT.

Disable filtering of shapes in sygus-rcons pool. (#7922)

This PR disables filtering of enumerated shapes in the pool of the Sygus reconstruction algorithm.

Fix `TypeNode::substitute()` for type constants (#7920)

Fixes cvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.

api: Fix formatting of docs for Term::getSetValue(). (#7914)

Remove static accesses to options (#7913)

This PR removes some more calls like options::foo() in favor of options().module.foo.

Tighten policy for unsat cores in sygus core connective (#7911)

Previous policy was due to limitations on options on subsolvers, which no longer exist.

Fixes cvc5/cvc5-projects#354.
Fixes #7902.

Guard use of unsat core mode pp-only (#7899)

Fixes cvc5/cvc5-projects#366. Now gives
(error "Error in option parsing: Unsat core mode pp-only is for internal use only.")

Fix `TypeNode::substitute()` (#7916)

Fixes cvc5/cvc5-projects#397. Fixes
cvc5/cvc5-projects#399. After performing the
substitution on the child node, the result was not added as a child to
the node under construction, resulting in nodes with too few children.
This commit fixes that issue.

Check the synthesized funs of `check-synth-next`. (#7915)

This PR ensures that the functions synthesized by cvc5 with check-synth-next command(s) are different from the preceding ones.

Add new idiomatic examples (#7912)

[Win64] Link LibPoly statically for static builds (#7891)

Fixes #7861. LibPoly was not getting linked statically for Windows
builds, even when building a static version of cvc5. This commit fixes
the issue.

Fix internal type error when printing lambdas with more than one variable in LFSC (#7909)

Check arity in Sort::instantiate (#7897)

Fixes cvc5/cvc5-projects#386.

Add new methods for RealAlgebraicNumber (#7907)

This PR adds some new methods for the RealAlgebraicNumber class: division, computing the (multiplicative) inverse and a specialization of std::hash.

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.