Make sure conflicts are not rewritten (in arithmetic) (#5219)

The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.

(proof-new) Add the strings proof constructor (#4903)

This is the method for converting strings InferInfo into instructions for building ProofNode. Notice that this is done as a standalone module, and thus the theory of strings uses Inferences only, not PfRule.

The next step will be to integrate this utility into InferenceManager.

Improve OSX support by adding os detection and adapting calls for OSX. (#5023)

On OSX there is another libtoolize tool already available.
The gnu libtoolize version installed with MacPorts or brew is called glibtoolize.
This change makes it easier to run the file on OSX.

Signed-off-by: Malte Mues (mail.mues@gmail.com)

Process pending inferences at the beginning of datatypes post check (#5213)

This fixes a potential crash in datatypes where a pending inference is not processed on a call to Theory::check. This ensures the pending set of inferences in datatypes is empty after each check. This also ensures the pending vectors are cleared before each check in datatypes.

bv-to-int: change order of passes (#5208)

Closes #5095 and replaces #5110.
There are two tests in #5095 that produce two different assertion failures when using bv-to-int.
The first happens because the substitution map wasn't applied after the pass.
The second happens because div (that is introduced in the pass) is not rewritten using witness.
Both problems are solved by making sure that apply-substs, theory-preprocess and ite-removal are executed after bv-to-int.
The two tests from #5095 are included as regressions.

(proof-new) proofs for ArithCongMan -> ee facts (#5207)

Threads proof production through the ArithCongruenceManager's pipeline
of information to the equality engine.

The idea is to define a method:

ArithCongruenceManager::assertLitToEqualityEngine(literal, reason, pf)
This method asserts a literal to the equality engine with the given
proof and reason. It stores the proof of the literal for the equality
engine's future reference, and is smart about symmetric literals.

This machinery uses proofs that are not closed over the reason, as the
equality engine requires.

Other functions in the pipeline:

assertionToEqualityEngine
equalsCostant
construct proofs and call assertLitToEqualityEngine.
Future commits will address the ee -> ArithCongruenceManager pipeline,
and the relationship between ArithCongruenceManager and the rest of
arithmetic.

(proof-new) Add interface for trusted substitution and update ppAssert (#5193)

The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.

This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.

This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.

(proof-new) Allow null proofs from generators in LazyCDProof (#5196)

In some cases, a proof generator provided to a LazyCDProof may provide a null proof, which causes a segfault on proof-new currently. This PR makes LazyCDProof robust to this case; nullptr is interpreted as the fact is an assumption.

Add operators bag.from_set, bag.to_set to the theory of bags (#5186)

Add arithmetic preprocess module (#5188)

This class serves a similar purpose to the strings preprocess module (https://github.com/CVC4/CVC4/blob/master/src/theory/strings/theory_strings_preprocess.h).

It can potentially be used for reducing extended arithmetic operators on demand via lemmas.

This PR does not change the current behavior, but generalizes the use of operator elimination in TheoryArith to make this possible.

Recover from some exceptions. (#5203)

This PR replaces more calls to SmtEngine functions with calls to corresponding Solver functions in command.cpp. The PR also adds CVC4_API_RECOVERABLE_CHECK macro to use for recoverable exceptions.

Remove subtyping for sets (#5205)

Removed subtyping for sets in type_node.h

Fixes #4502, fixes #4631.

cmake: Add warning when unit testing is disabled due to assertions being disabled. (#5204)

This further fixes the testing instructions for API tests (formerly known as system tests)
in INSTALL.md.

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

SyGuS: Add fp.sub to default FP grammar. (#5206)

Integer: GMP: Move implementation of member functions to .cpp file. (#5190)

This moves the GMP implementation of member functions of class Integer from
the header to the .cpp file. This only moves code, and adds documentation for
previously undocumented or poorly documented functions.

I ran a performance check on the cluster on non-incremental QF_BV, QF_BVFP,
QF_FP, QF_LIA, QF_LIRA and QF_LRA (BV and FP logics heavily rely on class
Integer since class BitVector is implemented on top of Integer). This change has
no impact on performance.

Make sygus more robust to unknown responses in solution verification (#5199)

This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.

This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.

Remove subtyping for sets theory (#5179)

This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:

Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON

sygus-inst: Add more special BV values. (#5191)

Fix CI builds and add cancel workflow.

Fix theory white unit test (#5194)

Standardization of Theory (#5181)

This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.

Minor simplifications to substitution map class (#5180)

This class is an important utility in preprocessing, which we are adding proof support for. This simplifies the interface of this class with regards to unused interfaces for clarity.

(proof-new) Fixes for theory preprocessing proofs (#5171)

This fixes several subtle issues with theory preprocessing.

The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.

It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".

(proof-new) Make shared solver proof producing (#5169)

This makes the shared terms database use a proof equality engine as a layer on top of its equality engine, analogous to how this done in theories.

Allow for theory combination of strings with nonlinear real arithmetic. (#5111)

This PR makes sure that enabling strings and nonlinear real arithmetic at the same time works fine.
Right now, the configuration for strings enforces linear arithmetic if no integers are enabled, in particular for NRA.

Fixed #5109.

Decouple modules from TheoryArithPrivate (#5184)

This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.

This is in preparation for further refactoring of (lazy) arithmetic operator elimination.

(proof-new) New proofs in arith::Constraint::externalExplain (#5176)

This commit threads proofs through the core of arith:
Constraint::externalExplain, which recursively explain arith literals.
One of the base cases here is asking the EE for an explanation, through
the congruence manager. To delay implementing proofs in
ArithCongruenceManager to a separate commit, we stub out proof
production in ArithCongruenceManager::explain for now.

Remove duplicate declarations in th_bv.plf (#5183)

I think this is dead code now, but still good to fix.

SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)

(proof-new) Make arrays proof producing (#5112)

This includes adding a basic inference manager to arrays that ensures that the correct applications of PfRule are given to the inference manager.

Note that some calls to lemma are yet to be converted. Also note that some minor simplifications were made for unnecessary parts of the code.

Add additional ground terms to SyGuS instantiation grammar (#5167)

This PR adds options to add additional ground terms to the SyGuS instantiation grammars.

Update theory of arithmetic to standard check (#5178)

This updates the theory of arithmetic to use the standard check callbacks (preCheck, postCheck, preNotifyFact, notifyFact). It also refactors some use of the non-linear solver which will solely live in TheoryArith.

The longer term goal is to have TheoryArithPrivate be responsible for linear arithmetic solving only, and to be treated as a black box. Eventually, the non-linear solver will be removed from this class.

This PR is required for several things, including refactoring of preprocessing and expand definitions for arithmetic (div/mod will not be eliminated eagerly). It is also required for fixing issues related to div/mod appearing in instantiations.

This is the last class to have a custom check method. Followup PR will make Theory::check non-virtual.

FloatingPoint: Add utility functions for largest and smallest normal. (#5174)

Allow to use the initial assignment for CAD (#5177)

While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.

(proof-new) Preprocessing passes use proper interfaces to assertions pipeline (#5164)

This PR eliminates all uses of assertions pipeline that are not proper, which two-fold:
(1) The assertion list should never be modified in a custom way (without going through replace / push_back),
(2) Places where an assertion is "conjoined" to an existing spot in the vector should use conjoin instead of replace.
This is required for proper proof generation.

This fixes CVC4/cvc4-projects#75.

Make SygusSolver use sygus attributes directly (#5172)

Previously, the SmtEngine was using an interface through TheoryEngine to set user attributes to indicate that e.g. a synth-fun is associated with a given grammar. Since SmtEngine and its members are internal now, this can simply be done directly via attributes. This makes it so that SygusSolver does not depend on TheoryEngine nor does it require the TheoryEngine to be initialized at the time a synth-fun is created.

Add GH action to cancel previous pending/running CI builds. (#5175)

GH introduced a new workflow event pull_request_target that now makes it
possible to cancel builds on the base repository.

BitVector: Extend interface of setBit to set it to a specific value. (#5173)

Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.

FloatingPoint: Add utility functions for largest and smallest subnormal. (#5166)

Remove too strict assertion to allow for approximate models (#5168)

This PR simply removes an assertion that would trigger whenever the arithmetic theory asserts a model that contains something else than a constant. This can be the case with witness terms.
In offline discussion we concluded that this discussion was overly strict. Note that these examples may still hit an error during model validation (Cannot run check-model on a model with approximate values.).
This PR also fixes a debug output I found during debugging.

Fixes #5113.

Add missing includes. (#5170)

The strategy class added in #5160 was missing the proper includes for std::ostream. For some reason it works for most configurations, but triggers compilation errors in certain cases.

Add strategy for nonlinear extension (#5160)

This PR adds a flexible strategy for the nonlinear extension that replaces the handwritten code in checkLastCall().

Dynamic allocation of equality engine for shared solver (#5152)

This updates shared solver to have dynamic allocation of equality engine, analogous to theory solvers.

(proof-new) Add the term conversion sequence generator (#5097)

This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.

[proof-new] Adds a proof manager for prop engine (#5162)

Also fixes some weird orderings in src/CMakeLists.txt

Fix bags headers (#5165)

Fix bags headers

(proof-new) Add proof managers and eager gens to arith (#5159)

This commit threads ProofNodeManager, EagerProofGenerator, etc
throughout the arith theory into the appropriate locations. These
objects are currently unused, but will be used in future commits.

Crediting Andy, since he set up some of this.

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com

(proof-new) Fixes for preprocess proof generator and proofs in assertion pipeline (#5136)

This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.

Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.

[proof-new] Adds a proof post processor for the Prop Engine (#5161)

The post processor connects the two proofs in the prop engine: the refutation proof in the SAT solver and the CNF transformation proof in the CNF stream. The proof generators from theory engine in the latter are also expanded during the connection.

[proof-new] Updates to proof node updater (#5156)

[proof-new] Adds a proof-producing CNF converter (#5137)

A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).

Clean up nonlinear extension (#5149)

This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager.

Reset assertions on resetAssertions (#5153)

The assertions object is currently not cleared on resetAssertions, only the prop engine is reset. This means that if a user added assertion, did not use them in a check-sat, and then called reset-assertions, they would not be removed from the assertions pipeline (storing the pending assertions before they are sent to the prop engine).

This fixes #5144.

Add utilities for arith/proof_checker and build it (#5157)

The arith proof checker was not being built (not in cmake). Now it is. A
few dependencies were missing.

[proof-new] Removing spurious forward declaration in CnfStream (#5155)

[proof-new] Adds a proof node hash function (#5154)

Disable regression that is timing out (#5142)

Seems to be timing out on 1/5 of our CI runs currently.

Minor fixes to quantifiers proofs (#5151)

Includes minor changes to the proof checker and a fix in the instantiate module.

[proof-new] Adds a proof manager for the SAT solver (#5140)

Tracks the refutation proof built by Minisat. See the header for extensive explanations.

This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).

Implement bags rewriter (#5132)

This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes.
Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).

Add new arithmetic BoundInference class (#5148)

This PR adds a new utility class that extracts bounds on single variables from theory atoms like x > 0 or y <= 17. It does not perform further reasoning (like recognizing x > y with y > 3 as a bound).
Note that the functionality was introduced in arith/nl/icp/variable_bounds.h, but is now available using Node only.
This PR also replaces the VariableBounds by BoundInference in the icp solver which allowed for checking the code.

Fix sygus quantifier elimination preprocess for multiple functions (#5130)

The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.

Use inference manager for nl_solver (#5125)

This PR migrates the nl_solver part of the nonlinear extension to use the new inference manager as well.
It adds a new method clearWaitingLemmas to the inference manager and uses ArithLemma (though NlLemma exists) as we don't need the additional functionality of NlLemma.

Connect the shared solver to theory engine (#5103)

This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.

It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.

This PR has no intended behavior changes.

FYI @barrettcw

Use original quantified formula for single invocation reconstruction (#5129)

This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.

Restrict bvxnor to only allow two operands (was n-ary). (#5138)

Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in
SMT-LIB. We  now restrict bvxnor to only allow two operands in order to
avoid confusion about the semantics, since the behavior of n-ary
operands to bvxnor is now undefined in SMT-LIB.

Make sygus refinement step more robust to unevaluatable counterexamples (#5102)

Currently, the CEGIS refinement loop of the sygus solver may terminate with "unknown" when a duplicate counterexample is generated. This is caused by a candidate t for a conjecture exists f. forall x. G[f, x] such that:

(1) G[t, c] evaluates to a non-constant expression,
(2) ~G[t, k] is satisfiable with model k = c.

Notice this exclusively limited to theories with incomplete functions, e.g. (non-linear) division.

In this case, we know that t is an incorrect solution, but the counterexample we found was not new.

Currently, we abort with "unknown" since the counterexample was not new. After this PR, we exclude t and continue, which is uncontroversially the correct behavior.

This PR moves the resposibility for lemma from synth engine to synth conjecture, which simplifies the behavior of the main check conjecture method.

Cleaning and documenting cnf stream (#5134)

Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.

SyGuS: Add default grammar for FP. (#5133)

 Function definition fmf preprocessing pass (#5064)

This defines the function definition finite model finding as a proper preprocessing pass.

This is required for cleaning/fixing bugs in the preprocessor on proof-new.

There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines.

Modify lemma vs fact policy for datatype equalities (#5115)

This changes the lemma vs fact policy for datatype equalities. Previously, datatype equalities were sent as lemmas unless they were over datatypes that were composed of datatypes only. This is now changed so that equalities that do not involve direct subterms with finite non-datatype types are kept internal.

The primary type of equality that this targets are "Instantiate" equalities, e.g. the conclusion of:
(is-cons x) => x = (cons (head x) (tail x))
These equalities have been observed to generate large amounts of new terms for many benchmarks.

With this PR, the the challenging Facebook benchmark goes from 2 min 45 sec -> 29 sec. If the instantiate rule is disabled altogether, it still correctly solves, and is faster (~14 seconds), which however is not correct in general.

This change triggered two other issues:
(1) A relations benchmark involving transitive closure now times out. This has been a common issue for the relations solver and should be revisited.
(2) A potential issue with doPendingLemmas in InferenceManagerBuffer was uncovered. In rare cases, we can be re-entrant into this method since OutputChannel::lemma may trigger further preregistration of terms, which can trigger a recursive call to doPendingLemmas in the case of datatypes, which causes a segfault due to corrupting an iterator. This PR adds a simple guard for this method.

This PR also fixes some existing issues in computing cardinality for parametric datatypes.

Disable cegqi-bv when using sygus (#5124)

This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.

I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).

Make IAND solver use inference manager. (#5126)

This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.

Missing format from #5112.

bv2int: new options for bvand translation (#5096)

Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):

bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).

Allow E-matching by default when strings are enabled (#5117)

This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.

Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.

New C++ API: Catch and throw recoverable exception. (#5122)

This allows to distinguish recoverable from non-recoverable exceptions,
and recover if possible.

FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)

For the same reason as in #5119.

Refactor Commands to use the Public API. (#5105)

This is work towards eliminating the Expr layer. This PR does the following:

Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.

Fix type issue with term formula removal (#5107)

We currently are using lookups with uint32_t but storing with int32_t. Somehow the compilers don't complain, but I noticed this was mismatched.

[Python API] Conversion to/from Unicode strings (#5120)

Fixes #5024. This commit adds a conversion from constant string terms to
native Python Unicode strings in Term.toPythonObj() and improves
Solver.mkString() to accept strings containing characters outside of
the printable range.

FP: Use Assert instead of PRECONDITION macro in converter. (#5119)

The FP converter (= word blaster) uses a PRECONDITION macro that is
defined in symFPU (if included) and calls traits::precondition. This is
a problem for two reasons. First, traits::precondition calls
AlwaysAssert, and PRECONDITION is called for every word-blasted node, so
this can be expensive. Second, in case of an assertion failure, we get
very generic failure messages, that don't allow to distinguish between
failures and are absolutely non-descriptive:

Check failure

b
This fixes both issues.

@martin-cs

Add simple BV solver (#5065)

This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.

Add skeleton for theory of bags (multisets) (#5100)

This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.

Fix compilation without LibPoly (#5118)

Commit e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.

Add method to get Python object from constant value term in Python API (#5083)

This PR addresses issue https://github.com/CVC4/CVC4/issues/5014. It simply interprets the SMT-LIB string representation and produces a Python object. It currently supports booleans, ints, reals, bit-vectors, and arrays. The method (`toPythonObj`) is only valid to call if `isConst` returns true.

Update copyright header script to support CMake and Python files (#5067)

This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.

ICP-based solver for nonlinear arithmetic (#5017)

This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.

Require dumping in a dumping test (#5108)

Add ; REQUIRES: dumping to a dumping test.
Fixes nightlies.

(proof-new) Add the arrays proof checker (#5047)

Includes adding the standard method for constructing the extensionality skolem using the skolem manager.

More flexible design for model manager distributed (#4976)

This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.

This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.

This PR is not intended to make any behavior changes to the current architecture.

Standardize equality engine notifications in sets (#5098)

Fix assertion list for globally defined recursive functions (#5084)

This was uncovered by a (spurious) proof checking failure on proof-new.

Add the shared solver (#4982)

This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine.

In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase.

In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral).

FYI @barrettcw

bv2int: quantifiers support (#5080)

This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.

Fix muzzled builds (#5093)

Commit 2c2f05c moved some function
definitions from dump.h to dump.cpp, which is good. However, the
corresponding definitions for muzzled builds weren't moved, so muzzled builds
defined the operator << multiple times. This made our nightly
competition build fail. This commit fixes the issue by moving the
alternative definitions to the source file as well.

[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)

Extends Theory Proof Step Buffer. These utilities are used so that we can account for the fact that Minisat silenly does these transformations on added clauses.

Logic exception for arrays indexed by arrays (#5073)

This throws a logic exception when a term of array type whose index is also an array is registered to the theory of arrays.

It refactors the preRegisterTermInternal method of arrays so that all non-equality terms are added to the equality engine in the same block of code, which also checks for the type.

Fixes #4237.

FYI @barrettcw

[Strings] Fix extended equality rewriter (#5092)

Fixes #5090. Our extended equality rewriter was performing the following
unsound rewrite:

(= (str.++ Str13 Str5 Str16 Str13) (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")) ---> (and (= (str.++ Str13 Str5) Str5) (= (str.++ Str16 Str13) (str.++ Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")))
The rule being applied was SPLIT_EQ_STRIP_R. The rewrite was applied
due to the following circumstances:

The rewriter found that (str.++ Str13 Str5) is strictly shorter than (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")
The rewriter stripped the symbolic length of the former from the
latter
stripSymbolicLength() was only able to strip the first component, so
there was a remaining length of (str.len Str13)
The rule SPLIT_EQ_STRIP_R, however, was implicitly assuming that the
symbolic length can either be stripped completly or not at all and was
not considering the case where only a part of the length can be
stripped.

The commit adds a flag to stripSymbolicLength() that makes the
function only return true if the whole length can be stripped from the
input. The commit also refactors the code in stripSymbolicLength()
slightly.

Note: It is not necessary to try to do something smart in the case where
only a partial prefix can be stripped because the rewriter tries to
apply the rule to all the different prefix combinations anyway.

(proof-new) Updates to proof node updater algorithm (#5088)

This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.

This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.