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.

Set assertion in `CnfStream::ensureLiteral()` (#3927)

Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).

bv-gauss-elim: Fix handling of inconsistent case. (#4027)

This fixes the case when all rows are inconsistent.
Fixes #3999.

Fix real to int for parameterized kinds (#4016)

Fix options for regression: --sort-inference is incompatible with unsat cores. (#4011)

Fix sort inference for top-level Boolean variables (#4012)

Fixes #4010.

Fix issue with reset-assertions. (#3988)

Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.

Logic exception instead of assertion failure for instantiate (#4006)

Fixes #4003.

Protects against a (class of) nonsensical option combinations.

Update bug report template

Remove assertion in resolution bound inferences (#3980)

* Fix assertion in resolution bound inferences

* Format

* Minor

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

Use fixed-width types in test/unit/context/contest_mm_black. (#3985)

Fix -Wshadow warning in test/unit/context/context_mm_black. (#3985)

Consolidate options that disable produceModels (#3973)

Also adds --sort-inference to this list, fixes #3936.

Fix assertion failure in sort inference for Boolean equalities (#3993)

Fixes #3990.

Fix -Wshadow warnings in sygus_grammar_cons.cpp. (#3986)

Do not set values for non-linear mult terms in collectModelInfo (#3983)

Fixes #3803.

When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.

 Fix real as int for incremental (#3979)

Fixes #3956 and fixes #3969.

Do not traverse quantifiers in nl ext purify (#3982)

Only register sygus terms to unfold if option is set (#3978)

Fixes #3953.

Document bv-to-bool recursion (#3848)

The BV-to-bool pass is implemented recursively.
This commit documents that.
We may want to change it at some point.

Enhancement: make the bool-to-bv pass more robust and targeted (#3021)

This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector.

Rename sygus option name (#3977)

This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).

It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.

Remove instantiation propagator infrastructure (#3975)

Ensure standard miniscoping is applied before aggressive miniscoping (#3974)

Fixes #3947.

Eliminate spurious assertion (#3976)

DecisionEngine: Use unique_ptr for enabled strategies. (#3984)

Fix type issue in arith rewrite equality (#3972)

Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.

Make registration of unit clauses more robust (#3965)

Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.

Increase stack size for Windows builds to 100 MB (#3943)

Fixes #3528. The default stack size for Windows builds is very limited
(it seems to be 1 MB). This leads to problems for some of our users'
benchmarks (see the previously mentioned issue and another email that
we've received recently). Bumping the stack size to 100 MB seems to
solve the issues for the benchmarks that we have received. This of
course does not mean that we shouldn't continue working towards making
less of our code recursive.

Clean up more uses of ExprManager in parsers (#3932)

Towards parser migration.

Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers.
This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.

Convert more uses of strings to words (#3921)

Towards theory of sequences.

Also adds documentation to strncmp/rstrncmp and adds them to the Word interface.

Fix quoting of options on Travis (#3981)

For some reason, Travis has started to treat our `TRAVIS_CVC4_CONFIG`
environment variable wrong, leading to failing builds. Travis started to
wrap the argument into double quotes, so when we had single quotes
around our argument list, the arguments were treated as a single
argument and when we had double quotes, the second pair of double quotes
terminated the first one permaturely. Declaring the environment
variables individually seems to work as expected, so this commit is
moving to that format.

Fixes for bounds on transcendental functions (#3832)

This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures).

There were previously two issues on why transcendental function applications were not being assigned bounds:

"Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly,
Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound.
This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes.

The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly.

Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat.

Rewrite again full for DIV rewrite (#3945)

Fixes #3944.

Explicit end marker for models printed in the CVC language (#3934)

Fixes https://github.com/CVC4/cvc4-wishues/issues/9.

When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.

This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```

Minor refactor for theory of sets (#3924)

Flattens a block of code and refactors the main check loop, will make it easier to incorporate new extensions.

It also avoids a needless call to check() for Relations when there are no relations constraints.

Simplify DatatypeDeclarationCommand command (#3928)

The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.

It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.

This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.

Remove tester name from APIs (#3929)

This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.

This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.

This is work towards parser migration.

Ignore model check warning in regression test (#3926)

PR #3918 added a new test case that results in a warning when checking
models, which makes the regression fail. This commit adds a flag to the
test to ignore that warning.

Make sygus datatype building independent of parser in sygus v2 (#3923)

The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.

The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.

This is work towards the SyGuS API.

Support default sygus grammar construction for sets (#3842)

Fixes #3645.

Make output of regression script more readable (#3911)

The output of the regression script was difficult to read (especially
the diffs). This commit makes the output more readable by adding colors,
separators, and using a unified diff.

Remove --apply-to-const preprocessing pass (#3919)

Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.

Add a new arith constraint proof rule: IntTightenAP (#3818)

This rule is used when a bound on an integer expression is tightened
because of integer reasoning.

Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.

For IntHoleAP, we will have to omit a hole.

Revert "Add a new arith constraint proof rule: IntTightenAP (#3818)"

This reverts commit c360b3af4371cf871935a8bae96be5f8fecf741b.

Add a new arith constraint proof rule: IntTightenAP (#3818)

This rule is used when a bound on an integer expression is tightened
because of integer reasoning.

Before this rule was subsumed by IntHoleAP, a catch-all rule for integer
reasoning. We are now articulating IntTightenAP separately, because we
can produce proofs for it.

For IntHoleAP, we will have to omit a hole.

Migrate a majority of the functionality in parsers to the new API (#3838)

This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.

Remaining tasks:

Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.

Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.

This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.

Move ownership of DecisionEngine into PropEngine. (#3850)

This is in preparation of fixing the issue we currently have with
reset-assertions.  This also removes a competition hack for QF_LRA.

Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"

This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.

Move ownership of DecisionEngine into PropEngine. (#3850)

This is in preparation of fixing the issue we currently have with reset-assertions.

This also removes a competition hack for QF_LRA.

Fix issues with real to int (#3918)

This fixes a few issues in the real to int preprocessing pass. Previously it was not robust to cases where the input had constraints that were not over the reals.

Fixes #3915 and fixes #3913 and fixes #3916.

Enable -Wshadow and fix warnings. (#3909)

Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.

Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>

Refactoring and cleaning the type enumerator for sets (#3908)

* Miscellaneous changes

* Removed unnecessary vector of enumerators

* cleanup

* cleanup

* cleanup

* refactoring

* cleanup

* refactoring

* used binary numbers for sets

* isFinished for enumerator

* format

* added theory_sets_type_enumerator_white.h

* format

* Used BitVector class

* Tracing

* Documentation

* moved implementation to theory_sets_type_enumerator.cpp

* minor changes

Standardize the interface for SMT engine subsolvers (#3836)

This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.

This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).

Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).

Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)

A local declaration of `s1` was shadowing `s1`, which meant that the
non-local definition of `s1` could never be not null. This meant that
parts of the code were never run. This commit fixes the issue by
removing the local declaration.

Fix variable shadowing bug in sets. (#3898)

 Split collect model info by types in strings (#3847)

Towards a theory of sequences.

We will need to do similar splits per type for most of the functions throughout strings.

Convert more uses of string to word (#3834)

 Throw warning instead of error for non-constant values in check-model stages (#3844)

Fixes #3729 and fixes #3720.

This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible.

Add support for str.from_code (#3829)

This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.

propEngine: Reorder class declaration according to code style guidelines. (#3846)

Fix assertion related to assignability in the model. (#3843)

Fixes #3813.

It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark.

Replace conditional rewrite pass in quantifiers with the extended rewriter (#3841)

Fixes #3839.

Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.

This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.

Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.

This PR relies on #3840.

Use enum for quantifiers rewrite steps (#3840)

Makes trace messages easier to understand.

Refactor operator applications in the parser (#3831)

This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes:

Indexed ops are carried in ParseOp via api::Op not Expr,
getKindForFunction is limited to "APPLY" kinds from the new API,
The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity.
TPTP should use DIVISION not DIVISION_TOTAL.
This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.

Changing TPTP parser to accomodate new API (#3837)

Removing dependency of kinds corresponding to expressions.

Update purifySygusGTerm to the new API (#3830)

Towards parser migration.

(Partially) updates the central function used for synth-fun in sygus v2 to the new API.

It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API.

Fix large models for strings (#3835)

Fixes #3375.

Marking as "major" since in fact we produce incorrect models in production without the fix.

Fix -Wshadow warnings in common headers (#3826)

Add support for is_digit and regular expression difference (#3828)

Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing.

Disable regression that times out on debug (#3833)

Move fix for vacuous sygus types out of the parser (#3820)

This moves a fix for vacuous sygus types out of the parser and into the Expr-level datatype.

This is a temporary fix so that further progress can be made on parser migration (and to declutter the parser).

This will be refactored when an API for SyGuS is established (CVC4/cvc4-projects#38).

Initial work towards -Wshadow (#3817)

Some initial work on using words (#3819)

Towards support for sequences (CVC4/cvc4-projects#23.)

Infrastructure for tautological literals in nonlinear solver (#3795)

Work towards CVC4/cvc4-projects#113 and #3783.

This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".

This PR is required for further refactoring of check-model for transcendental functions.

Use side effect utility for non-linear lemmas (#3780)

Fixes #3647.

Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.

This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.

Fix regression (#3827)

More fixes for printing sygus commands (#3812)

Towards v1 -> v2 sygus conversion.

This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).

Basic support for regular expression complement (#3437)

Fixes #3408 .

Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h

Refactor type ascriptions in the parser (#3825)

Towards parser migration.

This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API.

This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.

Minor improvement to ParseOp (#3808)

Use default consts when not using any const during grammar normalization (#3807)

Fixes #3802.

If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.

Fix node arity issue in reduction of int2bv (#3777)

Move equivalence class info to its own file in strings (#3799)

Code move only, no updates to behavior or content of code in this PR.

Support for witnessing choice in models (#3781)

Fixes #3300.

This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.