Add set.map signature to lfsc (#8860)

Fix buildbot failure

Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)

This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR.

It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default).

This is work towards efficient support for `to_lower`/`to_upper`.

[CMake] Improve FindGMP (#8846)

Fixes #8792. This commit fixes issues with/improves our current
implementation of FindGMP:

- Version check that does not rely on regex matches in `gmp.h`. Instead,
  this commit uses a test program that checks at compile-time whether
  the GMP version is recent enough. This is more robust, because on some
  systems (such as Fedora), `gmp.h` includes another file that has that
  version information.
- It now also checks for the `gmpxx.h` header and the `gmpxx` library.
- The commit changes the compile test to use the include directories and
  libraries that were found using `find_path` and `find_library`.

Disable `lfsc` tester if `proof` tester is disabled. (#8857)

This automatically disables the `lfsc` tester for regressions where `proof` tester is disabled.

Add MBQI to SMT comp script (#8858)

Also fixes 2 existing issues in the script (that @nafur pointed out).

Add declareOracleFun to the Java API (#8815)

Disable LFSC for regression with learned rewrite (#8855)

Fixes buildbot issues.

Fix corner case of interpolants from conjectures with no free variables (#8853)

Fixes #8852.

Add inference rules for set.map operator (#8849)

Fix check for whether a term contains an uninterpreted constant (#8845)

Fixes #8842.

We now say "unknown" for the benchmark on that issue.

Disable arithmetic static learning when unsat cores are enabled (#8830)

The arithmetic static learner uses non-local reasoning and does not have proof support. Thus it may rewrite A ^ B to A ^ B' where ( A ^ B ) => B', but the preprocessor by default assumes that the replacement is such that B => B'.

This disables the arithmetic static learner when unsat cores are enabled. Other static learning appears to be local and is still enabled.

This further corrects an issue in set_defaults that checked incompatibility with unsat cores based on whether proofs are enabled. We now check compatibility independent of whether proofs are enabled. This also corrects several restrictions on things that previously were treated as being incompatible with unsat cores (but not proof unsat cores) that were spurious.

Fixes #8822.

Eliminate static options access from pattern term selector (#8825)

Towards eliminating options scopes.

Preparation for SEQ_NTH applied to strings (#8779)

No behavior changes in this commit for current main.

[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.

Fix missing conclusion for sep pto neg prop (#8844)

Was introduced in the refactoring in #8768.

Fixes #8841.

Restricting the bit-width in int-to-bv (#8814)

`cvc5` only supports bit-widths of `unsigned` size for BitVector sorts (see, e.g., [here](https://github.com/cvc5/cvc5/blob/4338d9d49a41022d34cd4cbabf17a66fdf39efae/src/expr/node_manager_template.cpp#L178)).

This checks that the provided bit-width for the `int-to-bv` option is in the right range.

Fixes https://github.com/cvc5/cvc5-projects/issues/425 and includes a regression that is based on the test from the issue.

Disable arrays in eager bit-blasting (#8785)

Fixes cvc5/cvc5-projects#461 . This does not allow arrays in eager bit-blasting, that is, only QF_BV and QF_UFBV are allowed. The reason is that Ackermannization (which is turned on in eager bit-blasting) eliminates array operators but does not eliminate array variables, that later cause a logic exception.

Make interpolation robust to conjectures with no shared variables (#8840)

Fixes #8833.

Refactor how options are passed to the printer (#8827)

Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)

Make subs minimize utility robust to non-constant evaluation (#8839)

Fixes #8834.

Fix issues with to_real around coverings solver (#8837)

This PR fixes two issues with the (missing) handling of to_real.
The first is that equality substitution was not aware of to_real yet, possible introducing models for both x and (to_real x).
The second is that the conversion to libpoly polynomials would also not properly unpack to_real expressions.
Fixes #8835.

Fix FindCaDiCaL script (#8838)

This fixes issues with finding a system-installed cadical.
Fixes #8836.

Update to GoogleTest 1.11.0 (#8813)

Using GoogleTest 1.10.0, when trying to build unit tests on m1 mac an error about deprecated methods fails the compilation of gtest.

Eliminate more static options accesses (#8832)

Eliminate static options access for central ee (#8823)

Also refactors TheoryEngine to not maintain its own reference to logic info and an accessor to it.

Towards eliminating option scopes.

Eliminate static options access in skolemize (#8831)

Fix mixed arithmetic issue in relevant domain (#8826)

Fixes #8821.

Eliminate static options access in BV inverter (#8829)

Make Rewriter::rewrite non-static (#8828)

This furthermore eliminates smt::currentSolverEngine.

Use function array constants in HO solver (#8818)

This makes lambdas rewrite to function array constants when possible. This extends our HO solver and utilities to be robust to check whether a node represents a lambda (uf::FunctionConst::toLambda).

This furthermore removes the isConst rule for LAMBDA; lambdas are never constant.

The PR also improves our check-model so that warnings are not thrown if rewriting can show that the model value of a term is equivalent modulo rewriting to its representative in the model equality engine.

This eliminates the last remaining static calls to rewrite. This is work towards eliminating SmtEngineScope.

Make sure phase-shift lemma is properly typed (#8824)

This PR addresses #8773 by making sure that the phase shift lemmas generated by the sine solver are properly typed.

Eliminate some static options access (#8795)

In preparation for eliminating options scopes.

[proofs] [alethe] Remove static call to options from post-processor (#8817)

Add model-based quantifier instantiation (#8729)

This is a straightforward reimplementation of Ge/deMoura from CAV 2009.

Eliminate static access to dtSharedSelectors (#8804)

Towards eliminating option scopes.

Eliminate more static options accesses (#8802)

A block of code changed indentation in the induction solver, this is cleaned to conform to guidelines.

Introduce function array constant (#8793)

This introduces the FUNCTION_ARRAY_CONST kind and its payload FunctionArrayConst.

This is in preparation for refactoring isConst for functions in higher-order.

In particular, the plan is to never consider LAMBDA to denote a value of function sort. Instead, lambdas may be written to function array constants, whose uniqueness is trivial to justify.

This refactoring when completed will furthermore eliminate the last remaining static calls to the rewriter, to be done in a followup PR.

Fix subtype issues in proofs for nonlinear solver (#8782)

Causes a debug proof failure on proof-new.

bv: Disable rule ExtractArith. (#8816)

Add table.group operator (#8731)

Add declareOracleFun to API (#8794)

Java and Python will be added in followup PRs.

Remove spurious assertion in isLegalElimination (#8812)

Fixes #8805.

The isLegalElimination method correctly catches Int -> Real as an illegal elimination.

Make model core robust to when we cannot show the model satisfies input (#8811)

Fixes #8807.

bv: Add resource limits support for CaDiCaL. (#8788)

Fixes #8776.

Simplification of smt2 printer for type ascriptions (#8801)

Previously had code for dealing with subtypes

Move smt_util to preprocessing/util (#8799)

src/smt_util contains a single file that is only used by the miplib trick preprocessing pass. This moves it to preprocessing/util.

Reenable assertion in skolem definition manager (#8797)

This reenables a variant of an assertion that was deleted in #8749, a weaker version of that assertion should now hold.

Add option to send all instantiations in a bounded range (#8796)

There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings.

Add cross-compilation for arm64 on macOS (#8758)

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

More removing of unused code (#8806)

Trying to break cycles when printing a .dot DAG (#8698)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are:

- If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case.

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

New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)

Change the way cvc5 identifies THEORY_LEMMA clusters when --print-dot-clusters option is used. Previously, only proof nodes with SCOPE rule after a CNF cluster could identify a THEORY_LEMMA cluster. Now, any of the following rules, after a CNF cluster, can identify it:

1. SCOPE
2. THEORY_LEMMA
3. Any rule R in the following range: CNF_ITE_NEG3 < R < LFSC_RULE

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

Minor deleting of unused code (#8800)

Towards improving coverage.

Add options and regressions to increase coverage (#8803)

Also corrects an issue with the text interface. When get-model is used with model cores, we do not currently filter the output. This ensures that we do.

Basic cleanup of sep theory (#8790)

Most of the simplifications are due to the fact that we only handle a single heap type. (The solver was initially designed to potentially handle more than one heap type).

Make skolem definition manager robust to definitions for already asserted skolems (#8749)

It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways.

It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest.

Eliminate subtypes (#8783)

Refactor declare oracle command (#8742)

In preparation for adding oracle functions to API.

Minor cleanup of datatypes theory (#8791)

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.