Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)

This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.

This addresses CVC4/cvc4-projects#113.

Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:

QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.

Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.

Simplify and fix care graph for ufHo (#4924)

We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.

Fixes #4990.

Remove BV equality slicer (#4928)

This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.

FYI @aniemetz @mpreiner

Add TheoryState objects to each Theory (#4920)

This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).

Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.

Notice this PR does not update the theories to use these states yet, it simply adds the objects.

Split QuantElimSolver from SmtEngine (#4919)

Towards refactoring SmtEngine / converting Expr -> Node.

Simplify trigger notifications in equality engine (#4921)

This is further work towards a centralized approach for equality engines.

This PR merges the eqNotifyTriggerEquality callback with the eqNotifyTriggerPredicate callback, and adds assertions that capture the current behavior. It furthermore makes addTriggerEquality private in equality engine and invoked as a special case of addTriggerPredicate. Note this PR does not impact the internal implementation of these methods in equality engine, which indeed is different.

There are two reasons to merge these callbacks:
(1) all theories implement exactly the same method for the two callbacks, whenever they implement both. It would be trivial to do something different (by case splitting on the kind of predicate that is being notified), and moreover it is not recommended they do anything other than immediately propagate the predicate (regardless of whether it is an equality).
(2) It leads to some confusion with eqNotifyTriggerTermEquality, which is invoked when two trigger terms are merged.

Remove example theory (#4922)

This code is unused and obsolete.

Add strings-exp to regression (#4923)

str.at expands to str.substr, thus this benchmark (may) require strings-exp if things do not rewrite/preprocess. This triggers a regress0 failure on proof-new currently.

(cad solver) Add a partial check method. (#4904)

This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...

Make sets and strings solver states inherit from TheoryState (#4918)

This is towards the new standard for theory solvers.

This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.

Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).

Require `--strings-exp` when using `str.substr` (#4916)

Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.

Changes assertion (about maximum set cardinality) to an exception. (#4907)

Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.

[Regressions] Do not test `--check-proofs` anymore (#4914)

In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.

Fix SmtEngine::reset() (#4917)

Calling (reset) multiple times produced parsing problems (#4866) and could probably lead to all kinds of interesting issues.
In a nutshell, reset() failed to properly reset d_initialOptions (which is used to properly reset d_options) so that all options defaulted after the second call to reset().
This PR properly sets d_initialOptions after a reset (and the filename as well).

Fixes #4866.

Refactor functions that print commands (Part 2) (#4905)

This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.

(proof-new) Theory preprocessor proof producing (#4807)

This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.

Introduce the theory state object (#4910)

This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods.

The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers.

The next step will be to have the SolverState objects in theory of sets and strings inherit from this class.

Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)

This is work towards a configurable approach to equality engine management. This PR does not change any behavior, it only reorganizes the code.

This PR introduces the standard template for collectModelInfo, which isolates the usage of equality engine in relation to the model. In the future, theories will be encouraged to use the standard template for collectModelInfo and override collectRelevantTerms/collectModelValues only. This is to allow custom theory-independent modifications to building models (e.g. don't assert equality engine to model if we are using a centralized approach).

This PR standardizes TheoryArrays and TheoryDatatypes custom implementation of collectRelevantTerms as work towards using the standard template for collectModelInfo. Notice this required separating two portions of a loop in TheoryArrays::collectModelInfo which was doing two different things (collecting arrays and relevant terms).

(proof-new) Minor updates to trust node (#4900)

(proof-new) SMT proof postprocess callback (#4883)

This is the callback class for processing the final proof, which connects proofs of preprocessing and expands unwanted macro steps based on proof granularity mode.

The next step will be to add the ProofNodeUpdater that uses this callback and runs final sanity checks for checking proofs.

Quantifiers engine stores a pointer to the master equality engine (#4908)

This is work towards a configurable approach to theory combination.

Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.

Split SygusSolver from SmtEngine (#4891)

This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.

This PR updates Expr -> Node for the sygus interface in SmtEngine.

SmtEnginePrivate is no longer needed and is deleted with this PR.

Add the relevance manager module (#4894)

This PR adds the relevance manager module, which will be used in forthcoming PRs to query assignments for whether a literal is "relevant" (e.g. critical for satisfying the input formula). Leveraging this technique has led to noticeable improvements for non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager).

This PR does not enable it, but adds the module only.

(proof-new) Callbacks for term-context-sensitive terms (#4842)

Callbacks for term-context-sensitive terms.

It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.

These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.

Add identifier name for side condition. (#4902)

```
(! sc (^ ...)
      ^ this is the identifier!
```

We require that side-conditions have an identifier. We usually provide
this identifier, but in this one case we did not.

The old lexer accepted the side condition without the identifier. The
new one does not.

[CI] Update package list (#4906)

Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.

Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.

(proof-new) Prepare the theory of strings for proof reconstruction (#4885)

This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.

Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.

For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.

This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.

Add non-emptiness to conclusion of positive RE star unfolding. (#4899)

A recent commit (77e9881) simplified the form of the conclusion in regular expression star unfolding for the sake of uniformity in our internal proof calculus. However, this led to a noticeable drop in performance on a few specific RE benchmarks (the Norn set). This preserves the old behavior by extending the core rule for RE unfolding.

It also makes one minor change to the strings proof checker carried over from the proof-new branch.

(cad solver) Use the current model as initial assignment (#4893)

This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.

Minor cleanup related to notifications (#4898)

This includes eliminating TheoryBV's call to eqNotifyNewEqClass and fixing an issue with string's eqNotifyNewEqClass method, which was registering constant integers.

It also removes some unnecessary methods in Theory.

Add finishInit method to PropEngine (#4895)

This changes an initialization issue in regarding PropEngine and TheoryEngine.

In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.

The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.

(proof-new) Add the strings proof checker (#4858)

It also adds enumeration for two new rules that have been recently added.

Simplify equality engine notifications (#4896)

Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.

TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.

This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.

correctly parse sygus lang option (#4884)

--lang sygus is a synonym for --lang sygus2
also fixes typo in error message for language options parsing

Signed-off-by: polgreen <epolgreen@gmail.com>

Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)

This PR adds a small improvement to the CAD solver.
In Algorithm 4 of https://arxiv.org/pdf/2003.05633.pdf in lines 8 and 9, we only consider polynomials for resultant computations that have roots outside of the current interval.
This PR implements this check.
Fixes CVC4/cvc4-projects#210.

Split SmtSolver from SmtEngine (#4880)

This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.

This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).

Fixes for corner case of decision tree learning with different types (#4887)

There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.

Fixes regress1.

More basic fix for dumping synth-fun (#4886)

The commit (079a04b) appears to have broken the nightlies due to compile issues related a necessary addition to the Dump class (so that std::string could be printing on Dump streams).

This changes the temporary solution so that we simply print a string on the standard output, when the Dump is enabled. This is required for temporarily keeping dump=raw-benchmark working for synth-fun commands.

Add the distributed equality engine manager (#4867)

This is the first step towards making the approach for theory combination in CVC4 configurable.

This PR introduces the "distributed equality engine manager", which encapsulates the current policy that TheoryEngine uses regarding equality engines: each Theory creates a separate copy of an equality engine. The eventual plan is that the official equality engine of Theory is not necessarily unique to the theory, if equality engines are shared. A variant of this class could implement that policy.

This PR does not impact the code, it simply adds the definition of the class. A forthcoming PR will integrate this class into TheoryEngine, which will use dynamic allocation for equality engine objects.

FYI @barrettcw

[proof-new] Adding support for corner case of transitivity simulating MERGED_THROUGH_CONSTANTS (#4879)

generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)

Now that we are using the constant folding in equality engine for more than equality it is necessary to generalize the previously-hard-coded handling of MERGED_THROUGH_CONSTANTS.

Refactor functions that print commands (Part 1) (#4869)

This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.

Fixes for degenerate case of sygus decision tree learning (#4800)

Fixes #4790.

Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.

(proof-new) Improve robustness of CONG rule (#4882)

This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).

(proof-new) Proof support in the strings term registry. (#4876)

Adds basic support for proofs in the strings term registry. This code is not yet active until further parts of proof-new are merged.

(proof-new) Improve interfaces to proof generators (#4803)

This includes configurable naming and a caching policy for term conversion proof generator.

Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.

Add option to only build library (#4801)

This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API.

It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.

(proof-new) Witness form proof generator (#4782)

This class is responsible for the connection between terms and their witness form in the final proof.

Add naive support for integer variables. (#4835)

This PR adds naive support for integer reasoning to the CAD-based solver.
Essentially, it checks whether the sampled value is integral. If this is not the case, we "invent" a new interval covering the area between the two neighbouring integers with appropriate border polynomials.

(proof-new) Improving proof-production in Equality Engine (#4871)

This commit improves functionalities of the equality engine so that it is easier to produce proofs for its reasoning. They are:

avoiding assertion of already entailed predicates/equalities.
better EqProof of disequalities with constants
correct EqProof involving n-ary congruence kinds

Fix connection to master equality engine in sets (#4877)

This corrects an issue introduced by a merge of a previous commit (b5b2858) which dropped the connection from sets to its master equality engine.

Fixes several issues in sets regressions, including a timeout in regress0.

Fix infinite loop in arith_ite_simp (#4805)

We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on

(declare-fun a () Int)
(declare-fun b () Int)
(assert
    (and
        (= 1 (+ a b))
        (or (= 0 a) (= 0 b))
        (or (= 0 b) (>= b 8))
        (or (= 0 a) (not (>= b 8)))
    )
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.

Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.

Fixes #789.

Fix unsupported option in regress1. (#4874)

Fixes regress1.

Split SmtEngineState from SmtEngine (#4855)

This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).

Prepare theory of sets for dynamic allocation of equality engine (#4868)

In forthcoming PRs, Theory objects will be assigned equality engine objects dynamically.

This PR prepares the theory of sets for this update, which involves refactoring of its internal members.

Final preparations for changing API to use the Node-level datatype (#4863)

This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.

After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.

(proof-new) Extensions to proof checker interface (#4857)

This includes support for pedantic levels, as well as a utility for wrapping Kind in a Node (for the updated CONG rule, to be updated in a later PR).

Update Expr-level unit tests that depend on datatypes to Node (#4860)

In preparation for eliminating the Expr-level datatype.

Remove instantiation model true option (#4861)

This was an option that rejected instantiations that are true according to the current
model's equality engine.

This option was never helpful and will be burdensome to maintain with new updates
 to equality engine infrastructure.

New C++ API: Remove redundant API functions for mkReal. (#4870)

This further removes redundant API functions with a `const char*`
parameter. These are redundant (and can create ambiguity) since they
have `const string&` counterparts.

Make valuation class more robust to null underlying TheoryEngine. (#4864)

In some use cases (unit tests, old proofs infrastructure), we use a Theory with no associated TheoryEngine. This PR makes the Valuation class more robust to this case.

This includes making the "unevaluated kinds" a no-op in this case (this is necessary for Theory::finishInit with no TheoryEngine) and adding some assertions to cases that the Theory should never call without TheoryEngine.

This is required for a new policy for dynamically configuring equality engine infrastructure in Theory.

Splitting a few utility classes from EqualityEngine to their own file (#4862)

Includes iterators and notification callbacks. These classes will be highly relevant for planned extensions to the core theory engine infrastructure.

Move datatype index constant to its own file (#4859)

Towards removing the Expr-level datatype.

Moves DatatypeIndex to its own file, which is the only thing that is necessary remaining from expr/datatype.h.

Also updates the datatype kinds file in preparation for the removal.

GH Actions: Remove cancel action. (#4843)

The previously introduced action to cancel running builds is not able to
cancel builds on other branches, only on the same branch. As a consequence,
when pushing to a branch for which a PR has been submitted, builds on the
main repository are not cancelled.

This removes the cancel build. If we want behavior similar to how it was
on Travis, we need a workaround / more sophisticated solution since GH
Actions doesn't really allow / support this (due to permission issues).

Updates not related to creation for eliminating Expr-level datatype (#4838)

This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.

This required updating a unit test from Expr -> Node.

Split preprocessor from SmtEngine (#4854)

This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).

It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.

(proof-new) Refactor regular expression operation (#4596)

This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.

Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.

Split Assertions from SmtEngine (#4788)

This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.

Improve error message for unsupported exponents (#4852)

We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692

When checking models, ensure that error message is correctly formatted (#4853)

Issue
When CVC4 is checking models and encounters an issue, it presents an message like this:

Internal error detectedTHEORY_ARITH has an asserted fact that the model doesn't satisfy.
Notice: there's no space between detected and THEORY_ARITH.

Resolution
This PR ensures that the error message is correctly formatted.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com

[Strings] Add eager context-dependent evaluation (#4847)

This commit adds eager evaluation of string terms based on the current
context. To do so, it declares the string kinds to be "interpreted" in
the equality engine. This allows us to avoid making a series of
decisions such as:

** (= "describe" (str.substr actionName 0 8)) :DE-DECISION:
*** (= actionName "deletecertificate") :DE-DECISION:
**** (= resource_partition "aws") :DE-DECISION:
***** (= resource_region "af-south-1") :DE-DECISION:
****** (= resource_account "") :DE-DECISION:
******* (= (str.len (str.substr actionName 0 3)) 0) :DE-DECISION:
******** (= (str.len (str.substr actionName 0 4)) 0) :DE-DECISION:
********* (= (str.len (str.substr actionName 0 6)) 0) :DE-DECISION:
********** (= (str.len (str.substr actionName 0 5)) 0) :DE-DECISION:
*********** (= (str.len (str.substr actionName 0 9)) 0) :DE-DECISION:
************ (= (str.len (str.substr actionName 0 7)) 0) :DE-DECISION:
************* (= (str.len (str.substr actionName 0 10)) 0) :DE-DECISION:
************** (= (str.len (str.substr actionName 0 2)) 0) :DE-DECISION:
*************** (= (str.len (str.substr actionName 0 13)) 0) :DE-DECISION:
**************** (= (str.len (str.substr actionName 0 12)) 0) :DE-DECISION:
***************** (= (str.len resource_service) 0) :DE-DECISION:
****************** (= (str.len resource_account) 0) :DE-DECISION:
In such a case, we can detect that there is a conflict after the first
two decisions because (str.substr "deletecertificate" 0 8) is
deletece which is different from describe. The equality engine uses
the rewriter to evaluate interpreted kinds with constant arguments.

This technique leads to a significant speedup on some of the newer
Amazon benchmarks.

Add dummy returns if libpoly is unavailable. (#4845)

This PR adds dummy return statements do CadSolver in case libpoly is not available.

Fixes for getInterpolant and getAbduct API methods (#4846)

This fixes three issues in the getInterpolant method in the API, which was also copied to the getAbduct method:
(1) Use Node not Expr
(2) Must set up ExprManager scope
(3) The wrong solver pointer was passed to the returned term, which was causing segfaults on all abduction regressions.

We should also consider changing the interface of this method to return the term instead of a Boolean. This could be done as future work.

This fixes regress1.

Add documentation and build instructions for recompilation (LGPL). (#4844)

Modify the smt2 parser to use the Sygus grammar. (#4829)

Add API interface for specialized constructor term (#4817)

This is an interface to get the instantiated parametric datatype constructor operator to apply when the type of this operator cannot be inferred without a cast.

This is required for eliminating the Expr-level datatype and calls to ExprManager from the parsers.

Properly initialize d_fullyInited. (#4840)

Fixed #4839.
The Boolean flag d_fullyInited is not properly initialized and is thus flagged by --ubsan.

Add CAD-based solver (#4834)

Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail:

add --nl-cad option
add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation
add new Inference types for the NlLemma class
use CadSolver in NonlinearExtension (if --nl-cad is given)

Update documentation for Solver::mkVar() (#4833)

The documentation of `Solver::mkVar()` was not very clear regarding what
it could be used for. This lead to some confusion (see e.g. #4828).
This commit makes the documentation more explicit.

Add implementation for SyGuS interpolation module (step4) (#4811)

This is the 4th step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The 4th step finished the implementation of the interpolation module.

New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769)

This PR adds new rewrite rules for BV.
None of them is meant to be used by the default BV rewriter.
However, they are planned to be used in bv_to_int preprocessing pass.
In the pass we use FixpointRewriteStrategy to call various rewrite rules.
After consulting @4tXJ7f , we thought that the best way to include more rewrite rules in that call is to implement them using the existing BV rewrites infrastructure.

Generalize interface for candidate rewrite database (#4797)

This class will be used as a utility in a new algorithm for solution reconstruction and requires a generalized interface.

FYI @abdoo8080

Update datatypes in cvc parser to the new API (#4826)

This is leftover from the parser conversion. This is towards eliminating all remaining Expr-level calls in the parser.

Notice that 2 parser-level checks for records are eliminated in this PR, since we do not export record objects in the new API.

Examples for using sygus python api (#4822)

This PR adds examples for using the sygus python api.
The examples are obtained from the examples of the cpp sygus api.

Delete solver pointer in Cython __dealloc__ (#4799)

Split expression names from SmtEngine (#4832)

Towards splitting SmtEngine / deleting SmtEnginePrivate.

Split dump manager from SmtEngine (#4824)

Towards splitting SmtEngine.

This moves utilities related to managing information for dumping to its own utility, DumpManager.

Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.

Updates to dtype constructor in preparation for eliminating Expr-level datatype (#4825)

Fix ASan failure in interactive_shell_black (#4827)

This commit fixes an issue reported by ASan for unit test
interactive_shell_black. The unit test was failing because nodes were
created in the wrong node manager. The issue was likely introduced with
e8bbee7.

Ensure strict length constraint for decompose rule (#4821)

Fixes #4820. The performance issue was caused by
0988217562006d3f59e01dc261f39121df6d75f5. That commit introduced an
option (`--strings-len-conc`) that optionally moves the length
constraint for skolems to the conclusion of an inference instead of
making it part of the term registration. However, for
`DEQ_DISL_STRINGS_SPLIT`, we were only asserting that `LENGTH_GEQ_ONE`
in the case where this option was not enabled, instead of asserting that
the length of the skolem is equal to the component on the other side of
the disequality. This lead to an infinite loop of inferences because we
effectively were just splitting a component into two skolems and the
only restriction was that the first one was non-empty. We guessed the
second skolem to be empty, so the first skolem was equal to the
component, the skolem was marked congruent, and we ended up with the
same normal form as before.

The commit fixes the issue by adding an argument to
`getDecomposeConclusion()` that specifies whether to add the length
constraint or not. This option is used to always add the length
constraint in the case of `DEQ_DISL_STRINGS_SPLIT`.

Add methods for constructing datatype types from NodeManager (#4823)

This is work towards eliminating the Expr-level datatype.

This PR implements the required methods for constructing datatype types from NodeManager.

In particular, this PR copies the "mkMutualDatatypeTypes" methods and converts them to Node-level.

The next PRs will be in preparation for using these methods instead of the Expr-level ones.

It also adds a flag d_isRecord to DType, which is required for supporting record printing in the cvc printer, which will be updated in another PR.

It also eliminates an interface for constructing constructor types via Expr-level DatatypeConstructor objects, which was unused.

Ensure that we only find '.a's when building statically (#4785)

## Issue

When trying to building statically, and if your machine *does not* have static libraries (e.g., there is [no static GMP on CentOS 8](https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/8/html-single/considerations_in_adopting_rhel_8/index#removed-packages_changes-to-packages)), then CVC4's CMake does not detect this:

```
FAILED: bin/cvc4
: && /usr/bin/c++  -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -Wno-class-memaccess  -fuse-ld=gold   -static src/main/CMakeFiles/main.dir/command_executor.cpp.o src/main/CMakeFiles/main.dir/interactive_shell.cpp.o src/main/CMakeFiles/main.dir/signal_handlers.cpp.o src/main/CMakeFiles/main.dir/time_limit.cpp.o src/main/CMakeFiles/cvc4-bin.dir/driver_unified.cpp.o src/main/CMakeFiles/cvc4-bin.dir/main.cpp.o  -o bin/cvc4  src/libcvc4.a  src/parser/libcvc4parser.a  src/libcvc4.a  -Wl,-Bdynamic  /usr/lib64/libgmp.so  -Wl,-Bstatic  ../deps/install/lib/libantlr3c.a && :
/usr/bin/ld.gold: error: cannot mix -static with dynamic object /usr/lib64/libgmp.so
```

## Resolution

This PR changes CVC4's CMakeLists such that, if you're building statically, it *only* allows for linking against `.a`s (or `.a`s + `.lib`s on Windows).

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

Fix component contains for splicing due to substring. (#4705)

Fixes #4701. That benchmark now times out.

Add SyGuS Python API (#4812)

This commit extends the Python API with support for SyGuS functionality.
This required the addition of a nullary constructor for `Grammar` in the C++ API.
A unit test is also included, and is a translation of the corresponding C++ API unit test.

Examples are not added yet, but are ready and planned for a next PR (in order to keep this one shorter).

Split listener classes from SmtEngine (#4816)

This moves listener classes owned by SmtEngine to their own file.

The SmtEnginePrivate class previously what itself a NodeManagerListener. This class will be deleted. Instead a new NodeManagerListener is introduced here whose sole responsibility is to do the work required for node manager listening.

Note I had to add a (temporary) friend relationship to SmtEngine, which will be removed in an upcoming PR to split the management of dumping to its own utility.

Standardize explanations in arrays (#4804)

Some internal inferences had a non-standard way of providing (disjunctive) reasons and a custom way of explaining them.

This PR simplifies the array solver so that its explanations are analogous to the other equality engine based theory solvers (strings, datatypes, sets, ...). This is done in preparation for the incorporation of the proof equality engine in arrays, which follows a standard design for reasons/explanations.

The performance impact on QF arrays is negligible

Python API: Add support for sequences (#4757)

Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support
for sequences. This commit extends that support to the Python API. It
also adds simple C++ and Python examples that demonstrate how the API
works for sequences.

Cad implementation (#4774)

This commit implements the CAD interface added in #4773.

Adds the interface for the CAD-based arithmetic solver. (#4773)

This PR adds some utilities and, most importantly, the interface of the new
CAD-based solver.
The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code
structure follows the paper rather closely.