google test: expr: Migrate node_builder_black. (#5855)

Miscellaneous cleaning in theory engine (#5854)

This statistic is unused, I believe it is leftover from deleted code.

Adding an option to optimize polite combination for datatypes (#5856)

This PR makes the optimization introduced in bbca987 optional.

Introduce quantifiers registry utility (#5829)

This is a simple module for determining which quantifiers module has ownership of quantified formulas.

This is work towards eliminating dependencies of quantifiers modules.

Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.

Clarifying documentation of `--static-binary` (#5844)

The documentation regarding --static-binary is improved.

Eliminate equality query dependence on quantifiers engine (#5831)

This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.

[proof-new] Catch trivial cycles in SAT proof generation (#5853)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from

       l1 v l2   ~l1 v l3   ~l2 v l3
(ok) ------------------------------
                  l3
in which l3 = l1 v l2, to

         l1 v l2   ~l1 v l3   ~l2 v l3
(bad) ------------------------------
               l3 v l3
              ---------
                 l3
This commit now catches the trivial cycle before it's generated.

Add BV solver bitblast. (#5851)

This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.

[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.

Also improves a bit tracing and some comments.

(proof-new) Miscellaneous fixes and regressions (#5841)

(proof-new) Refactor theory preprocessing (#5835)

This simplifies our algorithm for theory preprocessing. The motivation is two-fold:
(1) Proofs are currently incorrect in rare cases due to incorrectly tracking pre vs post rewrites.
(2) We can avoid traversing Boolean connectives with term formula removal. Note that this PR relies on the observation that term formula removal leaves Boolean structure unchanged and can apply locally to theory atoms.

Furthermore, notice that our handling of lemmas generated by term formula removal is now more uniform. In the second algorithm, term formula removal is not applied to fixed point anymore. In other words, we do not remove skolems from lemmas generated by term formula removal recursively. Instead, since lemmas are theory-preprocessed recursively, we use the fixed point that runs outside the above algorithm instead of relying on the inner fixed point in term formula removal.

This PR resolves several open issues with proof production on proof-new.

I will performance test this change on SMT-LIB.

Remove quantifiers regression from decision folder (#5830)

This is a duplicate of https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 and moreover is slow on proof-new.

Cleanup some includes (#5847)

In particular, theory_engine.h is included many places spuriously.

A few blocks of code changed indentation, updated to guidelines.

Improvements for NL traces (#5846)

This makes it so that -t nl-ext is a concise summary of what the nl-ext solver is doing, which I use frequently for debugging.

This is a temporary solution, we should consider a deeper refactoring of traces throughout NL at some point.

[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).

Eliminate PREPROCESS lemma property (#5827)

This is now possible since we always preprocess lemmas.

Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.

Simplify alpha equivalence module (#5839)

This class uses a discrimination tree which can compute subsumption as well as alpha-equivalence. This class was initially designed to also support subsumption. However, we were only using this class for alpha-equivalence and hence (canonized) Node comparison suffices and the class can be simplified. It also makes minor cosmetic updates to the module.

If we plan to support subsumption checking later, we will write a new module, and use this class https://github.com/CVC4/CVC4/blob/master/src/expr/match_trie.h which is a more mature version of the class deleted by this PR.

Note: I verified that the new and old implementation was equivalent using a temporary AlwaysAssert.

Avoid calling the printers while converting sexpr to string. (#5842)

This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.

Fix BagsRewriter::rewriteUnionDisjoint (#5840)

This PR fixes the implementation of (union_disjoint (union_max A B) (intersection_min A B)) =(union_disjoint A B).
It also skips processed bags during model building.

Fix unguarded call to get representative (#5838)

Introduced in 3234db4.
Fixes #5837, that benchmark is now unknown.
Adds an SMT-LIB benchmark that also crashes.

[proof-new] Connecting new unsat cores (#5834)

Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.

Add bag inferences for operators: intersection, duplicate_removal, and empty bags (#5832)

This PR adds inferences for operators: intersection, duplicate_removal, and empty bags during post check.
It also fixes a bug in SolverState::getElements

(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)

This is work towards resolving two kinds of failures on proof-new:

(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.

A followup PR will simplify and fix proofs for theory-preprocessing.

Reorganize calls to quantifiers engine from SmtEngine layer (#5828)

This reorganizes calls to QuantifiersEngine from SmtEngine. Our policy has changed recently that the SmtEngine layer is allowed to make calls directly to QuantifiersEngine, which eliminates the need for TheoryEngine to have forwarding calls. This PR makes this policy more consistent.

This also makes quantifier-specific calls more safe by throwing modal exceptions in the cases where quantifiers are present.

Marking "major" since we currently segfault when e.g. dumping instantiations in non-quantified logics. This PR makes it so that we throw a modal exception.

Remove regex header from cvc4cpp.cpp (#5826)

This PR replaces the heavy hammer std::regex_match for checking numbers with string operations

Simplify lemma interface (#5819)

This makes it so that TheoryEngine::lemma returns void not LemmaStatus.

Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.

It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.

Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.

Always theory-preprocess lemmas (#5817)

This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.

Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.

It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.

This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.

Add option for whether to filter candidate rewrite pairs (#5825)

This option should be disabled for the new sygus reconstruction algorithm on #5779.

Split pattern term selector from trigger (#5811)

This separates the utilities for selecting pattern terms from the Trigger class itself. This includes a PatternTermSelector, which implements the techniques for selecting the pool of pattern terms, and TriggerTermInfo which contains basic information about pattern terms.

It makes minor refactoring to make the PatternTermSelector class more than just static methods, e.g. it is now a configurable object that selects pattern terms. This makes some of the methods take fewer arguments.

More refactoring is possible, to be addressed on future PRs.

(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)

This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).

Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.

Thread proofs through arith channels & similar (#5818)

Thread proofs through conflict/lemma storages & channels in TheoryArithPrivate

d_acTmp
d_approxCuts
lemma output channel
conflict output channel

Use term canonizer utility locally in quantifiers (#5823)

Term canonization was used in two places, which are unrelated and don't need to share the instance.
Also removes a few unnecessary methods from QuantifiersEngine.

Use standard conflict mechanism in quantifiers state (#5822)

Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck.

Introduce quantifiers inference manager (#5821)

This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.

The code for adding lemmas in quantifiers engine will be migrated to this class.

Remove deprecated quantifiers modules (#5820)

Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

Reestablishing support for define-sort (#5810)

Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.

This fixes issue #5809.

Add proofs to TheoryArithPrivate::propagate (#5812)

Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.

Refactor bags::SolverState (#5783)

Couple of changes:

SolverState now keep tracks of elements per bag instead of per type.
bags::InferInfo now stores multiple conclusions (conjuncts).
BagSolver applies upward/downward closures for bag elements

Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout

Split inst match generator into multiple files (#5805)

No code changes on this PR, only move + format.

Split E-matching strategies to own files (#5807)

Code move + format only

rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)

Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems

 Initial cleaning of e-matching instantiation strategy (#5796)

In preparation for splitting this into multiple files.

No behavior changes in this PR.

Initial cleaning of triggers (#5795)

In preparation for splitting trigger.h/cpp into multiple files.

This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.

Initial cleaning of inst match generator (#5794)

In preparation towards breaking this file up into multiple files.

No code changes, only updates to conform to new guidelines.

(proof-new) Instantiation list utility (#5768)

This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new.

Add interface for getting preprocessed term (#5798)

Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is.

This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are.

Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete.

[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)

Breaks down resolution, factoring and reordering. The hardest part of this process is making getting rid of the so-called "crowding literals", i.e., duplicate literals introduced during the series of resolutions and removed implicitly by the SAT solver. A naive removal via addition of premises to the chain resolution can lead to exponential behavior, so instead the removal is done by breaking the resolution and applying a factoring step midway through. This guarantees non-exponential behavior.

Add div, mod, abs in non-strict parsing mode (#5793)

The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.

arith: Proofs for Diophantine cuts (#5792)

Thread proofs through the diophantine "cutting" lemma generator.

Refactoring the single invocation solver (#5706)

This does an intermediate refactoring of the single invocation solver to make a few things clearer and to add preliminary support for functions that have been marked as solved by external techniques.

This is in preparation for generalizing the CAV 2015 single invocation techniques.

Fix type issues with relevant domain computation (#5788)

This fixes 2 issues with relevant domain type computation, the first involving arithmetic INST_CONSTANT that do not belong to the current quantified formula being solved for in a monomial sum, the second involving parametric datatype selectors.

Fixes #5635. Both benchmarks on that issue are unsolved (one timeout, one unknown) but throw no assertion failure.

Fix corner case of wrongly applied selector as trigger (#5786)

Fixes #5766.

Do not track processed in remove term formulas loop (#5791)

The assertion/tracking was spurious, since an eliminated term may occur in multiple contexts.

Fixes #5728 (which I could not reproduce currently). Adds a regression from a duplicate of that issue.

SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)

This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.

More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.

Use arbitrary ground term assignment for sorts where isInterpretedFinite is true (#5790)

This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.

This fixes #5738.

This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.

Implement proofs for arith BRAB lemmas (#5784)

All changes:

Add a Pf type alias for std::shared_ptr to
expr/proof_rule.h
Add an eager proof generator to TheoryArith for preprocessing
rewrites. Right now those are proven with INT_TRUST. Will eventually
fix.
Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable.
Same for TheoryArithPrivate::roundRobinBranch
Add EagerProofGenerator::mkTrustedRewrite.
Add some proofsEnabled methods.

Implement --no-strings-lazy-pp as a preprocessing pass (#5777)

This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.

Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.

Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

Split eager solver from strings solver state (#5775)

This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.

This is in preparation for adding new techniques to the eager solver.

No behavior changes in this PR, only reorganization.

Add unit test for api getInterpolant() -- issue #5593 (#5772)

The pull request addressed issue #5593 for adding an unit test.

Do not call ppRewrite on Boolean equalities (#5762)

Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.

Fixes #5761.

google test: expr: Migrate node_black. (#5764)

google test: Use ASSERT_* instead of EXPECT_*. (#5765)

Use ASSERT instead of EXPECT for consistency. There's no real benefit
for us to use EXPECT -- the main difference is that within a test,
EXPECT failures do not terminate the test, while ASSERT failures do.

This further fixes a minor issue in theory_sets_type_rules_white.h
(which is still not migrated to google test yet).

Foreign theory rewrite option (#5763)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.

Merge theory registrar and theory proxy (#5758)

The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.

This merges the helper class TheoryRegistrar into TheoryProxy.

Further simplifications in preparation for removing Expr layer (#5756)

This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.

These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.

This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.

Remove extended rewrite for arithmetic (#5760)

This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.

Fixes #5737, fixes #5740.

Strings arith checks preprocessing pass: step 2 (#5750)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the second step. It includes the implementation of the main function, as well as unit tests for it.

A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.

Fix issue 5513 (#5757)

Fix issue5513 by throwing an exception for unsupported bag operators

Rename getAntecedent to getPremises (#5754)

Changes:

renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)

[proof-new]  Implementing getProof in the API and SMT engine (#5751)

A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).

Add bags inference generator  (#5731)

This PR adds inference generator for basic bag rules.

bv-to-int: avoid binarizing nodes twice (#5749)

In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.

Make sure polynomials are properly factorized in nl-cad (#5733)

CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.

Remove dependency on expression layer in TPTP parser (#5753)

Fix warning in TPTP parser  (#5752)

strings arith checks preprocessing pass: step 1 (#5747)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.

Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.

Add new interfaces to term formula removal and theory preprocess (#5717)

This is in preparation for lazy lemmas for term formula removal.

Adding str.len to triggers (#5746)

This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.

Remove a few miscellaneous references to the expr layer (#5661)

Leftover from a development branch.

[proof-new] Only use old proofs for unsat cores if no proof new (#5725)

Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.

This also does some minor refactoring in some preprocessing. No behavior is changed.

Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.

Add option to track and notify from CNF stream (#5708)

This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).

This will be required for SAT relevancy.

No behavior changes in this PR.

Remove quant EPR option (#5716)

This was an experimental option used in combination with separation logic.

[proof-new] Adding a manager for the new unsat cores (#5723)

Based on proof nodes of refutations.

(proof-new) Miscelleneous fixes from proof-new (#5714)

Add proofs for nonlinear sign lemmas. (#5707)

This PR adds proof support for NL_SIGN lemmas.

Minor simplification to Theory::theoryOf (#5719)

This removes the special case of constants based on the observation that the theory that owns the type of a constant and the theory that owns its kind always should be the same.

This should lead to a small (maybe 1%) performance improvement, as this method is run ~191M times in our coverage build.

Delete duplicated code (#5718)

Move slow regression to regress3 (#5715)

Make theory preprocess rewrite equalities a preprocessing pass (#5711)

Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing.

This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine.

In detail, the motivation for this change:

(1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite.

(2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas).

(3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess".

Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.

Add proof for pi bound lemma (#5709)

This PR adds proofs for lemmas that introduce bounds on the constant representing pi.

Have unsat core regression agnostic to number of assertions in core (#5712)

Changing our unsat core infrastructure may change the cores we produce. This can be problematic for regressions that hardcode the number of assertions we get (such as this one). This commit changes such a regression to rather expect any core. It is motivated by exactly the previously described issue occurring after using the new proof infrastructure to generate unsat cores, which yielded a smaller core.

Kudos to @4tXJ7f for the sed magic.

Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

Add proof for sine shift lemmas. (#5710)

This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.

(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)

This PR adds proofs for the lemmas from the nonlinear factoring check.