Add node utils for the arithmetic rewriter (#8012)

This PR adds a bunch of small utilities to inspect or create nodes in the arithmetic rewriter.

Send all `nth` terms to the core array solver (#7990)

This updates our policy for the sequences array solver to send all
updates to the array core solver.

Rename kind PLUS -> ADD. (#8036)

This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).

api: Remove obsolete function declaration in Cython bindings. (#8032)

api: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8034)

This renames the arithmetic kinds MINUS and UMINUS on the
API level for consistency with our naming scheme for other
operators (e.g., BITVECTOR_SUB, FLOATINGPOINT_SUB).

api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)

Fixes cvc5/cvc5-projects#412.

Change name of Python API's package from pycvc5 to cvc5. (#7953)

In the process, I changed a CMake target name from pycvc5 to
cvc5_base_py_api. I could not change the target to cvc5, because that
name is taken.

Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)

Fixes cvc5/cvc5-projects#441.
Fixes cvc5/cvc5-projects#414.

Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)

This renames the internal arithmetic kinds MINUS and UMINUS for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_SUB, FLOATINGPOINT_SUB).

Use proper filename in -o subs documentation (#8030)

We somehow used the wrong filename in #7944.

Fix invalid rewrite involving iand (#8026)

Fixes #8016.

api: Rename mk<Value> functions for FP for consistency. (#8033)

Fix printing of re.loop as an operator in LFSC (#8029)

Make LFSC side condition for concat unify robust to equality with full string (#8028)

Was leading to LFSC proof checking failures.

Add missing null terminators for regexp (#8027)

Led to some LFSC proof checking failures on strings benchmarks.

Add additional check to avoid cyclic substitution (#7991)

The substitutions we extract from equalities in the nonlinear solver would sometimes generate cyclic substitutions.
This PR tries harder to avoid such cases.
Fixes cvc5/cvc5-projects#444.

Update datatypes.rst (#8009)

Remove more static calls to rewrite (#8025)

Extend proof step buffer to optionally ensure unique conclusions (#8017)

Fixes cvc5/cvc5-projects#439.

This extended (theory) proof step buffer with options for discarding duplicate conclusions. This option is now used in the strings theory proof construction, which may have duplication of conclusions due to purification. It simplifies some of the logic regarding popStep in this utility which is required due to the new policy.

Fix parser issue with tuple_project operator (#8021)

The current parser accepts the smtlib code below since it ignores all arguments after z.
This PR fixes this issue by sending all arguments to the operator to be checked.

(set-logic ALL)
(declare-fun z () (Tuple Int Int Int Int Int Int))
(declare-fun f () (Tuple Int Int Int))
(assert (= f ((_ tuple_project 0 1 2) z f f f f f f f f 0 0 0 0 0)))
(check-sat)

[BV] Fix strategy for `RewriteExtract` (#8011)

`RewriteExtract` was being too eager to return `REWRITE_DONE`. In
particular, it could happen that a term could be rewritten by a series
of `ExtractExtract` and `ExtractConcat` rewrites, but the method would
return `REWRITE_AGAIN` after the first application of `ExtractExtract`.
This commit fixes the method to be more conservative and return
`REWRITE_AGAIN` whenever a rewrite changed the node being rewritten.
Additionally, the commit makes constant folding the last step (to
maximize the chances that it applies) and makes `ExtractExtract` rewrite
multiple nested applications of `extract` with a single application.

[BV] Fix order of rewrites for `concat` (#8010)

This commit fixes the order of the rewrites for bit-vector
concatentation such that the rewrite that merges adjacents constants
comes last (the commit also updates the comments to be less confusing).
Before, it could happen that the rewrite step that removes unnecessary
extract operations introduces constants then then would not get merged
before returning REWRITE_DONE.

Add new ordering utility (#8008)

This PR provides a clean implementation of the comparators from the normal form utility, also supporting real algebraic numbers. They will be used within the refactored arithmetic rewriter.

Add variant of get-difficulty for full effort lemmas (#8018)

Add variant of get-difficulty for full effort lemmas

[Arrays] Fix response for `store` chains (#8015)

When rewriting applying the rule store(store(a,i,v),i,w) ---> store(a,i,w), the arrays rewriter would return REWRITE_DONE. However,
this is incorrect if there are three or more nested stores of that kind
or the rewrite store(a,i,select(a,i)) ---> a applies to the result.
This commit fixes the response to always be REWRITE_AGAIN.

Add bag.filter operator (#8006)

Consider RANs in variable ordering (#7964)

The variable ordering in the arithmetic normal form should also consider real algebraic numbers. This PR also adds new comparators (essentially doing the same) in the rewriter that will replace the normal form utility classes.

Add utilities for flattening nodes (#7961)

This PR adds new utilities for flattening nodes and checking whether they can be flattened. They replace the custom implementation we used in the arithmetic rewriter.

Fix memory leak in quantifier info (#8005)

Fixes #8001. One of the maps in `QuantInfo` was containing
heap-allocated objects that were not being destroyed. This commit
changes the raw pointers to `std::unique_ptr<MatchGen>` to avoid the
memory leak.

Rename docs-releases to docs (#7999)

This renames the repository URL where documentation for releases is stored. It now lives at https://cvc5.github.io/docs/

Start post-release for 0.0.7

Bump version to 0.0.7

Try a bit harder on the EQ_NCTN rewrite rule (#7998)

This makes a small change to the sequence rewriter to work a bit harder
on one of the rewrite rule. This fixes some performance issues we've
observed.

Signed-off-by: Bruno Dutertre <dutebrun@amazon.com>

Fix docs upload once again (#7997)

This PR finally sorts out the ambiguity of different commits from PRs, tags and regular branches (fingers crossed).

[Rewrite Synthesis] Fix args for non-chaining ops (#7996)

Fixes https://github.com/cvc5/cvc5-projects/issues/445. Fixes
https://github.com/cvc5/cvc5-projects/issues/446. The issue is related
to the preprocessing pass for doing rewrite rule synthesis based on the
input. It was removing duplicate arguments from both chaining operators
and non-chaining operators when constructing the corresponding
datatypes. In the case of non-chaining operators, it could happen that
the constructor of the datatype did not have the correct number of
arguments for a given kind if there was a term where multiple arguments
were the same. This commit fixes the issue by doing the duplicate
elimination only for chaining operators.

Document substitute in API (#7904)

Update AUTHORS und copyright of docs configuration. (#7994)

Properly recognize whether the current commit is a tag (#7989)

This actually fixes what #7901 tried: when uploading the documentation, we need to figure out whether it was a tag and we should upload as a release as well.
Furthermore it fixes how we setup the deploy keys.

Initial refactoring of conflict-based instantiation (#7380)

This done an initial pass at refactoring conflict-based instantiation (the code has been largely unchanged since it was written in early 2014). This code is a bottleneck on some Facebook benchmarks and needs revisiting.

This changes the style so the parent modules are made data members instead of passed to methods. Otherwise, it changes int -> size_t wherever applicable, although int is often used to denote possibly valid indices where -1 means invalid.

It updates to use range-based for loops and mostly organizes the order of data members in classes to meet style guidelines.

Followup PRs will make more significant refactoring, e.g. to split the classes into multiple utilities.

Add Card solver to bags (#7986)

This PR avoids reducing bag.card terms with quantifiers unless it is needed.
It does so by building a cardinality graph for bags and adds appropriate constraints on internal nodes in the graph and min size constraints for the leaves.
This works for many of the benchmarks where each internal node has a single set of children.
Reduction lemmas are only generated when there are multiple sets of children.
Cardinality for bag.difference_remove and bag.duplicate_removal is not supported and would handled in future PR

More fixes and improvements for query generator (#7988)

Includes proper printing of dumped benchmarks.

Add output -o post-asserts (#7987)

This is equivalent to -t assertions::post-everything.

Start post-release for 0.0.6

Bump version to 0.0.6

Send `nth(unit(...), ...)` terms to array solver (#7983)

This commit changes our policy of which terms we send to the array core
solver. Previously, we were not sending nth terms that
were applied to unit sequences. This was incorrect, because for example
the split STRINGS_ARRAY_EQ_SPLIT has to be applied to nth of units,
too, to guarantee model soundness: For example, if we have a disequality
nth(t1, i) != nth(unit(v), i), then we have to reason about the
(dis)equality of t1 and unit(v), because of the UF for the
out-of-bounds case of nth (i.e., we have to reason that Uf(t1, i) != Uf(unit(v), i), which requires t1 != unit(v)). Splitting on t1 = unit(v) is done by STRINGS_ARRAY_EQ_SPLIT.

Fixes and improvements to sygus satisfiable query generation (#7980)

Fixes issues related to the use of partial functions. Also ensures we avoid duplicate queries.

[Strings] Avoid trivial explanation (#7982)

The `STRINGS_N_UNIFY` inference could produce trivial explanations. For
example, if both `x` and `y` were of kind `seq.unit`, then the
explanation was `(= 1 1)`. This lead to issues when checking proofs.

[Strings] Remove redundant call to rewriter (#7978)

The term being rewritten was already rewritten a couple of lines above.

[FP] Fix unused variable warning (#7977)

Disable regression if poly is not available (#7981)

This regression fails if poly is not available.

Always compile RANs (#7979)

This PR makes sure that we always compile with real algebraic numbers, following #7976.

Use proper RAN nodes for nl model (#7939)

This PR finally uses proper RealAlgebraicNumber (wrapped in nodes) to represent nonlinear model values. This simplifies the implementation of getEqualityStatus, and should make theory combination much more robust.
Also, we reintroduce the possibility to have getEqualityStatus return unknown, though this should only happen in the presence of witness terms.

Refactor how arith rewriting checks for mult-by-zero (#7962)

This adds an explicit check for a zero factor in the post rewriter for multiplication.

Enable dump tester. (#7884)

This PR enables the dump tester, a parse-print-parse test for cvc5, on CI. It also includes some changes that reduce the number of regressions that fail with this tester.

Have RAN fall back to RANs (#7976)

Right now, the RealAlgebraicNumber can not be used if libpoly is not available. This makes using it in the arithmetic rewriter incredibly awkward. This PR makes it fall back to a wrapper around Rational if libpoly is disabled, making its usage way easier.

Ref count nodes in trigger trie (#7972)

Fixes cvc5/cvc5-projects#437.

Fix trivial explantions in sequences array solver (#7973)

Also tightens the explanation slightly, we were previously adding a spurious equality to the representative, instead of the base of the normal form.

Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)

This commit updates the inferences in the sequences array solver to more
closely resemble the current rules in the paper. Concretely, it adds an
implementation of the `Update-Bound` rule and it fixes the `Nth-Update`
rule to take into account all three branches in the conclusion of the
rule.

Co-authored-by: Yoni Zohar <yoni206@gmail.com>

Fix proofs for trivial cases of datatypes tester merge (#7969)

Fixes cvc5/cvc5-projects#433.

Also ensures we don't add (= t t) as part of a reported conflict.

Refactor abs rewriting (#7935)

This PR refactors rewriting for ABS to also support real algebraic number. We also generalize the ABS operator to real arguments in general, instead of integer arguments.

Fix CI build for macOS (#7970)

The macOS CI could not find the Cython executable anymore for some reason. This commit fixes the issue.

Add rewrites for `seq.update`/`seq.nth` (#7966)

This commit adds rewrites for `seq.update` and `seq.nth`. It adds a
rewrite to check if an update is out of bounds and it adds rewrites to
evaluate these operators using `stripSymbolicLength()`. This allows us
for example to evaluate updates on concatenations of non-constant
`seq.unit`s.

Fix a subtle issue with double negations in coverings proof (#7967)

When the coverings solver finds a conflict that consists only of a single negated assertion, the way we constructed the lemma would silently drop the double negation. While this is not a problem by itself, the generated proof is out of sync then.
This PR makes sure the double negation stays in place and is only removed by rewriting in the core lemma processing.
Fixes cvc5/cvc5-projects#430.

Make tracing for arithmetic rewriter more consistent and useful (#7960)

Tracing in the arithmetic rewriter was very inconsistent and oftentimes not particularly helpful. This adds a general trace showing all top-level calls to the arithmetic rewriter.

Update to latest libpoly version (#7963)

The latest libpoly version has a fix for the conversion of algebraic numbers to rationals. We need this in our arithmetic rewriter to properly simplify real algebraic numbers to rationals.

Distinguish purification types for strings proof reconstruction (#7521)

This improves the success rate for strings proof reconstruction for context-dependent simplifications.

It also makes a minor modification to how EXTF inferences work. As a special case, A => B becomes A ^ ~B => false when B is already equal to false. This PR removes this behavior for the sake of consistency. (This could be explored as a more general strategy for turning facts to conflicts from any source if necessary).

The strings solver applies context-dependent simplification in various ways. This ensures that the proof reconstruction is faithful for cases of congruence + rewriting instead of substitution+rewriting, which the inferences STRINGS_EXTF and STRINGS_EXTF_N rely on.

This fixes 11 cases where proof reconstruction fails for string theory lemmas on Amazon benchmarks.

Some random documentation issues (#7921)

This PR fixes a few issues in the documentation, mostly about examples that were not included where they should be.

[API] Add missing arity check (#7905)

Fixes #7894. The API was not performing an arity check for associative
operators with less than two children. This commit adds the missing
check.

Fix CMake script for static, auto-download, cln configuration (#7957)

The script was previously creating a 'CLN_STATIC_LIBRARIES' variable that
wasn't known about elsewhere in the code and caused issues when the Makefiles
depended on a CLN_LIBRARIES variable. Instead, the static libraries should just
go into CLN_LIBRARIES as normal.

This only seems to have affected the case where cln is set to auto-download and
the build is static.

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

Print original form for substitutions and learned literals (#7959)

Refactor options related to rewriting and symmetry breaking in sygus (#7949)

Note this also corrects a few inconsistencies in how the rewriter is invoked in fast / variable agnostic enumeration.

Notably, fast enumeration now leverages the term datatype sygus for rewriting, meaning it can evaluate recursive functions for enumerated terms.

[Strings] Fix rewriter for `re.loop` (#7956)

Fixes cvc5/cvc5-projects#409. Our
strings/sequences rewriter was applying rewrites for re.loop in the
wrong order. As a result, it rewrote ((_ re.loop 2 1) re.all) to
re.all instead of re.none as required by the SMT-LIB standard when
the lower bound is greater than the upper bound. This commit changes the
order s.t. the bounds check happens first.

Change how RANs are printed (#7955)

This PR adds real algebraic number as a special case in the smt2 printer.

Add inverse inference for update-over-concat (#7954)

This adds an inference that applies when an atomic update term becomes equal to a concatenation term.

This fixes bogus models discovered when writing the model soundness proof for the sequences array solver.

Improve names for sygus enumeration option (#7945)

Also deletes the unused (naive) basic enumerator.

Clean enumerative instantiation options (#7947)

--full-saturate-quant is kept as a generic option, and implies --enum-inst.

Implement -o subs to show learned top-level substitutions (#7944)

Also adds substitutions as part of the output of -o learned-lits for completeness.

Rename python APIs (#7950)

Rename python APIs to "base" and "pythonic"

Preprare central model building for RANs (#7951)

This PR uses a new utility isEvaluationResult() instead of isConst() within the core model building. This prepares model building for model values that are not constants (in the sense of isConst()) but still constant-lilke values, like real algebraic numbers.

refactor div rewriter, add support for ran (#7941)

This extends the rewriter for division to also support real algebraic numbers.

Fix learned rewrite pass for non-real equalties (#7936)

Fixes #7918.

Add operator<<(RewriteStatus) (#7952)

Adds a streaming operator for RewriteStatus. I found it helpful while refactoring / debugging the rewriter.

Weaken assertion in relevance manager (#7943)

Fixes #7937.

Refactor arithmetic pre-rewriter for multiplication (#7930)

This PR refactors the pre-rewrite stage for multiplication.

Add support for RANs in rewriter for `MULT` (#7940)

This PR refactors the post rewriter for multiplication. It now supports real algebraic numbers and tries a bit harder to avoid the overhead of the normal form abstraction.

Add RAN support in UMINUS rewriter (#7933)

This adds rewriting for UMINUS of real algebraic numbers

Add arithmetic rewriter for RAN (#7929)

This adds a rewriter for real arithmetic constants, possibly rewriting them to a rational.

Fix bug in evaluator for division by zero (#7942)

Fixes #7917.

Unify abstract values and uninterpreted constants (#7424)

This commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a declare-const command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in NodeManager::mkAbstractValue())
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.

This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.

Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an @ are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.

Refactor post rewriter for addition (#7931)

This makes the post rewriter for addition aware of real algebraic numbers. Also, it tries a bit harder to avoid the normal_form utilities if only constants are present.

Fix check whether we have a tag (#7901)

This PR fixes a subtle issue with the docs upload for releases. While most of the context of the original action is passed into the docs upload action, the git ref changes from refs/tags/... to refs/heads/.... However, we still can check the current ref against the head_branch of the original workflow.

Add -o learned-lits to output learned literals (#7934)

Prints both literals learned during preprocessing, and during search.

This feature was recently requested by Cetora.

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.