Move regular expression inclusion test to RegExpEntail (#4310)

In preparation for rephrasing this inference as a rewrite.

Change option names --default-dag-thresh and --default-expr-depth (#4309)

Split TermRegistry object from TheoryStrings (#4312)

This consolidates functionalities from TheoryStrings and InferenceManager related to registering terms, including sending "preregistration lemmas" for them. The main purpose of this PR is to detangle this module from InferenceManager so that these two modules have exactly one call to OutputChannel::lemma each.

For the purposes of the theory solvers, TermRegistry contains the official SkolemCache of TheoryStrings, and can be seen as subsuming the previous interface for this class.

This PR is needed for further progress on strings proofs, marking as major since this will be a blocker shortly for this project.

A few things were cleaned in this PR. One function changed name InferenceManager::registerTerm --> TermRegistry::getRegisterTermLemma. No major behavior changes.

Do not mark string extended functions as eliminated after reduction lemmas (#4306)

The current policy marked extended functions in strings as "reduced" (eliminated) when we generated their reduction lemma. The upside is that the solver can effectively ignore them. The downside is that we cannot do context-dependent simplification on them, and hence we miss out conflicts during the remainder of the check-sat call.

This changes the policy so they are not marked as reduced. Instead, reduction lemmas are cached in the standard way while allowing context-dependent simplification.

Fix assertion in enumerative instantiation (#4313)

Fixes regress1.

Convert more cases of strings to words (#4206)

Abort if in conflict in enumerative instantiation (#4298)

In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.

Fixes #4293.

Always flush lemmas from downwards closure in sets (#4297)

Fixes #4283.

This also makes a few minor improvements to how lemmas are sent in sets. In particular, lemmas are not sent if we are already in conflict.

Do not normalize to representatives for variable equalities in conflict-based instantiation (#4280)

Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.

Fixes #4275.

Always assign function values in higher order (#4279)

Fixes #4277.

Fix combinations of cegqi and non-standard triggers (#4271)

Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.

Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.

Disable preregistration of instantiations for cegqi in incremental (#4251)

Fixes #4243.

Disable macros when higher-order (#4266)

Fixes #4160.

Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)

Fixes #4228. That benchmark now times out.

Remove a few options (#4295)

These options are not robust and are not used.

Fixes #4282 and fixes #4291.

Remove a few spurious assertions (#4294)

Fixes #4290 and fixes #4292.

Remove early type check option (#4234)

Required to decouple options from NodeManager.

This option is now always enabled in debug, and disabled in production.

Remove argument extender (#4223)

This was a utility class for dynamically changing argc/argv.

Remove mergePredicates from EqualityEngine interface (#4305)

This function was equivalent to asserting an equality. Removing it for the sake of simplicity.

Fix dump-unsat-cores-full (#4303)

This adds a fix to ensure dump-unsat-cores-full works by modifying the public options function. This options currently does not work since dumpUnsatCores is only set internally now. This fix is only required until options are refactored so that SmtEngine owns the authoritative copy of options.

Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)

A recent change made it so that defined functions would print as the anonymous lambda corresponding to their definition if the SyGuS v1 parser was used. This was caused by comparison with the wrong kind in the new API.

Notice that the v2 parser does not have this issue.

This also adds a regression to ensure this behavior is maintained by the SyGuS v2 parser.

Fixes for extended rewriter (#4278)

Fixes #4273 and fixes #4274 .

This also removes a spurious assertion from the Node::substitute method that the result node is not equal to the domain. This is violated for f(f(x)) { f(x) -> x }.

Move slow nl regression to regress3 (#4276)

Should fix nightlies.

Add skip predicate to node traversal. (#4222)

Sometime you want to skip specific sub-DAGs when traversing a node. For example, you might be doing a transformation with a cache, and want to skip sub-DAGs that you've already processed.

This PR would add a skipIf builder method to NodeDfsIterable, which allows the user to provide a predicate according to which nodes will be omitted from the subsequent traversal.

Ensure exported sygus solutions match grammar (#4270)

Previously we were doing rewriting/expand definitions during grammar normalization, which overwrote the original sygus operators. The connection to the original grammar was maintained via the SygusPrintCallback utility, which ensured that a sygus term printed in a way that matched the grammar.

We now have several use cases where solutions from SyGuS will be directly exported to the user, including the current use of get-abduct. This means that the terms must match the grammar, and we cannot simply rely on the print callback.

This moves the code to normalize sygus operators to datatypes utils, where the conversion between sygus and builtin terms takes place. This allows a version of this function where isExternal = true, which constructs terms matching the original grammar.

This PR enables the SyGuS API to have an accurate getSynthSolution method. It also will eliminate the need for SygusPrintCallback altogether, once the v1 parser is deleted.

Split the non-linear solver (#4219)

This splits the "non-linear solver" from "NonlinearExtension". The non-linear solver is the module that implements the inference schemas whereas NonlinearExtension is the glue code that manages the solver(s) for non-linear.

This also involves moving utilities from the non-linear solver to their own file.

Explain non-emptiness by non-zero length in strings (#4257)

Several kinds of splitting lemmas in the strings solver can sometimes be avoided by observing that str.len(x) != 0 implies that x is non-empty. This generalizes the check for whether x is non-empty is explainable in the current context.

Add a few stats to strings (#4252)

To give an idea of the high-level behavior.

Towards proper use of resource managers (#4233)

Resource manager will be owned by SmtEngine in the future. This passes the resource manager cached by SmtEnginePrivate to the PropEngine created by SmtEngine instead of using the global pointer. It also makes a few preprocessing passes use the resource manager they already have access to and should use.

CI: Add a step to list dependencies. (#4255)

Disable slow sygus regression (#4232)

A regress2 SyGuS benchmark is taking 110 seconds in production on my machine. This was likely caused by the recent update v1 -> v2, which impacts the internal representation and hence the search. Disabling for now.

Split ProcessAssertions module from SmtEngine (#4210)

This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.

The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:

A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.

Added CHOOSE operator for sets (#4211)

This PR enables THEORY_UF by default for sets and adds the operator CHOOSE for sets which returns an element from a given set. The semantics is as follows:

If a set A = {x}, then the term (choose A) is equivalent to the term x.
If the set is empty, then (choose A) is an arbitrary value.
If the set has cardinality > 1, then (choose A) will deterministically return an element in A.

Perform theory widening eagerly (#4044)

Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().

Fix dump models and dump proofs (#4230)

A recent commit (45e489e) made it so that dump-models did not automatically enable produce-models in the global options object, but instead the SmtEngine enabled produce-models internally. The code for dump-models and dump-proofs was (perhaps out of paranoia) checking produce-models and produce-proofs. This removes this check, which is the correct thing to do since SmtEngine internally ensures produce-models is set.

Eliminate call to currentNM within NodeManager (#4227)

Eliminates 2 unintentional calls to the global access function.

Cleanup deprecated quantifiers attribute features (#4215)

Disable slow regression (#4221)

Benchmark recently became slow, disable for now.

Enum for all remaining string inferences (#4220)

Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.

Remove links field in all toml files (#4201)

This includes:

All options pertaining to SMTEngine are now handled at the top of setDefaults.
smtlibStrict was deleted in favor of a script.
statsEveryQuery enables stats by modifying a public option function. This is a slight hack but this code will likely get refactored as well soon.
A few other changes:

Fix a bug in SMTEngine: defineFunction should finalize options.
Call setDefaults before initilizing the TheoryEngine and ProofManager. This is necessary so that the PROOF(...) macro works earlier during initialization.
The next step will be to remove the links infrastructure for the options infrastructure. This will enable further detangling of our options dependencies.

Refactor disequality processing in string solver (#4209)

This commit refactors disequality processing in the core string solver.
It also adds statistics for the inferences and splits in those methods.
No semantic changes intended.

New C++ API: Rename Solver::mkTermInternal. (#4217)

This is for consistency with the other helper functions.

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.