Fix LFSC proof construction for concat clash of sequences (#8739)

Changes the internal proof calculus to require an explicit disequality between character constants for clashing sequences.

Makes it so that the disequality is expanded prior to proof post-processing, so that character clashing is properly expanded as it may require rewriting.

docs: Remove references to checkEntailed(). (#8789)

Generalize pto constraint tracking for multiple heaps in sep theory (#8768)

Fixes #8659.

Add getInterpolant with a grammar in the unit test for all language bindings (#8775)

Add getInterpolant with a grammar in the unit test for all language bindings

new test for resolved issue (#8784)

#8412 is now fixed on main. This PR adds a regression from that issue.
closes #8412 .

Last remaining fixes for eliminating subtyping (#8772)

Also fixes a debug failure for the nightlies.

This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples).

[proofs] Generalize handling of constants merged in equality engine (#8781)

Previously the reconstruction of EUF proofs was not considering a corner case from the equality engine where it infers that two constants are disequal from other equalities, but these other equalities all become of the form x = x at the time we are explaining this disquality. In this case the constant disequality is justified with MERGED_THROUGH_CONSTANTS rather than MERGED_THROUGH_TRANS as other disequalities.

Rename equality engine trace to print E-graph (#8780)

The current trace depends on `-t equality::internal`, which is pointless and
leads to confusion when one inevitably forgets this when checking which trace to
use to print the E-graph and the output does not contain it.

Eliminate the use of CAST_TO_REAL (#8759)

This simplifies the implementation of the API by not relying on CAST_TO_REAL. This was used as a way of manually marking integral reals as having real type.

Eliminate ops for parameterized type constructors (#8761)

We now preserve types when rewriting. This means that we no longer need to use operators that store the type of terms to construct in the cases of bags, sets, and sequences.

Make arith substitute its own utility (#8765)

Arithmetic substitutions behave differently in two ways:
(1) they traverse only symbols belonging to arithmetic
(2) they allow mixing Int/Real
This makes ArithSubs derive from the more general Subs class with these two behavior changes.

This is one of the last remaining non-trivial steps towards for eliminating TypeNode::isSubtypeOf.

Add heap-trail partitioning strategy, checks between partitions, and cubes with zero-level learned literals (#8703)

These changes extend the partition generator to be able to do the following:

Access the order_heap in MiniSat and make partitions from those literals.
Specify a number of checks between partitions. This is relevant for only the revised and strict-cube strategies.
Append zero-level learned literals to the partitions.

Fixes and improvement for IAND solver (#8771)

This fixes a model soundness bug in the non-linear solver for IAND, which was caused by the core NL model solving for an IAND term. This adds 2 delta debugged variants of a benchmark from an application.

It also improves the value-based refinement scheme for IAND significantly by ensuring we take the modulus of model values. This should make it terminating.

Eliminate use of getBaseType (#8764)

For the model, this was used for ensuring that we skipped enumerating the Real constant 1.0 if the Integer constant 1 already existed in the model. Now, these two nodes are disjoint, and due to #8740, the use of getBaseType in this context has no effect since the set of real and integer constants are disjoint.

It was also used in CEGQI in a similar manner, where since equivalence classes of Int and Real terms are disjoint, it is not necessary to search for e.g. Real variables in integer equivalence classes.

Add utilities in preparation for supporting str.nth (#8766)

Work towards efficient support for to_lower/to_upper.

Fix debug failures in LFSC proofs due to curried arithmetic operators (#8763)

This ensures we use different variants of PLUS, MULT, NONLINEAR_MULT internally to avoid type checking failures in debug mode during LFSC printing.

Fixes regression failures in debug mode for LFSC.

Refactor logic exceptions during preregistration for arithmetic (#8769)

Fixes #8755.

Update CoCoALib version (#8757)

This PR updates our cmake scripts for CoCoALib to use the latest and greatest version.
While we don't actually want to use any of the new features, the new version finally uses an Apache license!

Minor refactoring for sep theory (#8753)

Work towards fixing #8659.

Fix type of null terminator for ADD/MULT for LFSC (#8762)

This fixes many LFSC proof failures that are occurring now because of using 1.0 instead 1 as null terminator for MULT, and 0.0 instead of 0 for ADD.

Eliminate use of subtypes from remainder of type rules (#8756)

This PR should be added before the minor release that advertises our policy change for subtyping.

Preserve types in rewriter and make core type rules strict (#8740)

This is the key step for eliminating the use of subtyping.

This makes several changes:
(1) CONST_INTEGER is now used for integer constants, which is now exported in the API. The type rule for CONST_RATIONAL is changed to always return Real, even if its value is integral. This means we can distinguish real and integer versions of the integers. Note this also implies that the rewriter now fully preserves types, as rewriting TO_REAL applied to a constant integer will return a constant integral rational.
(2) The type rules for EQUAL, DISTINCT, ITE and APPLY_UF are made strict, in other words, we given a type exception for equalities between an Int and a Real. This restriction impacts the API.
(3) The arithmetic rewrite for (Real) equality casts integers to reals as needed to ensure Reals are only made equal to Reals. The net effect is that TO_REAL may appear on either side of equalities.
(4) The core arithmetic theory solver is modified in several places to be made robust to TO_REAL occurring as the top symbol of sides of equality.

Several assertions are strengthened or added to ensure that equalities and substitutions are between terms of the same type, when it is necessary to do so.

Two quantifiers regressions are modified since the solving techniques are not robust to TO_REAL. A few unit tests are fixed to use proper types.

[docs] Marking internal comment in proofs docs (#8747)

Make regular options access const (#8754)

One of the loose ends of the options refactor is that internal code can write to options at will, even when the accessing it via Env::getOptions() which returns a const reference. There are technical reasons for this, C++ does not propagate the constness into reference members.
This PR changes this behaviour by making the references members we use all over the place (options().smt.foo) const references and adding new functions writeSmt() which allow write access -- if you have a non-const handle to the options object.
In order to do that, this PR also changes all places that legitimately change the options (options handlers, set defaults, solver engine and places where we spawn subsolvers) to use the new syntax. After that, only a single place remains: the solver engine attempts to write the filename (from Solver::setInfo("filename", "...");) into the original options (that are restored to the new solver object after a reset. As only the API solver has write access to this, it is moved to the Solver::setInfo() method.

With this PR, all internal code is properly guarded against erroneous (and reckless) changing of options.
Fixes cvc5/cvc5-projects#12.

Remove --build from GMP configure line (#8752)

This is an attempt to fix the pypi build.

Relax an assertion in the evaluator (#8751)

In a rare case this can throw after https://github.com/cvc5/cvc5/pull/8740, complaining that `(/ 0.0 0)` and `(/ 0.0 0.0)` are not the same.

Ensure substitutions in nonlinear solver are properly typed (#8748)

We would apply substitutions between int and real terms, effectively hiding the intness of variables from the coverings solver.
Fixes #8744.
The example from #8744 times out after the fix, thus no regression.

Fix some issues with the Python API tests (#8746)

This PR addresses a few issues in the Python API:
    the implementation of defineFunsRec() lacked the call to the C++ function
    a bunch of tests for defineFunsRec() were missing
    the test for getInstantiations() was incorrectly named and thus not valled.
    add missing test for hashing of Sort

Add test coverage for almost everything from the Java API  (#8723)

This PR adds tests for almost everything that is not yet covered by the java API tests.

Compress debug symbols to make libcvc5 smaller (#8743)

This adds `-gz` which compresses the debug symbols to make debug builds smaller. In my setup, `libcvc5.so` shrinks to about half its size from ~450MB to ~225MB.

Improvements for evaluation in model (#8738)

This marks APPLY_SELECTOR and SEQ_NTH as unevaluatable kinds.

This means that get-value applied to applications of them e.g. (seq.nth t) will evaluate to c if (seq.nth t) is in the same equivalence class as constant c. (Note that this could be further improved to reason by congruence for (seq.nth s) where s = t, which I'm considering to do on a followup PR).

This removes many of the required -q from the command line arguments of our regressions. This also does some minor cleanup to our regressions to remove -q from further regressions.

Do not depend on subtyping for APPLY_UF in TPTP parser (#8737)

Add unit tests for getInstantiations (#8741)

Do not rely on subtyping in real-to-int preprocessing pass (#8732)

Disable proof testers for delicate regressions. (#8735)

This PR disables regress2/nl/ufnia-factor-open-proof.smt2 benchmark which fails with some debug builds in the nightlies. We should consider adding an option to disable testers under certain build configs. This PR also ensures that the lfsc tester displays all the options used to generate the LFSC proof.

More preparation for strict type rules (#8733)

This is work towards making equalities and substitutions between terms of equal types.

Fix proofs for ppAssert for theory Bool (#8708)

Fixes #8705.

This also impacts unsat cores when proofs are enabled.

Fallback for sequential substitution proof reconstruction (#8730)

This makes our proof reconstruction fallback to a trivial sequential reconstruction in very rare cases where a sequential substitution fails to reconstruct. This can happen in some rare cases where terms are used in the domain of a substitution that otherwise would be modified by earlier substitutions. This occurs on 2 QF_SLIA benchmarks, attached is a delta-debugged version.

This also changes a warning message to a trace for this case, as a warning message may cause LFSC proof checking to fail when it should just give a warning for a TRUST_SUBS step, which is the default behavior regardless.

Eliminate arithmetic subtyping for (dis)equalities from TPTP parser (#8724)

Towards making equality strictly typed / eliminating arithmetic subtyping.

Separate ill-typed portion of arith models (#8734)

This makes it so that the ill-typed portion of arithmetic models is not included in the main arithModel map.

Conceptually, we should not include entries in the arithmetic model that violate type constraints since these should never be used e.g. in non-linear to justify whether a model is correct. Instead, by not including that value, we assume that no value was given for that variable. Sanity checking of the arithmetic model then needs only to access the ill-typed portion of the model directly.

This makes it so that strict type invariants can be enforced in the non-linear solver's model.

Fix LFSC side condition for matching premise of concat_unify (#8726)

Occurs in QF_SLIA/20180523-Reynolds/pyex/peterc-pyex-doc-cav17-td/pymongo/pymongo-mongoclient/cc647bd246e485aa31a4dc8978e5211a7c1336911d1bfc78b45ee679.smt2 after 464 seconds on my machine.

Add test coverage for almost everything from the Python API (#8720)

This PR adds tests for almost everything that is not yet covered by the python API tests.

Preparation for making equality strictly typed (#8728)

This changes several places in arithmetic so that it never generates equalities between and an Int and a Real.

It also changes several uses of mkConstReal on integer values with mkConstInt whenever their type does not matter.

Since we do not construct CONST_INTEGER yet, this PR has no behavior change yet.

Fix cache in learned rewrite preprocessing pass (#8725)

Fixes #8722.

Fix more issues with subtypes in regressions (#8727)

In preparation for making type rule for equality strict.

Add operators table.aggr and table.join (#8681)

Use purification for set comprehension reduction (#8711)

Currently, the reduction lemma does not purify set comprehension from its reduction predicate. This means that our rewriter (if it were smart enough) should rewrite the reduction predicate to true.

Moreover, a new forthcoming model-based instantiation technique was giving wrong answers when set comprehensions were present since it could prove the reductions were tautological.

Improve finding Python library/includes (#8718)

On macOS, find_package(PythonLibs ...) does not find the Python
include directory or library when they were installed via homebrew.
find_package(Python ...) is more robust, but only available on newer
versions of CMake. If we are compiling cvc5 on macOS and we have a newer
version of CMake available, this tries to use find_package(Python ...)
to find the paths.

fix link to `Testing cvc5` in `INSTALL.md` (#8675)

The current link renders strangely and does not lead to the relevant subsection. This PR fixes that.

Make equality solver the entry point for all equality engine explanations in arithmetic (#8719)

This makes it so that EqSolver is the main entry point for all equality engine explanations in arithmetic; it still defers to the CongruenceManager to compute these explanations.

To do this, when the core linear solver depends on an explanation from the equality engine, it instead provides a placeholder. Since explanations are computed recursively in TheoryEngine, this will trigger another call to TheoryArith::explain, which will then be handled by the EqSolver. Thus, there should be no net effect on the overall explanations in this commit.

This is work towards eliminating the dependency of the linear solver on the equality engine.

Make printStatisticsSafe public (#8721)

Solver::printStatisticsSafe() is private right now. There is no real reason for that, and as we claim that the driver is only using the regular API we should just make it public.

Add declareOracleFun interface to SolverEngine (#8622)

After this PR, declare-oracle-fun will be added to the API and parser.

Refactor oracles using new std::function backend (#8717)

This also updates several places to be generalized to methods that return a vector of Nodes. Previously we had assumed a use case returning a single node.

After this PR, #8622 will be updated to use the new std::function interface.

Remove unecessary calls to equality engine from congruence manager (#8715)

Removes a deprecated explain interface.

Remove obsolete private methods from API (#8716)

This PR removes two private utilities from the API: Sort::sortSetToTypeNodes and one DatatypeDecl constructor.

Fix rewrite for to_real in division by zero (#8714)

Fixes #8712.

Add support for oracle constant nodes (#8707)

This is the beginning of a refactoring to make std::function the basis for oracles internally, not binary names.

Fix LFSC node converter for 0-ary tuples (#8706)

Was missing 0-ary Tuple case for type-as-node.

Also removes a spurious check in the user-defined sorts case.

Fixes some issues in the nightlies.

Update LFSC version (#8713)

This updates the get-lfsc-checker script to get the latest version of
LFSC, which supports older versions of CMake.

Use (non-recursive) unpurified form instead of original form for defining Skolems (#8699)

This modifies our treatment of purification Skolems in the internal proof calculus. In particular, we now use an "unpurified form" instead of "original form" for defining Skolems. SKOLEM_INTRO is modified to prove the equality between a skolem and its unpurified form.

For example:
k1 purifies (ite A B C)
k2 purifies (+ k1 1)

The unpurified form of k2 is (+ k1 1), its original form is (+ (ite A B C) 1).

As a consequence:
(1) Our global skolem sharing is now slightly weaker, for example a k3 could be constructed whose unpurified form is (+ (ite A B C) 1); previously this would guaranteed to be k1.
(2) We do not require recursively computing the original form of terms when constructing purification Skolems,
(3) The witness form proof generator requires a fix point.
(4) The LFSC signature is simplified, and does not require a side condition to recursively compute the original form of a Skolem.

Fixes cvc5/LFSC#81.

docs: Some fixes in options docs. (#8710)

Change option name for mbqi in fmf (#8701)

In preparation for a new basic implementation of MBQI.

Simplify representation of datatypes at the TypeNode level (#8702)

They previously were TYPE_CONSTANTs hashed by the index of their DType in the NodeManager. Now they are variables having an attribute that is their index.

This makes datatypes more analogous to uninterpreted sorts, and eliminates the need for an auxiliary DatatypeIndexConstant class.

Final preparation for CONST_INTEGER (#8700)

With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.

This does not make this change yet, so CONST_RATIONAL is still used throughout.

Migrate basic EqualityEngine management from CongruenceManager to EqSolver (#8684)

This is work towards having the linear arithmetic solver not impose restrictions on equalities.

The linear arithmetic solver using a CongruenceManager which involves many non-standard uses of the equality engine.

The responsibilities of the CongruenceManager should be migrated to the arithmetic EqSolver, which manages the equality engine in the default way.

This PR is the first step. It makes it so that the memory management and notifications of the equality engine are now solely the responsibility of the EqSolver.

All relevant notifications from the EqSolver are directly forwarded to CongruenceManager. Thus there are no significant behavior changes in this PR.

This PR required removing the experimental option arithCongMan, which forces having the CongruenceManager and the EqSolver both use equality engines.

Add strict-cube and decision-trail partitioning strategies (#8651)

Add the strict-cube modification to the revised partitioning algorithm and add the full-trail partitioning strategy.

More robust treatment of flattening in arith rewriter (#8695)

Currently can allow rewritten forms to be rewritable.

Fixes #8692. Fixes #8693. Fixes #8697.

Make arith msum utility agnostic to Int (#8694)

This utility should continue to assume arithmetic subtypes.

Fixes #8691.

Add missing tests for some corners of the API (#8688)

This PR adds a bunch of unit tests for some not yet covered corners of the API.

docs: Do not use explicit line numbers in literalinclude. (#8690)

Further refactoring in preparation for CONST_INTEGER (#8687)

Miscellaneous refactorings from trying to enable CONST_INTEGER.

Fix tuple printing in LFSC (#8696)

We weren't collecting them as user-defined types after the recent refactor to Tuples.

Properly represent Tuples in the TypeNode AST (#8648)

This makes it so that Tuple types are properly represented in the AST. It also removes a spurious restriction that disallowed higher-order tuples (this was leftover from a very old sanity check in the old API).

For example, a tuple type over (Int, Int) is now (TUPLE_TYPE INT INT) instead of a DATATYPE_TYPE constant.

Tuple types behave exactly like datatypes; we can still retrieve their DType as before.

This is in preparation for gradual types and symbolic tuple projections.

Add simple type rule for real-or-int arguments (#8685)

This adds a simple type rule, ARealOrInteger, which checks whether the
argument of an operator is either a Real or and Int. Note that this
is currently equivalent to AReal, but the plan is to make AReal
strict in the future.

Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)

This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver.

Towards proper usage of TO_REAL (#8680)

This is work towards making the rewriter preserve types, which is work towards eliminating subtyping.

This makes it so that the arithmetic rewriter does not simply drop TO_REAL from all terms, as this may change the type of the Node. Instead, TO_REAL is pulled upwards, and can be removed beneath arithmetic relations. TO_REAL is not eliminated if it occurs as a child of an operator not belonging to arithmetic. For example if x,y : Int:

(= (+ (to_real x) y) 0.0) ---> (= (to_real (+ x y)) 0.0) ---> (= (+ x y) 0.0) ; note this is the same rewritten form as before
(P (+ (to_real x) y)) ---> (P (to_real (+ x y))).

The one exception is that to_real applied to constants is simply dropped (for now), for example:

(to_real 5) ---> 5

where above, a Real term is rewritten to an Int term. (Fixing this will require further PRs that make integer constants of kind CONST_INTEGER and integral CONST_RATIONAL have Real type, thus we can have the above rewrite return 5 that is constant and has type Real).

Several quantifiers utilities are patched to preserve their behavior wrt handling TO_REAL.

Finally, a few fixes for subtypes are made to the regressions that we were not catching as errors before, and adds one regression.

The net effect of this PR is that the rewritten form of terms may have to_real applications that occur as direct children of symbols from other theories. Special care is required for preregistration, shared terms, and getting model values in the linear solver to strip off TO_REAL if necessary before using the (unmodified) interface to the linear solver.

FYI @barrettcw

Document non-standard string operators (#8679)

This adds documentation for `str.indexof_re`, `str.update`, `str.rev`,
`str.to_lower`, and `str.to_upper`. Note that it moves the documentation
of strings to the "non-standard or extended theories".

Ensure mkConstInt is used on integral rationals only (#8683)

This is work towards using CONST_INTEGER for integer constants.

This corrects a few places that incorrectly assumed that integers were necessary.

Refactor interfaces for E-matching (#8665)

InstMatch objects are now fully owned by Triggers. They are passed by reference to InstMatchGenerators.

This also simplifies the interfaces by not passing the quantified formulas.

This is in preparation for making InstMatch objects carry entailment test information.

Make extended rewriter use standard Subs utility (#8682)

This is work towards ensuring all substitutions are strictly typed.

Add an option to enable all testers. (#8676)

Add missing parenthesis for bags documentation (#8673)

Add unit test for code not exposed by java API (#8678)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the java API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the java API.
It also corrects a few other minor issues.

Add unit test for code not exposed by python API (#8677)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the python API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the python API.

Add some missing API tests (#8669)

This PR adds a couple of simple API tests for parts of the API that are not covered yet.

Move tests around (#8670)

This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/.

int-blaster: not allowing higher order functions (#8674)

Currently we throw an OptionException if higher order logic is enabled, but we only check this once we reach an APPLY_FUN node.
This PR does the check regardless of APPLY_FUN, thus capturing, e.g. BAG_MAP.
Fixes cvc5/cvc5-projects#415.
The PR also includes a simplified version of the test from that issue.

Move datatype split inference scheme to its own method (#8664)

Clean code for datatypes split (#8667)

Non-moving version of #8664.

Make labelled separation logic asserts preserve labels (#8671)

This is a first step towards fixing #8659.

The issue is that when two labels are equal, we assume they refer to subheaps of the same heap. This is incorrect for magic wand. This ensures we preserve labels, a further PR will ensure that syntactic equality on labels (instead of semantic equality) is used for knowing when two pto constraints must be unified. This means that SEP_LABEL nodes should never be rewritten.

Fix PyUnicode_AsWideCharString signature (#8522)

Add proper exception specification to the `PyUnicode_AsWideCharString` signature.

Add resource limiting to coverings solver (#8672)

Right now, resource limits are not checked while the coverings solver is computing. This PR adds a new resource and spends it within every recursive call of the coverings solver. This fixes cases where cvc5 does not honor the per-call time limit on QF_NRA.

Add option to apply constant propagation for all learned literals (#8668)

Adds `--simplification-bcp`, disabled by default.

Refactoring of initial lemmas in datatypes (#8666)

This is work towards revising how/when the datatypes instantiate rule is applied.

This simplifies the management of when new terms are registered in the theory of datatypes.

We now use the equality engine's eqNotifyNewClass callback to know when a term should be considered. Previously, this was split over two methods (additionally, collectTerms).

Most importantly, this eliminates the need for a manual addition of the "instantiated constructor term" in getInstantiateCons, which complicates the logic for the impact of applying the datatypes instantiate rule.

Minor improvements for entailment test (#8663)

Makes some minor improvements to the existing (non-incremental) entailment tests, based on comparing with a new implementation.

Minor improvements to quantifiers utilities (#8661)

Make IndexTrie take nodes (#8649)

This makes the class easier to use and allows for a usage where the null node is interpreted as specifying all nodes.

This is in preparation for using this class for testing whether an instantiation from any instantiation strategy is currently feasible based on learning in the style of fail masks from Janota et al FMCAD 2021.

Also, this class should be renamed to something more appropriate, since it no longer takes indices.

FYI @MikolasJanota

Move rep set iterator to its own file (#8647)

Refactor InstMatch (#8646)

Also simplifies the (old) version of multi trigger matching, which copied InstMatch objects unnecessarily, and also used EqualityEngine iteration instead of iterating on a trie.

This is in preparation for making InstMatch objects optionally track fast (and generalized) failures based on configurable criteria.

Refactor mkRep option for instantiation (#8657)

This removes mkRep as an option for addInstantiation.

It adds a new interface for making term vectors representative, which is required for FMF instantiation.