Add missing stat for lemmas based on inferences (#4214)

Add safe_print() support for Kind enum (#4213)

This commit changes the mkkind script to generate a toString()
method for the Kind enum. This method can be used by the
safe_print() function to print statistics if CVC4 has been terminated
before solving a problem. The stats for strings include statistics that
rely on printing kinds (e.g. the number of reductions done of each
kind).

Type-independent preregistration of empty word (#4205)

Also removes another instance of empty string in TheoryStrings for consistency sake.

New C++ API: Remove Op::getSort(). (#4208)

Update theory rewriter ownership, add stats to strings (#4202)

This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:

- We can't have a single `Rewriter` instance shared between different
  `SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
  `SmtEngine` and calling the rewriter retrieves the rewriter associated with
  the current `SmtEngine`. This is a temporary workaround before we get rid of
  singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
  non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
  the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
  changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
  from `SequencesRewriter` and calls its `postRewrite()` before applying its
  own rewrites (this is essentially a reversal of roles from before: the
  `SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
  mirrors the `EqualityEngine`s owned by the individual theories.

Only rewrite lambdas via array representations when constant (#4203)

Fixes #4170.

Split sequences rewriter (#4194)

This is in preparation for making the strings rewriter configurable for stats.

This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas.

No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.

Remove undocumented/uncommon aliases (#4177)

This commit removes aliases that are either undocumented or associated
with uncommon options.

Note: The removal of --statistics, --language, and --output-language may be controversial. The options were undocumented previously and I am in favor of simplifying the options as much as possible, however. Please let me know what you think.

Introduce enums for all string inferences, excluding the core solver (#4195)

Introduce enum values for all calls to sendInference outside of the core solver.

This included some minor refactoring.

Initialize theory rewriters in theories (#4197)

Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).

Support char smt-lib syntax (#4188)

Towards support for the strings standard.

Adds support to (_ char #x ... ) syntax for characters.

Fix install for ANTLR contrib script and CI dependency caching. (#4196)

Rename checkValid/query to checkEntailed. (#4191)

This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.

Switch to GitHub actions for CI (#4190)

Enable CI with GitHub actions, add macOS builds and disable Travis CI.

Fix fmf benchmark (#4193)

Fixes regress1.

This benchmark is too delicate in the current state.

Remove replay and use-theory options and idl (#4186)

Towards disentangling Options / NodeManager / SmtEngine.

This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.

The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.

The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.

It also removes the solver in src/theory/idl, which cannot be enabled after this commit.

Fix strange bound regression (#4192)

Several things have happened with this regression lately, in chronological order:
(1) Instantiations involving bounded set quantifiers were changed to use choice to represent symbolic instantiations,
(2) fmf-bound was decoupled from finite-model-find (the latter is not enabled when the former is),
(3) choice was set to be an "unevaluated" kind (in 0060de3).

After (1) and (2), for the regression test/regress/regress1/fmf/fmf-strange-bounds.smt2, CVC4 was answering "sat" correctly but internally there was a source of incompleteness. In particular, a choice term was being generated in an instantiation that was later incorrectly evaluated, thus allowing CVC4 to skip an instantiation it shouldn't have.

The recent commit of (3) resolved this issue, making it so that choice is not an evaluated kind. This meant the benchmark went "sat" -> "unknown".

This PR fixes this issue by enabling --finite-model-find, which is now necessary to answer "sat".

It also adds a further test quantifier that was used in debugging this issue.

Fixes regress1.

Convert more uses of string-specific functions (#4158)

Towards theory of sequences.

Fixing regressions (#4189)

An option was recently deleted, forgot to disable it from a regression. Fixes a failure in regress1.

Rewrites for all remaining return statements in strings rewriter (#4178)

Towards proofs for string rewrites. All return statements all now associated with an enum value.

An indentation in a block of code changed in rewriteMembership.

Support indexed operators re.loop and re.^ (#4167)

Towards support for the strings standard.

This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).

This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.

Also fixes #4161.

Remove ref skolem datatype option (#4185)

Fixes #4180, fixes CVC4/cvc4-projects#133, fixes CVC4/cvc4-projects#134.

Add coverage badge. (#4187)

Coverage information is updated nightly.

Fix arguments to print callback (#4171)

The method applyParseOp may modify the argument vector. In the case of the sygus V1 parser, this argument vector was then being used to set up a print callback, leading to incorrect printing and failures.

Work towards having a working V1 -> V2 conversion for the release.

FYI @abdoo8080

Frontend support for the choice operator (#4175)

Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue

Enumeration for String rewrites (#4173)

In preparation for string proof infrastructure.

This introduces an enumeration type to track string rewrites.

It also makes inference printing more consistent.

Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)

Convert the last few Sygus benchmarks to V2. (#4172)

Stop printing datatype declaration for Sygus V1 grammar. (#4168)

Node traversal iterator (#3845)

Implement an iterator for pre- and post-order traversals.

I believe that this will be useful in pre-processing passes, many of
which do postorder traversals that they implement by hand.

Right now this iterator does not support modification of the traversal
pattern, but we could add this later on, if we want it.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

Split transcendental solver to its own file (#4156)

* Attempting to split transcendental function solver

* Clean

* Format

* More

* Format

* Attempt link

* Format

* Fix

* Another refactor

* More

* More

* Rename

* Format

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>

Fix issues with unsat cores and reset-assertions (#4159)

Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.

The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.

The regression test is an extension of the example in #4151 and covers
both issues.

Fix expected output on arith regression (#4162)

A benchmark went unknown -> sat, likely due to the arith-brab commit, thus leading to a failure on regress1.This updates the status on this benchmark (also adds --nl-ext-tplanes to it).

Move string utility file (#4164)

Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.

Do not require that function sorts are first class internally (#4128)

This PR removes the requirement in the NodeManager that argument types to the function sort are first class.

Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633

Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.

FYI @abdoo8080 .

Support unicode internal representation and escape sequences (#3852)

Work towards support for the strings standard.

This updates the string solver and parser such that:

The internal representation of strings is vectors of code points,
Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models,
The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings,
Handle unicode escape sequences according to the SMT-LIB standard in String,
Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary,
Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.

Move set defaults function to its own file (#4154)

This moves SmtEngine::setDefaults to its own file.

This design is not final. One could imagine this being a part of a "OptionsSetter" utility. I am leaving this as is until we refactor the relationship between SmtEngine and Options.

Regardless, the general file structure should be such that this method is separate from SmtEngine, since setting default options is a large task that should be addressed independently from the core of SmtEngine.

This is initial preparation towards converting the SmtEngine from Expr -> Node.

A few very minor changes were made to the code to make the separation possible.

Added unit-cube-like test for branch and bound (#3922)

* unit-cude test wip

* test for wip unit cube test

* fixed simple rounding

* wip

* Passing tests except for sat vs unknown ones

* added flag for cube test

* put example back to normal

* Fixed for style guidelines.

* fixed rewrite bug

* removed extra comments

* unit-cude test wip

* test for wip unit cube test

* fixed simple rounding

* wip

* Passing tests except for sat vs unknown ones

* added flag for cube test

* put example back to normal

* Fixed for style guidelines.

* fixed rewrite bug

* removed extra comments

* Small fixes based on PR feedback

* replace NodeManager::currentNM with nm and clang formatted

* renamed test

* Added a regression test that triggers branch and bound

* Added ; COMMAND-LINE: --arith-brab

* Updated arith-brab test

* arith-brab enabled by default

* Added --nl-ext-tplanes to regress0/nl/ext-rew-aggr-test.smt2

Co-authored-by: Amalee Wilson <amalee@cis.uab.edu>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

Disable slow regression (#4157)

Should fix timeout in asan build.

Add stats for string reductions, lemmas and conflicts (#4149)

This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).

Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.

Generalize more string-specific functions (#4152)

Towards theory of sequences.

Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field.

Care graphs based on polymorphic operators in strings (#4150)

Towards theory of sequences.

To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.

Support async-signal-safe printing of inferences (#4148)

Commit c9b7c3d introduced code for
counting the number of string inferences done per type of inference.
However, it did not add support for printing the inference names in an
async-signal-safe manner via safe_print() (note that printing in
signal handlers is done differently from the regular stats printing).
This commit adds the corresponding code, s.t. we get the inference names
when printing the stats when CVC4 is interrupted or crashes.

bv2int : linear mult opt (#4142)

 Generalize more uses of string-specific functions (#4145)

Towards theory of sequences.

Int2BV fail on demand (#4079)

This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.

Restrict partial triggers to standard quantified formulas (#4144)

Fixes #4143.

Restrict cases of sygus grammar reduction based on argument variants (#4131)

An assertion is triggered for some V2 versions of SyGuS V1 benchmarks during sygus grammar reduction. This PR updates this technique so that it only applies to sygus constructors whose sygus operators are lambdas of the form
lambda x1 ... xn. f( x1 ... xn ).

FYI @abdoo8080 .

Infer when sygus operators are equivalent to builtin kinds (#4140)

The V2 parser always turns sygus operators into lambdas for consistency. This PR ensures that we nevertheless infer when a sygus operator is equivalent to a builtin operator, e.g.
(lambda x y. (+ x y)) is equivalent to +.

The main reason this is required is to ensure that solution reconstruction heuristics work optimally when we make the switch SyGuS V1 -> V2 (see 5 failing benchmarks due to --cegqi-si=all on #4136).

Simplify auxiliary variable handling in CEGQI (#4141)

Fixes #3849 and fixes #4062.

Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables.

In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be:
(1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 )
(2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2).
Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities).

This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above.

Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.

Throw exception for non-well-founded unimplemented SyGuS types. (#4125)

Fixes #3931.

Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype.

Change transcendental function app slave list to unordered_set (#4139)

Fixes #4112.

Collect statistics about normal form inferences (#4127)

This commit adds code to count the number of inferences made of each
inference type for normal form inferences. It extends the Inference
enum in `infer_info.h` and adds two new `sendInference()` methods in the
`InferenceManager` to send and count inferences that have a corresonding
entry in the `Inference` enum.

Sort inference does not handle APPLY_UF when higher-order is enabled (#4138)

Fixes #4092 and fixes #4134.

Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.

Convert V1 Sygus files to V2. (#4136)

Simplify heuristic in `processNEqc` (#4129)

This commit removes a special case in `CoreSolver::processNEqc()` where
we stopped looking for inferences for a given normal form as soon as we
found the highest priority inference (currently that an element in the
normal form is empty). This effectively elevates the priority of this
inference to the other inferences that are done immediately instead of
being added to the `pinfer` vector that holds the possible inferences.
The experiments that I've run seem to confirm that it is unnecessary to
have this special case.

Don't run bv_nat parse test with competition build (#4126)

This commit should fix the nightlies.

Generalize mkConcat for types (#4123)

Towards theory of sequences.

The utility function mkConcat needs a type to know what to construct in the empty string case.

Fix variable shadowing issue in sygus-inference (#4121)

This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options.

Fixes #4083.

Fix sort comparison within assertion in cegis (#4113)

Guard cases of sort inference in quantifier free logics in uf cardinality (#4074)

Fixes #4068 and fixes #4085 and fixes #4063.

Split string-specific operators from TheoryStringsRewriter (#3920)

Organization towards theory of sequences.

The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.

Do not assign higher-order representative if function does not exist (#4073)

Handle failures for sygus QE preprocess (#4072)

If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.

Parse error for SyGuS version 1.0 vs 2.0 (#4057)

This adds a useful error message that recognizes a divergence in the expected input format (version 1 vs. version 2), which will be useful when we switch to SyGuS version 2 by default. This warning message is already potentially useful for users who are using --lang=sygus2.

Make handling of illegal internal representatives in quantifiers engine more robust (#4034)

Fixes #4002 (that benchmark is now unknown).

The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.

The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.

A block of code changed indentation in this PR, which was updated to the new standards.

Refactor enumerator for strings (#4014)

Towards theory of sequences. This separates out a virtual base class and utility class for the strings enumerator, which will be extended for sequences later.

Fix regression output related to sygus+bv-div-zero (#4122)

Bv2int fail on demand

Postpone failure in bv-to-int preprocessing pass.

Only apply testConstStringInRegExp to const regexp (#4120)

Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.

SyGuS must use total bitvector division (#4119)

Our SyGuS utilities are not designed to deal with partial bitvector division. If a user forced an older version of SMT-LIB semantics while using SyGuS, this led to a number of issues.

For now, we disable this option when it is combined with SyGuS, regardless of whether the user turns it on.

A more permanent solution will be to remove the old SMT-LIB semantics option bv-div-zero-const entirely.

Fixes #4097 and fixes #4088 and fixes #4104.

Only allow bv2nat/int2bv with BV and integer logic (#4118)

CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.

Remove spurious assertion (#4117)

Fixes #4106.

The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).

Explicitly handle isFinite for rounding modes (#4115)

The function TypeNode::isFinite is designed to compute finiteness without computing cardinality for the sake of efficiency; there was a missing case for rounding modes, leading to an assertion failure.

Fixes #4101.

Always enable cbqi literal dependency (#4116)

Fixes #4105.

It appears that the two (experimental) options in that issue were incompatible.

A block of code changed indentation in this PR and was updated to guidelines.

Fix issue with multiple infinities in CEGQI for LIRA (#4114)

Fixes #4086.

Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.

Move node visitor class from smt_util/ to expr/ (#4110)

Done by:

Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.

SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)

Remove AlwaysAssert(false) for hole.

clang-format

Fix simplicity check in prop

Fix antecedent loop. Whoops

Only save farkas+tightening proofs. Error on holes

I'll remove the error later

Expand the definition of a "simple" farkas proof.

Before, a "simple farkas proof" was one that just applied the farkas
lemma.

Now it allows for the antecedents to (optionally) be tightened.

Note that hasSimpleFarkasProof was (and is) dead code.

We will use it to decide whether to print a proof or a hole.

DecisionEngine: Use single unique pointer for ITE strategy . (#4078)

Previously, DecisionEngine maintained a vector of ITE strategies.
However, only one was ever created. This uses a single unique_ptr member
for the ITE strategy instead of a vector.

Issue 4077: Add unit test to reproduce issue. (#4107)

This adds the unit test reported in issue #4077.
The issue was fixed in #4081.

Create master equality engine at context level 0 (#4081)

Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.

Handle cases in --sygus-rr where evaluation is not constant (#4100)

Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant.

Fixes #4096 and fixes #4089.

Removing a few deprecated options (#4052)

Remove regress for real to int (#4071)

Missed this one when real to int was disabled for quantifiers. Fixes regress1.

Generalize type rules for strings to sequences (#3987)

Towards theory of sequences.

Fix case of non-constant value for sygus sampling (#4051)

Fixes #4050.

Add options for nec regression (#4056)

Currently an nec benchmark in regress2 is very slow (57 seconds in production) due to disabling the nec-specific options in 67c730c). This reenables these options for this benchmark.

Convert most instances of dataypes in parsers to the new API (#4054)

I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future:
(1) The sygus v1 parser will be deleted,
(2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 .

Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser.

The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.

Do not allow quantifiers over real variables in real to int pass. (#4049)

With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.

Remove local theory extension option (#4048)

This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.

Do not make models for quantified function variables (#4039)

If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.

New C++ API: Remove support for (reset). (#4037)

Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.

Ensure legal candidate equalities when using relational triggers (#4035)

Fix double notify in equality engine (#4036)

Fixes #3955.

Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.

This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.

A block of code changed indentation in this commit.