Add assertion to require inference ids (#8091)

Use witness terms to represent values for large strings in models (#8089)

This makes it so that we don't prematurely fail on some Facebook benchmarks.

bv: Add --tlimit-per support for CryptoMiniSat. (#8086)

bv: Add --tlimit-per support for CaDiCaL. (#8085)

This commit adds --tlimit-per support for CaDiCaL via CaDiCaL's Terminator class.

Fixes #8049

Fix handling of `LogicException` during solving (#8000)

Fixes #7974. This commit fixes our handling of LogicExceptions during solving. Instead of leaving MiniSat in a bad state, it catches the exception, resets the decision trail, prints the error message, and then returns unknown.

[Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)

When rewriting (seq.nth s n) where both terms are constants, cvc5 was
blindly converting the n to a uint32_t, which caused issues when n
was greater than the largest value that can be represented by a 32-bit
integer. This commit introduces a corresponding check and does not
perform the rewrite for large n.

Add addition utilities for the arithmetic rewriter (#8013)

This PR adds methods to deal with sums in the arithmetic rewriter. Sums are stored as std::map<Node,RealAlgebraicNumber> (see the code for some reasoning), and we implement adding terms to sums, collecting sums into nodes and distributing a multiplication over nested sums.

Simplify formalism of introduced arithmetic skolems (#8073)

This ensures that all skolems introduced by arithmetic have concrete terms as witnesses. This avoids introducing witness terms.

This PR is important for ensuring that the "original form" of terms does not contain introduced free variables. This means that certain features (quantifier elimination, learned literals) are useful to the user. This was requested by Certora.

This also will improve proof reconstruction for extensions of non-linear arithmetic.

It also ensures that we share skolems in some cases, e.g. we use the same skolem for eliminating (div x y) and (mod x y).

Distinguish proof mode from unsat core mode (#8062)

Previously, we were making unsat cores mode the source of our configuration for unsat cores and proofs at the same time.

This led to a lot of unnecessary complication in the logic, and would allow bugs e.g. if produce-difficulty but not produce-unsat-cores was enabled.

Fixes cvc5/cvc5-projects#406.

Fix LFSC node conversion for non-shared selectors (#8078)

Print more commonly used murxla commands (#8046)

Given that murxla requires multiple invocations with different arguments for a typical workflow, I found it very helpful to have them recalled whenever I build it.

Always produce assertions (#8041)

There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option.

Make witness form visited ref counted (#8081)

Fixes #8079.

Generalize LFSC concat unify for splitting constants (#8077)

Was causing LFSC proof failures on ~5 SMT-LIB strings benchmarks.

Add user documentation for resource limits (#8058)

Though we regularly get questions about how resource limits work, they were entirely undocumented. This PR adds some general explanation to the user docs.

Fix unsoundness in IAND solver (#8053)

Fixes #5461, fixes #8063. The initial lemma schema was assuming arguments were in bounds.

This also modifies the solver so that we throw logic exceptions when encountering iand or transcendentals.

Allow non-value model values (#8076)

We previously required model values to be "values", i.e., constants or constant-like stuff like real algebraic numbers or lambdas. This is an inherent problem for, e.g, transcendental models: the simplest model for a transcendental problem may legitimately be 3 * PI or PI + exp(3). This PR removes this restriction, only requiring that values are rewritten.

Improve combination of NRA and transcendentals (#8075)

This PR tackles two issues when combining transcendental reasoning with nonlinear arithmetic.
Firstly, the NRAT logic would inadvertently have transcendental reasoning disabled because we only checked for integers. This simply adds an additional check at the end to enforce transcendental reasoning if necessary.
Secondly, we assert that we never add multiple substitutions for the same variable. This weakens the check to allow add the very same substitution multiple times.
Fixes #7984.

[BV] Fix response of `RewriteConcat` (#8074)

RewriteConcat was returning REWRITE_DONE, but it could happen that
applying ExtractWhole was removing an extract around another
concat that could then be flattened (see added unit test for an
example). This commit makes the response more conservative and only
returns REWRITE_DONE if the node did not change.

Fix indexof_re reduction (#8065)

Fixes https://github.com/cvc5/cvc5/issues/6654.

Note that this regression now answers unknown with `--ext-rewrite-quant`; the regression without this option is added.

Correct search location for CLN libs (#8070)

On (e.g.,) openSUSE, the default install path (via CMake) for libraries is lib64 and not lib. However, FindCLN.cmake is hard-coded to only search in lib.

This PR corrects FindCLN.cmake such that the build looks in ${CMAKE_INSTALL_LIBDIR} instead.

Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com

[Seq] Check types for split on indices (#8066)

We applied `STRINGS_ARRAY_EQ_SPLIT` to pairs of `seq.nth` terms of
different types. This lead to assertion (in debug) and performance
problems (in production). The commit adds a type check.

Fix another rewrite involving iand (#8054)

Fixes #8052.

[Rewriter] Always rewrite again when kind changes (#8007)

Fixes cvc5/cvc5-projects#438. The rewriter
returned REWRITE_DONE prematurely when rewriting operators such as
bvand in certain cases. If only a single term was left after removing
duplicates from a bvand, the kind of the current node would change and
another pre-rewrite could apply, but the rewriter still returned
REWRITE_DONE. After adding an assertion in the rewriter that checks
that REWRITE_DONE implies that no other pre-rewrite applies, it was
discovered that not only the bit-vector rewriter has this issue, but
other rewriters, e.g., the Boolean rewriter, as well. This commit
changes our semantics for REWRITE_DONE to mean that no other rewrite
applies provided that the kind did not change. This makes it easier for
developers to decide when to return REWRITE_DONE, because it only
requires reasoning about rewrites that apply to a single kind.

Standardizing notifications for setting options in set_defaults (#8057)

FP: Rename tester kinds. (#8037)

This renames FP tester kinds for consistency:
FLOATINGPOINT_ISINF -> FLOATINGPOINT_IS_INF
FLOATINGPOINT_ISN -> FLOATINGPOINT_IS_NORMAL
FLOATINGPOINT_ISNAN -> FLOATINGPOINT_IS_NAN
FLOATINGPOINT_ISNEG -> FLOATINGPOINT_IS_NEG
FLOATINGPOINT_ISPOS -> FLOATINGPOINT_IS_POS
FLOATINGPOINT_ISZ -> FLOATINGPOINT_IS_ZERO

Use Add instead of Plus (#8043)

This fixes the current documentation builds for the pythonic API

Simplify handling of disequalities in strings (#8047)

This simplifies how string disequalities are handled, and fixes a caching bug in our implementation of extensionality.

The simplifications are two-fold:
- We track disequalities via assertions, not via an equality engine callback
- We process disequalities by iterating on the disequality list, not via iterating on pairs of equivalence classes

Extensionality is fixed by not *explaining* disequalities, which leads to being out of sync with the cache (as the disequality could have a different explanation in another SAT context).

This fixes the last known issues with `--seq-array=X`.

Improve theory combination over real algebraic models (#8045)

Though we support real algebraic models now for theory combination, cvc5/cvc5-projects#451 uncovered the possibility to assert if an equality was in fact not equal during theory combination and the difference was real algebraic.
This PR fixes this issue by adding the proper check.
Fixes cvc5/cvc5-projects#451.

Eliminate even more static uses of rewrite (#8044)

Test proof granularity theory-rewrite by default (#8038)

Recently we updated proof granularity to be macro by default, but we should test theory-rewrite granularity in our regressions.

Replace a some more static options (#8042)

We now have access to the options in a few more places in quantifiers.

Eliminate more static uses of rewrite (#8040)

Add table.product operator (#8020)

Add miscellaneous missing theory definitions for LFSC (#8039)

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.