(proof-new) Minor updates to strings base solver (#4606)

In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions.

This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness.

Cardinality-related inferences per type in theory of strings (#4585)

Towards theory of sequences.

This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.

(proof-new) Split TheoryEngine (#4558)

This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs.

This PR does not change their behavior and is code-move only modulo a few cosmetic changes.

Fix install of static builds (#4604)

We use CMAKE_INSTALL_PATH to set the installation prefix as an RPATH
in the executable. However, for static builds, changing the RPATH fails.
This commit changes our build system to only change the
CMAKE_INSTALL_PATH if we are doing a shared library build.

Add rewrite for str.replace_re. (#4601)

This was discovered due to a proof checking abnormality, where the checker surprisingly succeeded in proving that the reduced form for a str.replace_re was equivalent for 2 different sets of skolems after rewriting.

 (proof-new) Add lazy proof utility (#4589)

Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.

(proof-new) Add eager proof generator utility. (#4592)

Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/.

(proof-new) Remove arith-snorm option. (#4591)

This option only marginally helped and will be difficult to support with the new proof infrastructure.

(proof-new) Theory proof step buffer utility (#4580)

This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.

Add support for str.replace_re/str.replace_re_all (#4594)

This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.

Fix getKind for Python bindings (#4496)

I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.

(proof-new) Refactor skolemization (#4586)

This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized.

This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.

(proof-new) Add trust node utility (#4588)

This is a core data structure for associating a formula with a proof generator.

Language bindings: Enable catching of exceptions (#2813)

Fixes #2810. SWIG relies on throw specifiers to determine which
exceptions a method can throw. The wrappers generated by SWIG catch
those C++ exceptions and turn them into exceptions for the target
language. However, we have removed throw specifiers because they have
been deprecated in C++11, so SWIG did not know about any of our
exceptions. This commit fixes the issue using the %catches directive,
declaring that all methods may throw a CVC4::Exception or a general
exception. Note: This means that users of the language bindings will
just receive a general CVC4::Exception instead of more specific
exceptions like TypeExceptions. Given that we are planning to have a
single exception type for the new CVC4 API, this seemed like a natural
choice.
Additionally, the commit (significantly) simplifies the mapping of C++
to Java exceptions and fixes an issue with Python exceptions not
inheriting from BaseException. Finally, the commit adds API examples
for Java and Python, which demonstrate catching exceptions, and adds
Python examples as tests in our build system.

Ensure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp (#4570)

## Issue

When building CVC4, and when there are no source code codes (a so-called "no op" build), it seems that some of CMake targets are still fired:

```
[avj@tempvm build]$ ninja -d explain -d stats
ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist
ninja explain: proofs/signatures/all is dirty
ninja explain: output doc/all of phony edge with no inputs doesn't exist
ninja explain: doc/all is dirty
ninja explain: output src/base/CMakeFiles/gen-gitinfo doesn't exist
ninja explain: src/base/CMakeFiles/gen-gitinfo is dirty
ninja explain: output src/base/CMakeFiles/gen-tags-debug doesn't exist
ninja explain: src/base/Debug_tags.tmp is dirty
ninja explain: src/base/CMakeFiles/gen-tags-debug is dirty
ninja explain: src/base/Debug_tags.tmp is dirty
ninja explain: output src/base/CMakeFiles/gen-tags-trace doesn't exist
ninja explain: src/base/CMakeFiles/gen-tags-trace is dirty
ninja explain: src/base/Trace_tags.tmp is dirty
ninja explain: src/base/Debug_tags is dirty
ninja explain: src/base/Debug_tags.h is dirty
ninja explain: src/base/Trace_tags.tmp is dirty
ninja explain: src/base/Trace_tags is dirty
ninja explain: src/base/Trace_tags.h is dirty
ninja explain: src/base/CMakeFiles/gen-tags is dirty
ninja explain: src/base/Debug_tags.h is dirty
ninja explain: src/base/Trace_tags.h is dirty
ninja explain: src/base/Debug_tags is dirty
ninja explain: src/base/Trace_tags is dirty
ninja explain: src/base/gen-tags-debug is dirty
ninja explain: src/base/gen-tags-trace is dirty
ninja explain: output src/base/all of phony edge with no inputs doesn't exist
ninja explain: src/base/all is dirty
ninja explain: output src/expr/all of phony edge with no inputs doesn't exist
ninja explain: src/expr/all is dirty
ninja explain: output src/options/all of phony edge with no inputs doesn't exist
ninja explain: src/options/all is dirty
ninja explain: output src/theory/all of phony edge with no inputs doesn't exist
ninja explain: src/theory/all is dirty
ninja explain: output src/util/all of phony edge with no inputs doesn't exist
ninja explain: src/util/all is dirty
ninja explain: src/all is dirty
ninja explain: output test/regress/all of phony edge with no inputs doesn't exist
ninja explain: test/regress/all is dirty
ninja explain: test/all is dirty
[5/6] Generating Trace_tags
metric            count  avg (us)  total (ms)
.ninja parse      2      7192.5   14.4
canonicalize str  3315   0.2      0.7
canonicalize path 3315   0.2      0.5
lookup node       5325   0.2      1.1
.ninja_log load   1      548.0    0.5
.ninja_deps load  1      3882.0   3.9
node stat         2234   1.4      3.0
StartEdge         12     76.8     0.9
FinishCommand     5      74.6     0.4

path->node hash load 0.77 (2468 entries / 3209 buckets)
```

This is mainly because `gen-tags-debug`, `gen-tags-trace` and `gen-gitinfo` are targets with no (stated) outputs and nothing that generates them.

## Solution

This commit cleans-up the CMake inside of `src/base/CMakeLists.txt` such that, on an incremental build with no changes, no targets are fired:

```
[avj@tempvm build]$ ninja -d explain -d stats
ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist
ninja explain: proofs/signatures/all is dirty
ninja explain: output doc/all of phony edge with no inputs doesn't exist
ninja explain: doc/all is dirty
ninja explain: output src/base/all of phony edge with no inputs doesn't exist
ninja explain: src/base/all is dirty
ninja explain: output src/expr/all of phony edge with no inputs doesn't exist
ninja explain: src/expr/all is dirty
ninja explain: output src/options/all of phony edge with no inputs doesn't exist
ninja explain: src/options/all is dirty
ninja explain: output src/theory/all of phony edge with no inputs doesn't exist
ninja explain: src/theory/all is dirty
ninja explain: output src/util/all of phony edge with no inputs doesn't exist
ninja explain: src/util/all is dirty
ninja explain: src/all is dirty
ninja explain: output test/regress/all of phony edge with no inputs doesn't exist
ninja explain: test/regress/all is dirty
ninja explain: test/all is dirty
ninja: no work to do.
metric            count  avg (us)  total (ms)
.ninja parse      2      9198.0   18.4
canonicalize str  5314   0.2      1.1
canonicalize path 5314   0.2      0.9
lookup node       7324   0.2      1.6
.ninja_log load   1      635.0    0.6
.ninja_deps load  1      4309.0   4.3
node stat         2240   1.3      3.0

path->node hash load 0.78 (2490 entries / 3209 buckets)
```

The important bit is `ninja: no work to do.` in the output.

### Notes

I think the only thing to note is that I have changed the CMake around this comment:

```
# Note: gen-tags-{debug,trace} are targets since we always want to generate
# the temporary tag files {Debug,Trace}_tags.tmp in order to check if tags
# were added/modified/deleted.
```

I believe that the intention here was to ensure that the tags are **always** generated on a source file change.

Given that the CVC4 CMake is passing in the files to be processed (`${source_files_list}`, which is a *string*), we can add a target dependency on this *list*  (`${source_files}`) to ensure that `{Debug,Trace}_tags.tmp` always get regenerated on a change.

So I believe I have captured the intent of the comment, without requiring the targets to be "unconditional".

I have also added a dependency on `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` in some places because, without this, if you change one of `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` then the associated targets don't get fired.

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

Fix Java target and Relations example (#4583)

Currently, our CVC4Config file is never including the CVC4 Java targets
because of a typo in `cmake/CVC4Config.cmake.in`. For this reason, our
build system for the examples would never actually build the examples.
Fixing this issue brought up another issue in our Relations Java example
that was using an outdated `System.loadLibrary()` call. This commit
fixes the typo and the example.

Note: Most changes in `Relations.java` were caused by ClangFormat.

Fix ambiguous overload in unit test (#4582)

Fixes nightlies. The compiler version used for our nightlies (GCC 5.4.0)
complains about mkFunctionSort({bSort}, bSort) being ambiguous because
we have two variants of mkFunctionSort(): one that takes a single
Sort and one that takes a vector of Sorts. This commit makes the
function call unambiguous by removing the use of list initializations.

(proof-new) Add abstract proof generator class (#4574)

Also adds a commonly used proof generator: the proof reference proof generator.

Fix Coverity issues (#4587)

This commit fixes the following Coverity issues:

- 1495606: uninitialized field
- 1495605: uninitialized field
- 1488953: uninitialized field
- 1495604: mismatched iterator

Use NlLemma utility for all lemmas in non-linear. (#4573)

This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future.

This also enables a fix on the IAND branch related to preprocessing lemmas.

Fix destruction order in NodeManager (#4578)

Fixes #4576. ASan was reporting memory leaks because the skolem manager
was being destroyed after the attributes and zombies were already
cleaned up in the destructor of NodeManager. This commit changes the
destruction order to ensure that the skolem manager is destroyed before
the rest of the cleanup.

Note: this issue did not only make the benchmark in #4576 fail but
several tests in our regressions.

Keep definitions when global-declarations enabled (#4572)

Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.

Smt2 parsing support for nested recursive datatypes (#4575)

Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.

Adds 3 regressions using the option --dt-nested-rec.

Datatypes with nested recursion are not handled in TheoryDatatypes unless option is set (#3707)

Towards experimental support for non-simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec). Builds a check for non-simple recursion in the DType class. If a term of a datatype type is registered to TheoryDatatypes for a datatype that has nested recursion, we throw a LogicException unless the option dtNestedRec is set to true. Also includes a bug discovered in the TypeMatcher utility and another in expr::getComponentTypes.

It also adds a unit test using the new API for a simple parametric datatype example as well, not related to nested recursion, as this was previously missing.

(proof-new) Updates to CDProof (#4565)

This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.

Skip parse-error regression for comp builds (#4567)

Fixes nightlies. Competition builds do not report parsing errors like
other builds. As a result, one of the regression tests that is testing
for parse errors was failing for competition builds. In this particular
example, we just report `unknown`. This commit marks the regression to
be skipped for competition builds.

(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)

This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.

This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.

Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.

Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.

Changing default language (#4561)

Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now.

Printing FP values as binary or indexed BVs according to option (#4554)

Fix handling of Boolean term variables (#4550)

Fixes #4446. This commit fixes two issues related to the handling of
Boolean term variables:

Removing Boolean subterms and replacing them with a Boolean term
variable introduces an equality of the form (= v t) where v is the
Boolean term variable and t is the term. It is important that these
equalities do not get removed. This commit changes
Theory::isLegalElimination() to take this into account.

The incorrect model reported in the issue was caused by some of the
Boolean term variables not being assigned values by the SAT solver
when we decided that the benchmark is satisfiable. Our justification
heuristic (correctly) decided that it is enough to satisfy one of the
disjuncts in the assertion to satisfy the whole assertion. However,
the assignments that we received from the SAT solver restricted us to
pick a specific value for one of the Boolean constants:

Literal | Value | Expr
---------------------------------------------------------
'7 ' 0 c
'0 ' 1 true
'1 ' 0 false
'2 ' 0 (a BOOLEAN_TERM_VARIABLE_274)
'5 ' _ b
'3 ' 1 (a BOOLEAN_TERM_VARIABLE_277)
'4 ' _ BOOLEAN_TERM_VARIABLE_274
'6 ' 0 BOOLEAN_TERM_VARIABLE_277
This meant that we had to pick true for BOOLEAN_TERM_VARIABLE_274
but we picked false since we simply treated it as an unassigned
variable. In general, the justification heuristic handles embedded
skolems introduced by term removal first and asks the SAT solver to
decide on Boolean term variables. However, for some logics, such as
QF_AUFLIA, we use the justification heuristic not for decisions but
only to decide when to stop, so those decisions were not done. This
commit introduces a conservative fix that adds a check after
satsifying all the assertions that makes sure that the equalities
introduced for Boolean terms are satisfied as well. Due to the eager
treatment of Boolean term variables when we use the justification
heuristic also for decisions, it is likely that we don't really have
the problem in that case but it doesn't hurt to enable the fix. It is
also possible that this fix is only required with models but it is
definitely safer to just always enable it (there could be tricky
corner cases involving the theory combination between UF and Boolean
terms). Additionally, this commit changes the ITE-specific naming in
the justification heuristic to reflect more accurately that we are in
general dealing with skolems introduced by term removals and not only
due to ITE removal.

Fix lifetime and copy issues with NodeDfsIterable (#4569)

When running node_traversal_black with ASan and UBSan, there were two
distinct issues being reported. UBSan was complaining that we were
assigning an invalid value to a Boolean. This happened because
d_initialized in NodeDfsIterator was uninitialized and the default
copy constructor tried to copy it. This commit removes that data member.
ASan was complainig that NodeDfsIterator::begin() was trying to access
a skip function that had been freed. In particular, this happened when
NodeDfsIterable was used in a range-based for loop like so:

for (auto n : NodeDfsIterable(n).inPostorder())
{
  ...
}
The problem here is that the lifetime of a temporary within the range
expression is not extended (the lifetime of the result of the range
expression is extended, however) [0]. This is a problem because
NodeDfsIterable(n) is a temporary and inPostorder() returns a
reference to that temporary. It makes sense that the compiler cannot
possibly know that the reference from inPostorder() corresponds to
NodeDfsIterable(n), so it cannot extend its lifetime. See [1] for more
details on the problem with chained functions.

This commit fixes the issue by replacing the fluent interface of
NodeDfsIterable by a constructor with default arguments. Additionally,
it introduces an enum to represent the visit order to avoid having a
nondescript Boolean argument.

[0] https://en.cppreference.com/w/cpp/language/range-for#Temporary_range_expression
[1] http://cpptruths.blogspot.com/2018/10/chained-functions-break-reference.html?m=1

If using 'ninja', tell the user to run 'ninja' not 'make' (#4568)

## Issue

If you call CVC4's `configure` script with `--ninja`, then you get a misleading status message:

```
[avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5
Now change to 'build' and type make, followed by make check or make install.

-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/working/CVC4/build
```

## Solution

This commit simply fixes the status message to tell the user to run the correct command based on the specified generator:

```
[avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5
Now change to 'build' and type 'ninja', followed by 'ninja check' or 'ninja install'.

-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/working/CVC4/build
```

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

Add a method for retrieving base of a constant array through API (#4494)

Update Java tests to match changes in API (#4535)

Commit cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 renamed
`Result::Validity` and `SmtEngine::query()` to `Result::Entailment` and
`SmtEngine::checkEntailed()`, respectively. The commit did not update
the Java tests which lead to issues in debug builds with Java bindings.
The commit also adds a corresponding `NEWS` entry.

Wrap Result in Python API (#4473)

This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova.

New C++ Api: Second and last batch of API guards. (#4563)

This adds the remaining API guards in the Solver object (incl. unit tests).

Add sygus datatype substitution utility method (#4390)

This makes the method for substiutiton and generalization of sygus datatypes a generic utility method. It updates the abduction method to use it. Interpolation is another target user of this utility.

Fix abduction with datatypes (#4566)

Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.

Theory strings preprocess (#4534)

This makes it so that the main reduce function in TheoryStringsPreprocess is static, so that it can be used both by the solver and the proof checker.

It also updates the functions to make use of IndexVar for constructing canonical universal variables.

New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

(proof-new) Adding rules and proof checker for EUF (#4559)

(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)

(proof-new) Add builtin proof checker (#4537)

This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.

Fix normalization of author names in contrib/get-authors. (#4553)

Do not apply unconstrained simplification when quantifiers are present (#4532)

Fixes #4437.

This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.

It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.

Update CEGQI to use lemma status instead of forcing preprocess (#4551)

This PR removes a hack in counterexample-guided quantifier instantiation.

The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.

Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.

This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.

Use prenex normal form when using cegqi-nested-qe (#4522)

Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.

This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).

Add Term::substitute to Python bindings (#4499)

Add hash Op, Sort and Term in Python bindings (#4498)

Fix scope issue with pulling ITEs in extended rewriter. (#4547)

Fixes #4476.

Do not handle universal quantification on functions in model-based FMF (#4226)

Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.

This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.

Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.

New C++ API: Keep reference to solver object in non-solver objects. (#4549)

This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.

(proof-new) Proof step buffer utilities (#4533)

This class is used for delaying proof node creation until it is necessary.

Move non-linear files to src/theory/arith/nl (#4548)

Also makes CVC4::theory::arith::nl namespace.

This includes some formatting changes.

Set theoryof-mode after theory widening (#4545)

Fixes #4367. We set the theoryof-mode depending on whether sharing is
enabled or not. However, we were checking whether sharing was enabled
before theory widening, leading to unexpected results. This commit moves
the check after widening the theories.

For the benchmark in the issue, setting the theoryof-mode before theory
widening lead to problems because of the following:

The main solver checks the condition for enabling term-based
theoryof-mode, decides not to do it because sharing is not enabled
Main solver adds UF to the logic
Main solver does a check-sat all
Unsat core check runs, sees both UF and NRA enabled, and switches
to term-based mode
Main solver gets to second check-sat call, now the theoryof-mode is
suddenly changed, which leads to problems in the equality engine
This commit fixes the issue in this particular instance but it is important
to note that it does not address the issue of the subsolver changing
settings in general. This can only really be solved by separating the
options from the ExprManager/NodeManager and having separate
options for each SmtEngine/Solver instance.

Do not parse ->/lambda unless --uf-ho enabled (#4544)

Fixes #4477. Logic ALL includes higher-order but we currently do not
support solving higher-order problems unless --uf-ho is enabled. This
commit changes the condition under which we parse -> and lambda to
only enabled parsing of those symbols if the logic allows higher-order
constraints and --uf-ho is enabled.

Incorporate sequences into the word interface (#4543)

Also renames a function mkWord -> mkWordFlatten.

Do not cache operator eliminations in arith (#4542)

Fixes #4525. The actual problem in the issue is not that the unsat core
is satisfiable but that our unsat core check is not working as intended.
Our unsat core check uses the same `ExprManager` as the main `SmtEngine`
and thus also shares the same attributes for nodes. However, since we
have a different `SmtEngine` instance for the check, we also have
different instances of `TheoryArith`. This leads to the check failing
due to the following:

- Our only input assertion is `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
  0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
  expanded as expected but no attribute is set because it happens in a
  simple `TheoryArith::eliminateOperators()` call.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
  `(/ 1 0)` (not cached) and then we expand it recursively to the
  expected term and cache `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/
  1 0))`.

Up to this point, things are suboptimal but there are no correctness
issues. The problem starts when we do the same process in the unsat core
check:

- Our only input assertion is again `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
  0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
  expanded as expected but no attribute is set or checked because it
  happens in a simple `TheoryArith::eliminateOperators()` call. Note
  that the skolem introduced here for the division-by-zero case is
  different from the skolem introduced above because this is in a
  different `TheoryArith` instance that does not know the existing
  skolems.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
  `(/ 1 0)` (not cached) and then we use the cache from our solving call
  to expand it `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`.
  Note that `divByZero` here is the skolem from the main solver.

As a result, the preprocessed assertions mix skolems from the main
`SmtEngine` with the `SmtEngine` of the unsat core check, making the
constraints satisfiable.

To solve this problem, this commit removes the caching-by-attribute
mechanism. The reason for removing it is that it is currently
ineffective (since most eliminations do not seem to be cached) and there
are caches at other levels, e.g. when expanding definitions. If we deem
the operator elimination to be a bottleneck, we can introduce a similar
mechanism at the level of `TheoryArith`.

update example in README to use ctest. (#4540)

An example for restricting timeout in tests uses the old `make regress0` instead of the new `ctest -L regress0`

Add the sequence type (#4539)

This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.

The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.

Fix term registry for constant case, simplify. (#4538)

We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.

It also removes a deprecated option that is deleted in the proof-new branch.

Add the Expr-level sequence datatype (#4526)

This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.

Tweak the use of static_assert to support older compilers. (#4536)

C++11 introduces static_assert(bool, string).
C++17 introduces static_assert(bool)

By adding a message we can support older compilers such as those
used by our nightly build system...

Fix an incorrect limit in conversion from real to float (#4418)

This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.

Convert more uses of strings to words (#4527)

Fix mismatched iterators (CID 1493892). (#4531)

Issue found by coverity.

(proof-new) Update proof checker. (#4511)

This adds new required features to proof checker and the base class of proof rule checker.

This is required as the first dependency towards merging further infrastructure related to proofs.

(proof-new) Updates to strings skolem cache. (#4524)

This PR makes strings skolem cache call the ProofSkolemCache. This is required for proper proof checking, as it makes all skolems be associated with their formal definition, encapsulated by a witness term.

It furthermore makes skolem sharing more uniform and aggressive by noting that most string skolems correspond to purification variables (typically for some substr term). A purification variable for a term that rewrites to a constant can be replaced by the constant itself.

It also introduces an attribute IndexVarAttribute which is used to ensure reductions involving universal variables are deterministic.

Update to CaDiCaL version 1.2.1. (#4530)

[SMT-COMP] Redirect non-answers to /dev/null (#4528)

Commit 00badd3a63a2fa568373d5c58553944b579d42bb changed our run script
to write output other than `sat`/`unsat` to a file if `$2` is passed to
it. However, it looks like StarExec does not pass that parameter to our
script despite the documentation claiming that it does [0]. This commit
makes our check more defensive by redirecting our unnecessary output to
`/dev/null` if `STAREXEC_WALLCLOCK_LIMIT` is set. I've done a quick test
run on StarExec and it looks like this does the trick.

[0]
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables

remove unused field d_emp_exp in TheorySetsPrivate (#4521)

Remove unused field d_emp_exp in TheorySetsPrivate

Add the sequence datatype (#4153)

This class is the Node-level representation of a sequence. It is analogous to CVC4::String.

Fix mistakes in sygus API comments. (#4520)

Refactor operator elimination in arithmetic (#4519)

This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.

The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.

As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.

This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.

Also notice that --rewrite-divk is effectively now enabled by default always.

Fixes #4484, fixes #4486, fixes #4481.

[SMT-COMP] Use tear-down-incremental for arithmetic (#4518)

This commit changes the run-script for the incremental track to use
`--tear-down-incremental=1` for all logics that involve arithmetic. The
main motivation for this change is avoid issues that we have with the
lemmas generated for `mod`/`div` during `ppRewrite` that cause
model-soundness issues.

CaDiCaL: Clean up initialization on creation. (#4516)

(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)

This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).

This allows us to justify the regular expression inclusion inference as a rewrite.

Cryptominisat: Clean up initialization on creation. (#4515)

Add support for SAT solver Kissat. (#4514)

(proof-new) Proof node to SExpr utility. (#4512)

This is required for dag-ifying ProofNode output.

Update string kind names in new API (#4509)

To match the smt2 Unicode standard. The internal ones are left unchanged for now.

(proof-new) Minor update to strings solver state (#4510)

Disable re-elim by default (#4508)

Disabling re-elim performs better overall in many recent experiments.

Make Grammar reusable. (#4506)

This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.

Throw logic exception for equality between regular expressions (#4505)

Fixes #4503.

Fix missing check for cardinality one in unconstrained simplifier (#4504)

Fixes #4482.

Normal form equality conflicts and uniqueness check (#4497)

This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.

It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.

Add proof skolem cache (#4485)

This adds the general utility for maintaining mappings from Skolems to their witness form via attributes.

I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs.

Fix parametric datatype instantiation (#4493)

A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.

CegqiBv: Clean up after renaming options. (#4487)

Use debug-check-model to enable internal debugging in check-model (#4480)

Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.

Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.

Add a simple script to convert sygus v1 files to v2. (#4409)

Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.

Fix cached free variable identifiers in sygus term database (#4394)

Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.

Fixes #4383.

Renamed operator CHOICE to WITNESS (#4207)

Renamed operator CHOICE to WITNESS, and removed it from the front end

Use fresh variables when miniscoping (#4296)

Fixes #4288.

When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.

Update enum and option names for sygus languages (#4388)

This ensures sygus is interpreted as sygus version 2; sygus1 must be used to specify sygus version 1.

Required for the 1.8 release.

Make SolveEq and PlusCombineLikeTerms idempotent (#4438)

Fixes #3692 and an assertion failure that came up during the test runs
for SMT-COMP. The bit-vector rewrites `SolveEq` and
`PlusCombineLikeTerms` were not always idempotent. At a high level,
`SolveEq` combines common terms from two sides of an equality and
`PlusCombineLikeTerms` combines common terms within an addition.
However, in doing so, these rewrites were reordering the operands of the
bit-vector addition based on the node ids of the terms that were
multiplied with their coefficients. Consider the addition `3 * x * y + 5
* y * z` (the bit-width does not matter). `PlusCombineLikeTerms` would
reorder this addition to `5 * y * z + 3 * x * y` if the node id of `y *
z` was smaller than the node id of `x * y`. The issue is that node ids
are not fixed for a given term: If we have a term `x * y` and that term
reaches ref count 0, we may get a different id for that same term if we
recreate it later on. When terms reach ref count 0, we don't immediately
delete them but add them to our set of zombies to be deleted whenever
the list of zombies grows larger than some fixed size. When applying
`SolveEq` and `PlusCombineLikeTerms` multiple times (even in direct
succession without doing anything else), the node order may change
because some of the terms like `x * y` may be zombies while others have
been deleted and get new ids, leading to the relative order of node ids
changing. I suspect that we could construct a case where we get into an
infinite rewrite loop.

This commit addresses the issue as follows: It does not perform the
rewrites `SolveEq` and `PlusCombineLikeTerms` if none of the operands
change. This makes the rewrites idempotent. Note however that we are
still not guaranteeing that a term has the same rewritten form
throughout an execution because the node ids may change if the term has
been freed in the meantime. However, this limitation is consistent with
other rewrites such as the reordering of equalities.

I am including the minimized test case from our run on SMT-LIB. I am
ommittin the test case from #3692 because I couldn't trigger it on
master (not surprising since the issue requires very specific
circumstances to actually occur). However, I was able to reproduce the
issue on the CVC4 version mentioned in the issue and confirmed that this
fix worked for that older version.

Do not enable unconstrained simplification if arithmetic is present (#4489)

For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71).

Update run scripts for SMT-COMP 2020 (#4454)

This commit adds additional options for the model validation track and
makes sure that non-"sat"/"unsat" outputs from the sequential porfolio
approaches are written to a file instead of stderr when running on
StarExec.