Refactor rewriting of arithmetic atoms (#8175)

This PR uses the new utilities for atom rewriting in the arithmetic rewriter.

Fix special casing for PI in model value (#8189)

PI should be considered a model value but not a "base" model value. This avoid spurious debug assertion failures, which are now treated as warnings. This makes a difference when another theory e.g. UF says that PI is currently equal to a constant value c. Since our lemma schemas are model-based, we may require building a spurious model where PI is c, and refine afterwards.

This also fixes a bug in our extended function rewriting which would mistakenly think that PI was reduced, and hence skip a full effort check if PI was the only extended function in the current context. This was previously causing a final model to be one where PI = 0.0.

Fixes #8183.

Preserve model values for exact sine points (#8188)

Fixes #8182.

Track names for witness terms in model (#8184)

This ensures that enough information is set to allow users to understand models with witness terms.

For example, for input:

(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (= (str.len x) 999999999999999999999999))
(assert (= (str.len y) 999999999999999999999999))
(assert (= z (str.++ x y)))
(check-sat)
we now get:

sat
(
(define-fun x () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ))
(define-fun y () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) ))
(define-fun z () String (str.++ (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ) (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) )))
)

Add two reduction schemas for sin terms (#8171)

This restores our reasoning for symmetry of sine, now on-demand and without introducing sin terms eagerly.

It also ensures that sin terms whose arguments fall exactly on boundary points are removed from consideration from the transcendental solver. This allows us to answer sat for inputs involving sin(k) when k = pi/2.

It also cleans the relationship of sine solver and transcendental state, and makes a small fix to the monotonicity of sin schema.

Remove broken/unused `--mmap` option (#8178)

Fixes #2705. This commit removes the broken and unused --mmap option.
Given that we are planning to change to a different parser at some
point, it is not worth attempting to fix the option.

Add scripts to build python wheels (#8132)

This adds a new set of scripts to build python wheels for cvc5. It includes

mk_wheel.py which builds the python wheel within an existing build folder
mk_build_dir.py which runs configure.sh and directs cmake to a custom python interpreter
mk_clean_wheel.sh which builds the python wheel in a clean environment (a python venv and a fresh build folder)
a dockerfile that slightly customizes manylinux2014 to our use case
a readme giving a highlevel overview of what we are doing

Refactor rewriting of arithmetic leafs (#8177)

Minor refactoring of how we rewrite arithmetic leaf nodes (constants, algebraic numbers and "variables").

Refactor rewriting of arithmetic addition (#8180)

This PR uses the new addition utilities to refactor rewriting of arithmetic addition. This properly handles real algebraic numbers now, eliminating a few more edge cases where the previous solution might allow for non-idempotent rewrites.

Consider PI to be a model value (#8176)

Fixes cvc5/cvc5-projects#460.

The special case is necessary due to the node representation of nullary operators, which uses variables internally to represent operators. The other nullary operators are not model values.

Syntax fixes for LFSC signature (#8172)

Add utilities to rewrite atoms for the arithmetic rewriter (#8014)

This PR adds utilities to rewrite atoms in the arithmetic rewriter. They retain compatibility with the current normal_form utility, but make the process more transparent so that changing the normal form in the future should be simpler.

Refactor rewriting of arithmetic negation and subtraction (#8170)

Slightly refactor negation and subtraction, get rid of utility functions.

Slightly refactor arithmetic rewriting for extended operators (#8169)

This PR mostly reorders the implementation to match the order in the header, and does a few very minor refactorings for the rewriters for transcendental functions, and the pow2 and iand operators.

Fix non-termination in quantifiers rewriter (#8165)

Caused by 2 rewrite steps (conditional splitting and extended rewriting) being inverses of each other when miniscoping is disabled.

Fixes the third benchmark on #8159.

Simplify and fix how purified terms are managed in the trancendental solver (#8167)

Simplification is leftover from the sine symmetry heuristic, now the mapping from terms to what purifies them is injective.
Also makes the mapping context-dependent.

It also ensures that we keep model values for purification arguments. Fixes #8160.

Fix dropped bounds on PI (#8164)

Fixes #8162.

In this example, we were failing to send the initial PI bound lemma, likely due to a conflict while this lemma was buffered.

This makes the PI refinement utility more robust by explicitly checking based on the model whether we need to refine PI.

Remove approximations infrastructure from model (#8166)

We now allow partial specifications. Recording approximations is arithmetic specific, and if necessary could be added as a post-processing analysis e.g. during check-model.

Remove spurious assertion involving constants for arguments to UF from FMF (#8168)

Fixes #8163.

Make quantifiers terminate if it detects a (duplicate) quantifier-free conflict (#8157)

Fixes #6859.

The benchmark is now unknown.

Add regression for fixed transcendental regression (#8155)

Fixes #7938.

Consolidate extended rewrite preprocessing modes (#8156)

[Python API] Add support for blocking models (#8134)

The methods for blocking models were missing in the Python API. This
commit adds the blockModel() and blockModelValues() methods as well
as the corresponding tests.

Ensure variables are constrained in model when equal to transcendental function apps (#8153)

Fixes #8147.

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.