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.

Hide options for and related to the BV abstraction module. (#4041)

All things related to the current BV solver are obsolete in the sense
that we are working on a new BV solver implementation. The BV abstraction
module has several issues and is quite hacky, it should only be enabled
in experimental settings. We don't want to remove it yet though, we want
to keep it around for future evaluation purposes. This commit
categorizes the option to enable the module and a second option related
to the module as 'undocumented'.

Simplifications to the Datatypes API (#4040)

Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.

I updated the Python files, although would be helpful to double check this is correct.

Co-authored-by: makaimann <makaim@stanford.edu>

Add automatic Cython binding installation (#3933)

* Remove getIndices for Kinds

* Test importing pycvc4

* Distutils install for pycvc4

* Use full path for cvc4kinds prefix

* Remove zip_safe option (not needed for distutils)

* Automatically clean up setup.py intermediate files

* Rely on make install to install pycvc4

* Run make install when testing python bindings

* Fix: Check importing pycvc4 when python bindings are built

* Remove one -Wshadow warning for cython-generated files

* Put the fake kinds submodule in generated __init__.py

* Remove unnecessary file permission options in python CMakeLists

* Respect install prefix unless in a virtualenv

* Handle python2 print function

* Use VIRTUAL_ENV environment variable to check if in python virtualenv

* Add header and documentation to setup.py.in

* Capitalize CVC4 in PyCVC4Install

* Update src/api/python/CMakeLists.txt

Co-Authored-By: Mathias Preiner <mathias.preiner@gmail.com>
* Simplify CMakeLists for setup.py configuration

* Shorten virtualenv check with Mathias's suggestion

* Set TRAVIS_CVC4_PYTHON_BINDINGS to no in other builds

* minor: bash syntax fix

* Move pycvc4 import check to makeInstallCheck

* Include installed pycvc4 location on PYTHONPATH

* Better way to set PYTHONPATH

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

Do not enable some SMT-COMP specific options by default (#4038)

Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).

Issue #789 can be downgraded to "minor" after this PR.

Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.

Guard against null relevancy condition in SyGuS (#4033)

Fixes #4025.

Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).

Add missing datatype functions to new API (#3930)

This is in preparation for migrating the parser to use the Term-level API for datatypes.

Notably, this adds the function mkDatatypeSorts for making mutually recursive datatypes. I've added a unit test that demonstrates this method (which mirrors the Expr-level datatype API).

Switch to Nodes for conjecture generator (#4026)

Fixes #4022.

reset-assertions: Update TheoryEngine's PropEngine* (#4032)

Fixes #4028. TheoryEngine's pointer was not updated to the new
PropEngine when resetting assertions. This commit fixes that. As far
as I can tell, this was the only class storing a PropEngine* that
isn't owned by PropEngine, so we should hopefully not have other
similar issues.

Remove experimental symmetry breaker (#4005)

This never impacted performance positively. Fixes #3997 and fixes #4015.

There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.

Fix non-parametrized operators in subgoal generation (#4023)

Fixes #4021.

We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.

Remove partial instantiation for local theory extensions (#4020)

Fixes #4019.

This feature was never fully implemented.

Fix (#4017)

Fixes #4001.

This assertion was more of a conjecture (stating that easy cases of miniscoping are already handled). However some option combinations can break this invariant, regardless the code should do the correct thing.

Fix duplicate variable issue in sygus-qe-preproc (#4013)

Introduce tables in the rewriter (#3742)

This commit adds tables in the rewriter that store which function should
be used to rewrite which kind. We have separate tables for `EQUAL`
because every theory has its own equality rewriter.