Generalize LFSC string signature to sequences (#8220)

[proofs] Alethe: Removed Steps that are Double-Printed (#7754)

This PR fixes that some steps are printed more than once. To this end, it deletes that the reference maps in which the steps are stored are constant and optimizes where the steps are added to the maps. It also stores ProofNodes instead of Nodes in the maps.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Throw logic exception if a transcendental function is encountered when nl-ext is not full (#8212)

Fixes cvc5/cvc5-projects#376.

Add regression for fixed issue (#8213)

Fixes #5815.

This adds the regression, in theory I still think it is possible for the assertion to fail, but I don't think it is worth pursuing right now.

Improve error for higher-order logic (#8207)

Makes the error more informative when a higher-order function variable is encountered.
Fixes cvc5/cvc5-projects#450.

cmake: Fix murxla setup. (#8215)

Integrate pythonic api (#8131)

We decided we want to ship the pythonic API together with our base python API.
This PR adds a new target cvc5_python_api that first builds the base python API and then copies the pythonic API over. Furthermore we now use the cvc5.pythonic module to generate the corresponding documentation.

Fix rewriting of mixed-integer atoms (#8214)

The sixth input from #8159 revealed a subtle issue in our rewriting of arithmetic atoms. As real and integer atoms are rewritten differently, we check this and then call different functions. However, we check this on the original input, although this property can change during rewriting, e.g., when the only real variable vanishes.
This PR fixes this issue.

Fix issue with dropping non-reduced sine terms (#8211)

Fixes #8208.

A spurious "break" was leftover from when this code was a loop, this meant when the first reduced term was encountered, it ignored the remainder.

Fix models involving cardinality of sets of finite type (#8206)

Was caused by a flag not being reset, thus making it so that subsequent models did not use exclusion sets.

Fixes #5402. (Fixes the last benchmark on that issue, the first two are fixed by #8201).

Always purify universe from set minus (#8201)

This fixes a bug in our handling of set cardinality + set universe (also used for set complement).

The bug was caused by using the rewritten form of terms to compute siblings in the cardinality graph. This is problematic for
(set.minus set.universe t) whose sibling was computed to be rewrite( (set.inter set.universe t) ) = t.

To avoid the issue, we now purify the argument of set.minus to avoid this behavior.

Fixes #5400.
Fixes the first benchmark on #5402.

This also eliminates a spurious lemma schema for set universe that was leftover from handling set subtyping.

Eliminate CDHashMap::insertAtContextLevelZero (#8173)

This method unnecessarily complicates the usage of CDHashMap. It had one usage in the current code, for dealing with global declarations. However, this was an entirely artificial use case, as one should properly manage scopes when this option is true (i.e. global-declarations simply disables user-level scoping in the symbol table).

It also simplifies the symbol table so that it doesn't automatically push a global outermost scope. Instead, this scope is pushed when the logic is declared, so that background symbols are correctly added at level 0.

Fixes #4767.

Fix incorrect assertion in prop engine proofs (#8204)

Leftover from when unsat cores mode was tied to proof mode.

Fixes cvc5/cvc5-projects#462.

Clean usage of options in regressions (#8190)

We now support tester annotations, thus it is best practice not to use check-unsat-cores or check-models explicitly in the regressions.

This changes regressions to not use these options, where these options are either:

removed entirely (the benchmark was fixed in the meantime)
changed to -q (the benchmark succeeds with a warning)
changed to produce- instead of check- if the option on the benchmark is required to ensure a configuration of models/unsat-cores is run. This is done for unsat-cores on sat benchmarks and models on unsat benchmarks.
replaced by DISABLE-TESTER: model.
one spurious regression is deleted, which was identical to another + check-models.
It also makes some fixes to enable more benchmarks succeed with check-models, and adds a warning when fmf-fun is combined with check-model.

Improve error message when not using strings-exp (#8203)

Fixes #6005.

Also improves smt2 printing of sequences so that we print the compliant kinds, which is work towards cvc5/cvc5-wishues#106.

Move libpoly <-> CoCoA conversion to new utility (#8199)

This PR factors the conversion between libpoly and CoCoA out of the LazardEvaluation class into a new utility. The goal is to make it reusable for other applications of CoCoA within cvc5, for example to replace the (rather naive) equality substitution utility by a new simplification technique based on CoCoAs Gröbner bases. This PR merely moves code around and should not actually change anything.

Refactor rewriting of arithmetic division (#8195)

This PR does minor refactoring of how we rewrite division. Also, it moves some functions around to reconcile the order in header and source file.

Add utility to access how to print floating point (#8141)

This makes the code for printing a floating point based on its BV components accessible as a utility.

This is required for proper printing of FP constants in LFSC.

Make blockModelValues robust to non-closed enumerable types (#8055)

Fixes cvc5/cvc5-projects#420.

Also fixes the trivial case where there is nothing to block, in which case we should add false (via mkOr) not true.

Add regressions for fixed issues (#8202)

Fixes #4463.
Fixes cvc5/cvc5-projects#403.

Prune spurious roots in lazard evaluation of coverings solver (#8200)

This PR fixes a subtle issue in the Lazard evaluation used in the coverings solver if --nl-cov-lift=lazard is used.
When isolating real roots (over a partial assignment that contains real algebraic number), the core root solver may find roots that are spurious, i.e., they are not actually roots of the input polynomial. This is due to the way how the multivariate polynomial is "partially evaluated" before calling the univariate real root isolation.
When using the libpoly real root isolation, this is all done internally. For the Lazard evaluation, however, we explicitly call the libpoly real root isolation on a univariate polynomial that already has these spurious roots, hence we need to remove them ourselves.

While debugging this issue, another weird oversight was detected (and fixed): for some reason we expected the vanishing factor (after factoring the defining polynomial when constructing the next field extension) to only have two term. There is no reason for this restriction, and the code below works just fine.

Add standard theories to documentation (#8192)

This PR adds the standardized theories to our theories overview.

Fix issue involving dropped purification lemmas for transcendental functions (#8198)

Fixes #4693.
Fixes #8181 (which now times out).

The issue was caused by purification lemmas being dropped, often in incremental mode. This meant that we were replacing sin(t) by sin(k) when checking models, but not having any information about sin(k).

We now are more robust and send the purification lemmas for transcendental functions based on checking whether it is necessary to do so.

Do not use sygus evaluation functions in sygus-inst (#8185)

This simplification was realized while we were writing the paper.

This should avoid spurious check-model failures when using sygus-inst.

Disable regression (#8191)

Benchmark is "unknown" on some builds. We don't have a strong reason why we will always say "sat" for this benchmark.

Fixes one of the issues in the nightlies.

[BV] Fix rewriter policy for `bvneg` (#8196)

Our rewriter was returning `REWRITE_DONE` prematurely for `bvneg`. This
commit makes the status returned more conservative.

Fix lambda lifting + proofs (#8152)

Was leading to eager proof checking failures on proof-new.

Remove unused data members from `TheoryArrays` (#8197)

Rename cad to coverings (#8187)

The nonlinear subsolver that implements cylindrical algebraic coverings is still called cad in many places, which really was a misnomer from the beginning. This PR renames it everywhere.

[Seq/Model] Do not enumerate elements of constants (#8179)

Fixes #8133. In the input from the issue, the string solver was
assigning a skeleton `(seq.unit smvX)` to a constant of sort `(Seq (Seq
Int))`. This constant was asserted to be different from `(seq.unit (as
seq.empty (Seq Int)))`. However, the `TheoryModelBuilder` was assigning
`smvX` the value `(as seq.empty (Seq Int))`, because `(as seq.empty (Seq
Int))` was not being registered with the equality engine. This is
because elements of constant sequences are not considered children, but
are a data member of the `Sequence` class. The commit updates
`TheoryStrings::collectModelInfoType()` to also register elements of
sequence constants with the equality engine.

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.