Make model builder robust to multiple value-like terms in the same equivalence class (#8150)

This changes our policy on handling when two value-like terms are in the same equivalence class. We now give preference to the "base" model value, and either warn or throw a debug exception.

After f7675b2, we can have the situation where e.g. (seq.nth seq.empty 1) is in the same equivalence class as a constant, where (seq.nth seq.empty 1) is considered value-like, despite being unevaluatable. We now ensure that the constant is taken as the representative of the equivalence class, and not this term.

It also removes assignable terms from consideration when assigning values to equivalence classes. In particular, (seq.nth seq.empty 1) is skipped, so a warning is not even given when the above occurs.

Fixes #8148.

Improve error message for missing options include (#8154)

This PR improves the error message if one tries to use options whose header have not been included.

Make sine solver sound with respect to region boundaries (#8117)

Fixes the last benchmark on #7948.

Fixes a refutation soundness issue in the transcendental solver where a concavity region would be incorrectly assigned to a point if it was between the current model value of c*PI and its true value, where c in {-1, -1/2, 1/2, 1}.

We now only assign a concavity region if the model value of the argument lies within sound lower/upper bounds for the boundaries.

Notice that this means that points may be unassignable to a region if they lie inside the approximation interval for c*PI. An application of sin applied to an argument whose model value is that point cannot be refined.

A followup PR will address termination issues where the Taylor degree is incremented even when no function can be refined.

Check for free variables in several SolverEngine calls (#8130)

Fixes the nightlies due to ensuring that a unit test fails in production (it was failing only in debug).

Fixes #8127.

Get rid of some static objects in arithmetic theory (#8146)

This PR tackles cvc5/cvc5-projects#17 by removing static variables or making them constexpr.
Most static variables are either compile-time constants (we make them static constexpr) or used to count how often a function is called for debug output (we remove these).

Make uninterpreted sort owner non-static (#8144)

This eliminates the static member `s_uninterpretedSortOwner` from Theory which seems to be the cause of several issues related to the array solver in incremental mode, and with check-unsat-cores. This is moved to a data member of Env.  This eliminates a static access to `theoryOfMode` from within theoryOf calls.

Note that static calls to `Theory::theoryOf` or `Theory::isLeafOf` now assume type-based theoryOf mode as a default argument. Thus, the preferred method for determining theoryOf types and terms is through `Env` now.

This fixes issues with the array solver in incremental mode.

The root issue is that spawning subsolvers (e.g. for check-unsat-core) can overwrite `s_uninterpretedSortOwner`. This means that a second call to `check-sat` (which does not reinitialize set_defaults) will use the *overwrtten* setting, which can be different from what was used for the first check-sat.  In particular, for #5720, the uninterpreted sort owner changes from ARRAYS to UF at the 2nd call, and the array theory solver fails to send an extensionality lemma.

This commit also simplifies `Theory::theoryOf` slightly.

Fixes https://github.com/cvc5/cvc5-wishues/issues/52.
Fixes https://github.com/cvc5/cvc5/issues/5720.
Fixes https://github.com/cvc5/cvc5/issues/6276 .
Fixes https://github.com/cvc5/cvc5/issues/5836.

Add regression for some fixed array issues (#8145)

Found while checking whether the latest fix solves array issues, these were already resolved.
Fixes #4414.
Fixes #4546.

Add two regressions related to RAN models (#8142)

This PR adds regressions for two issues that relate to the previously incomplete handling of real algebraic models.
The issue has been resolved by properly integrating real algebraic numbers as model values and in the rewriter.
Fixes #6547. Fixes #6619.

Allow elimination of unevaluated terms by default (#8136)

Fixes #8118.

Further relax what is considered a value in the model (#8095)

Fixes #8094.

This makes it so that "value-like" terms can appear as subterms in other terms that are then subsequently also considered values. For example (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is now considered a value.

This also changes the default option for when to use witness terms for strings in models, based on some user feedback.

Do not insist that entries for UF are constant in FMF (#8140)

Fixes #8096.

Eliminate match from LFSC proofs (#8090)

The smt 2.6 term match is very hard to represent in LFSC, this eliminates it in favor of the ITE term that it is syntax sugar for. Like other aspects of the LFSC conversion, this is part of the trusted core.

This avoids internal type errors in the LFSC node converter.

Remove long obsolete unsafe interrupt exception (#8139)

We used to use UnsafeInterruptException to deal with resource outs in the resource manager: when resources were exhausted, we would throw this exception that was catched in the core solver engine. This had the significant downside of leaving the solver in a potentially inconsistent state. We moved away from using it long ago in #4732.
What remained was the UnsafeInterruptException class itself and a bunch of places that still catch this exception that is no longer thrown anywhere.

This PR removes this class for good.

Option exception when incompatible with proofs (#8064)

This changes set defaults so that it doesn't silently disable proofs or unsat cores.

Fixes cvc5/cvc5-projects#440.

Fix creation of RAN from non-dyadic rational (#8138)

Libpoly only allows to create real algebraic numbers from dyadic rationals. For non-dyadic rationals, we need to create a polynomials and create it the general way. Libpoly requires all defining polynomials to be primitive, in particular the leading coefficient must be positive. We would always have it negative, which only becomes a problem if libpoly has assertions enabled, though.

Fixes #8126.

Fix icp candidate parsing (#8137)

For constraints of the form c * x ~ poly(x) where c != 1 we would sometimes forget to take the inverse of c when parsing the assertion to the internal representation of the ICP solver. This PR fixes this issue, and does a few more changes:

--nl-icp is really not well-tested and disabled by default. We make it an expert option.
we no longer issue the propagation lemmas if we already found a conflict
the nl-icp trace was heavily polluted by output from the interval utils, which are now moved to a new nl-icp-debug trace
Fixes #8135.

Properly sanatize user names in LFSC (#8080)

Previously, we would get LFSC proof checking failures if we were using an identifier that was valid in SMT-LIB but not LFSC.

Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>

[Rewriter] Do not attempt to rewrite constants (#8061)

This commit changes our rewriter policy to not attempt to rewrite nodes
with no children.

Fix pruning of covering intervals in proofs (#8084)

We need to mirror the pruning of intervals in the coverings solver in the corresponding proof. To match the proof nodes with the coverings-internal intervals, we use ids, where non-interval nodes have the id zero. In this process, we had three separate issues that never showed up because we don't have a proof checker for CAD proofs:

we did not check for zeros, pruning all non-interval nodes
we ran the pruning on the direct children of a CAD_RECURSIVE proof step, which are SCOPE nodes that don't have ids
iterating over and then removing children was done by a custom but faulty reimplementation of std::remove_if
Thus, we now

never prune zero nodes,
prune based on the (single) child node, if we are checking a SCOPE node, and
simply use std::remove_if.

Refactor multiplication in arithmetic rewriter (#7965)

This PR refactors the rewriting of multiplication. Most importantly, we explicitly deal with distributivity of addition and multiplication explicitly using the new utilities.

Fix issue in datatypes care graph computation involving subtyping (#8125)

The datatypes care graph was incorrectly computed for constructors taking `Real` arguments, due to subtyping.

This fixes the term index to cache on the *return* type for constructors, not the argument types.  Caching based on argument types was incorrect even for non-parametric datatypes with arguments that have subtyping.

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

This also does minor cleanup and additions done while debugging the issue.

Support some cases of isConst for regular expressions (#8114)

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

Having `isConst` return true is required for some rare use cases of regular expressions, e.g. rewrite rule synthesis involving regular expression variables.

Remove refineConflicts option (#8129)

Was introduced in 8a0c056.

Fixes #8119.

Change inference scheme in transcendentals to rewrite rule (#8115)

Avoids introducing new sine terms.

Relax what is generated in the model from NL (#8113)

This makes it so that we don't assign concrete values to equivalence classes with transcendental functions.

It also removes some unused infrastructure.

[proofs] [dot] Enable DAG and tree printing with dot files (#8107)

Add a proof option that allows DAG and tree print format when using dot files.

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

Fixes and additions for LFSC signatures (#8120)

Fixes a critical issue in the re intersection rule, where a null terminator was missed.

Also adds a sketch of the theory signature for floating points.

Add unit test for fixed issue with get-difficulty (#8060)

Fixed by recent updates to get-difficulty.

Fixes cvc5/cvc5-projects#434.

Throw option exceptions when combining input conversion preprocessing with sygus (#8059)

Fixes cvc5/cvc5-projects#436.

Add well formed term check to solver engine (#8056)

Fixes cvc5/cvc5-projects#413.

Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)

This changes the `STRINGS_ARRAY_UPDATE_BOUND` inference to explicitly
include the disequality between the term before and after the update if
the update has an effect. This is an optimization that prevents us from
splitting on that (dis-)equality later on.

Make spurious assertion into warning (#8051)

Fixes cvc5/cvc5-projects#401.

Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)

Our `STRINGS_ARRAY_NTH_UPDATE` inference was missing an explanation that
establishes the relation between the update and the nth term. On the
current set of benchmarks, this does not cause an issue, but there
should be cases where it does. The commit also changes the array core solver
to take better advantage of `d_indexMap`.

Introduce skolem function to make transcendental function purification consistent (#8116)

Previously, we could introduce multiple purifications for the same sin term.

Missing ids for arith conflicts (#8108)

Fixes #8097.

Remove some irrelevant node kinds from the model (#8110)

There are several kinds of nodes that are currently sent to the model that don't need to be. Furthermore, we require not sending some of these due to the new invariants in #8095.

[proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)

Instead of printing "trust" in the case of a simplification rule that cannot be translated to an Alethe simplify rule print "all_simplify". This also replaces the heuristic in THEORY_REWRITE to determine which simplify rule is needed.

[proofs] Consolidate multiple substitutions to single AND proof in trust substitution map (#8109)

This ensures that a common proof node is used for a substitution instead of copying its children. This optimization had been noted in a comment but had not yet been enabled.

This should speed up proof reconstruction for substitutions.

[proofs] Make cache (optionally) persistent in lazy CD proof (#8104)

Should address severe performance issues in some use cases of proofs.

Only consider relevant terms in the array-inspired sequence solver (#8105)

Avoids segfault in model construction due to asking for the value of irrelevant (non-shared) term.

Support `try` and `all` reconstruction modes. (#8098)

This PR adds a simple procedure to quickly reconstruct Sygus terms that are already in the grammar. This new procedure fails if the terms are not in the grammar.

Ensure proofs are fully disabled when incompatible (#8092)

Was causing regression failures on proof-new when proofs + sygus are enabled. We now force proofs to be disabled.

Fix for lambda-to-array constant conversion for unused arguments (#8082)

Fixes #4434.

Fix type check of `seq.nth` (#8093)

The code for type checking `seq.nth` was trying to retrieve the sequence
element type before ensuring that the type of the first argument was a
sequence, which lead to assertion failures. This commit reorders the
checks to avoid this issue.

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.