(proof-new) Skeleton proof support in the Rewriter (#4730)

This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).

It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.

The unit test of this feature should be added on a followup PR.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.

Debug instantiations output (#4739)

This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```

It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).

It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug.  Marking major since this fixes debug regress1.

Minor refactoring of subsolver initialization (#4731)

This decouples asserting a formula with initialization (previously it was a complex process to assert a formula due to having to clone/export to a new ExprManager). Now it is trivial.

This commit fixes an unintended consequence of the previous complications. Previously, SmtEngine::setOption would be set after asserting formulas to an SmtEngine subsolver, which is technically incorrect, as options should be finalized before the first assert.

This is required for further cleaning up of options listeners.

Fix caching in TheoryEngine::getExplanation() (#4736)

Commit 64a7db86206aa0993f75446a3e7f77f3c0c023c6 introduced a caching
mechanism in `TheoryEngine::getExplanation()`. However, there seem to be
issues related to the timestamps of the explanations. This commit fixes
the issue by making the timestamp part of the cache. The change ensures
that explanations for a certain node never rely on other explanations
for that node with a later timestamp.

Fix options messages that were inverted (#4734)

Use TypeNode/Node in ArrayStoreAll (#4728)

This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.

Fix type comparisons involving pointer. (#4738)

Fixes debug regressions, introduced by a combination of the addition of sequence update and the change to pointers.

Fix whitespace issue in instantiations output. (#4737)

Fixes regress1.

 (proof-new) SMT Preprocess proof generator (#4708)

This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.

It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.

 User-facing print debug option for sygus candidates (#4720)

This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:

(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.

Statistics on instantiations per quantified formula. (#4719)

This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).

It also simplifies and improves printing of Instantiation Tries.

Implement --tlimit for windows (#4716)

The new mechanism for --tlimit only works for POSIX compatible systems (that implement setitimer). This PR implements an alternative (though roughly equivalent) approach for windows, based on SetWaitableTimer().

To make this work (without code duplication) we need to call the timeout_handler function from time_limit.cpp as the windows solution employs an asynchronous callback instead of signals. I used the opportunity to rename util.cpp to signal_handlers.cpp (as it really does not do anything else) and reformat the file.

As I do not have a windows system at hand, I have not been able to actually test this apart from making sure that it compiles with the mingw setup.

Add support for string/sequence update (#4725)

This adds basic support for string/sequence updating, which has a semantics that is length preserving.

Remove ExprSequence (#4724)

Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().

Cache explanations in TheoryEngine::getExplanation (#4722)

For some hard verification benchmarks from Facebook, TheoryEngine::getExplanation was found to be the bottleneck, where the main loop of TheoryEngine::getExplanation would be run regularly 30k times, sometimes over 1 million times for a single conflict.

This caches explanations in this loop, where now the loop is executed roughly 1k times at max for the same benchmark.

One challenging benchmark that previously solved in 8 min 45 sec now solves in 2 min 45 sec.

FYI @barrettcw .

Changing bv_to_int options (#4721)

This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.

Adding test for whether a kind is n-ary (#4718)

Add support for printing 'get-abduct' in verbose mode (#4710)

Issue
For any of the following files:

test/regress/regress1/abduct-dt.smt2
test/regress/regress1/sygus-abduct-test-ccore.smt2
test/regress/regress1/sygus-abduct-test.smt2
test/regress/regress1/sygus-abduct-ex1-grammar.smt2
test/regress/regress1/sygus-abduct-test-user.smt2
test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2
test/regress/regress1/sygus/abduction_streq.readable.smt2
test/regress/regress1/sygus/abd-simple-conj-4.smt2
test/regress/regress1/sygus/uf-abduct.smt2
test/regress/regress1/sygus/yoni-true-sol.smt2
running the following:

./bin/cvc4 -vvv <file>
would print:

Invoking: ERROR: don't know how to print a Command of class: N4CVC416GetAbductCommandE
Resolution
This PR adds support in src/printer/smt2/smt2_printer.cpp to be able to print a Command of type GetAbductCommand.

Given the similarities between get-abduct and synth-fun, I have refactored the printing logic in toStream(std::ostream& out, const SynthFunCommand* c) for a printing a SyGuS grammar to be shared between both SynthFunCommand and GetAbductCommand.

As a result, you now see something like this:

[avj@tempvm build]$ ./bin/cvc4 -vvv ../test/regress/regress1/abduct-dt.smt2
Invoking: (set-option :incremental false)
Invoking: (set-logic ALL)
Invoking: (declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))

Invoking: (declare-fun x () List)
Invoking: (assert (distinct x nil))
minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.
Invoking: (get-abduct A (= x (cons (head x) (tail x))))
(error "Cannot get abduct when produce-abducts options is off.")
Signed-off-by: Andrew V. Jones andrew.jones@vector.com

(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (#4709)

We need multiple policies for generic proofs for term conversion, in particular, substitution has a "apply once" semantics which does not apply rewrite steps to a fixpoint like the rewriter.

This is required for eliminating SUBS steps in the final proof.

Also note that an internal method for getting proofs was generalized, which will be required for doing multiple variants of proofs in this utility in the future.

(proof-new) Update Theory interface for proof-new (#4648)

This includes 4 changes:

Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.

This PR is also contingent on the performance tests for proof-new on SMT-LIB.

Always Update Git information when rebuilding (#4696)

Commit 61734b41b7b96e7e7cbf46021a357d840d64b42e changed the way some of
our source files are generated. However, the change meant that once
`git_versioninfo.cpp` was generated, it was never updated again: The
custom command for `git_versioninfo.cpp` has no dependencies, so CMake
does not rebuild it unless the output file is missing [0]. This commit
reverts the change to our `gen-gitinfo` target and adds `git_versioninfo.cpp`
to `BYPRODUCTS` for the target to indicate that the file may have changed.
I am not sure if there is a better solution because we actually have to run
`GitInfo.cmake` to see if there have been any changes in the Git information.
Introducing a dependency on all source files is not sufficient because other
files or just the branch name may change. Note: The original solution only
updates the timestamp of `git_versioninfo.cpp` if its contents actually
change (`GitInfo.cmake` uses `configure_file()` to generate
`git_versioninfo.cpp`, which only updates the timestamp when the
contents changed [1]), so we don't do any unnecessary work.

[0] https://cmake.org/cmake/help/latest/command/add_custom_command.html
[1] https://cmake.org/cmake/help/latest/command/configure_file.html

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

Front end support for integer AND (#4717)

[Interpolation] Add interface for SyGuS interpolation module (#4677)

This is the second step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The second step creates the component for computing interpolation, while omits the implementation.

Add deps/install/lib to RPATH and warn user when using dynamic libs. (#4684)

Installing the cvc4 binary does not work right now if it links against a shared library obtained via one of the contrib scripts.
This PR thus adds deps/install/lib to the RPATH so that the installed binary works at all in this case.

This change however paves the way to more problems: If one install such a dynamically linked binary and then removes (or updates) one the shared libraries in deps/install/lib, the installed binary most probably stops working.
Hence, this PR checks whether this may happen (whether we link dynamically and link against a shared library from deps/install/lib) and, if this is the case, informs and warns the user about this issue.
If the user tries to install to the default install prefix (/usr/local) we disallow installation entirely.

Update competition scripts (#4715)

This PR creates a "current" sygus comp scripts, similar to what we have been doing for SMT COMP. It updates these scripts to fix the option names, as many have changed recently.

This also copies the SMT COMP current scripts to 2020, since they were used in the current state. @4tXJ7f let me know if this is not the case.

Ensure legal elimination for witness rewrite (#4688)

Fixes #4685.

A recent commit #4661 added assertions for checking whether a witness rewrite corresponded to a legal elimination. #4685 demonstrates that these assertions can be violated and hence should be checked to ensure the rewrite is sound.

Disable unsat cores in timeout regression (#4713)

Fixes a timeout in the nightlies.

One regression times out during unsat core checking. This appears to be random, the subcall to check for unsat-cores is applying sygus-inst in the expected way, however, it struggles to find the right instances.

Furthermore note that we are planning to redo implementation of unsat cores soon (when proof-new is fully merged), so we should revisit this (and all other) regressions with --no-check-unsat-cores when that happens.

Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)

This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.

The number of inferences can then be seen with --stats:

nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.

This also adds a few high level stats to the new statistics class for non-linear.

(proof-new) Theory engine proof generator (#4657)

This adds the proof generator used by TheoryEngine for generating proofs for explanations.

Re-implement handling of --tlimit (#4655)

As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed.
In more detail, this PR:

removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager)
adds a new TimeLimitListener that lives in src/main
uses TimeLimitListener directly in runCvc4()
adds a signal handler for SIGALRM (that also uses the existing timeout_handler)

Add getName() method to options. (#4704)

getName() returns the long option name if it exists and an empty string otherwise.

Always interleave theory combination with quantifiers (#4703)

This removes an option setting that made quantifiers always run at full effort (before theory combination) when an undecidable theory was present. The intuition is that such theories may also be unfair wrt theory combination, so quantifiers might as well "join them" at full effort.

However, this option modification significantly hurts our performance in terms of timeouts on verification benchmarks from Facebook, where theory combination needs to run but quantifiers (alone) is preempting it from running. The correct solution is in fact to have other theories interleave with theory combination with the same policy as quantifiers (I've opened CVC4/cvc4-wishues#74).

Improve and fix secant and tangent lemmas in the transcendental solver (#4689)

Fixes #4686.

This benchmark failed an assertion that corresponded to the fact that a refinement lemma did not evaluate to false in the current model (and hence does not rule out the current model).

This was caused by applying the rewriter in a way that led to an incorrect approximation. This meant that some tangent and secant lemmas would be ineffective.

The benchmark in that issue now times out, but makes progress in the refinement lemmas it generates.

This also simplifies and improves the use of approximated values (instead of model values) when constructing tangent and secant lemmas.

Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)

This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.

The changes that were required for this PR include:

The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.

Increase the minimum version of CMake due to the use of 'APPEND' with strings (#4702)

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

Front end support for sequences (#4690)

With this PR, we now support a preliminary draft of a theory of sequences.

This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.

As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.

We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).

[GitHub] Add link to fuzzing guidelines in issues (#4695)

Remove SWIG bindings (#4683)

This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.

Fix regression option (#4680)

 (proof-new) Updates to skolem manager interface (#4664)

Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.

(proof-new) Proof rule checkers run on skolem forms (#4660)

Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.

Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.

(proof-new) Proof node updater (#4647)

Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.

Requires #4617.

Add solver for integer AND (#4681)

This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.

Add testing infrastructure for LFSC signatures (#4678)

This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.

Co-authored-by: Alex Ozdemir aozdemir@hmc.edu

 Inferences and model construction taking into account seq.unit (#4607)

Towards theory of sequences.

This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction.

It also fixes a bug in the best content heuristic, which previously failed to update the best score.

(proof-new) Updates to evaluator (#4659)

This will be required to separate "evaluation steps" from "rewrite steps" when reconstructing proofs of rewrites.

(proof-new) Improve rewriter for WITNESS (#4661)

Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.

Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.

Fix normal form for re.comp (#4676)

Fixes #4674.

Update NEWS post 1.8 release (#4666)

Fix GMP compilation for win64. (#4675)

Simplify quantifiers strategy for when to apply last call effort check with fmfBound (#4673)

There was a strategy in place for alternating which rounds quantifier instantiation would run on when --fmf-bound is enabled.

However, this made it so that in some cases, no instantiation strategy would be applied, if e.g. fmfBound was enabled but no quantified formulas were handled by that strategy.

It is not clear if this strategy is a good idea, considering all use cases of quantifiers, and hence this PR deletes this block of code.

This makes it so that several eqrange benchmarks are answered "unsat" quickly.

Interpolation step 1 (#4638)

This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The first step creates the API framework, while omits the implementation for getting interpolation.

contrib: Update to GMP 6.2.0, compile static and shared libraries. (#4671)

Add internal support for integer and operator (#4668)

Towards merging iand branch to master. This adds internal support for an "integer AND" operator.

Make ExprManager constructor private (#4669)

This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.

Python Sort tests (#4639)

This commit ports over the sort_black tests to the pytest infrastructure to test the Python bindings. It also adds missing functionality that was revealed during the testing.

Fix memory leak in unit test node_algorithm_black (#4670)

Commit ccd4500 modified the unit test
node_algorithm_black. It added d_bvTypeNode as a data member to the
class and initialized it in setUp() but did not free it in
tearDown(), which set off ASan. This commit fixes tearDown() to free
d_bvTypeNode.

Marking this as major because it should fix the nightlies.

Fix non-termination issues in simpleRegExpConsume (#4667)

There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions.

This also improves trace messages for simpleRegExpConsume.

Fixes #4662.

Proof Rules and Checker for Arithmetic (#4665)

This PR introduces proof rules for arithmetic and their checker.

The code is dead, since these rules are never used.

Add API for retrieving separation heap/nil term (#4663)

This commit extends the API to support the retrieval of heap/nil term
when separation logic is used and changes the corresponding system test
accordingly. This commit is in preparation of making the constructor of
`ExprManager` private.

fix and test (#4658)

This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly.

(proof-new) Add TrustNode interfaces to OutputChannel (#4643)

Remove sygus1 parser (#4651)

We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).

As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.

This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.

FYI @abdoo8080 .

Update option --nl-ext to enable/disable incremental linearization solver only (#4649)

Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques.

I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations.

It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.

Fix CVC4_EXTRAVERSION variable (#4653)

When I created the PR for 733083c, it
did not contain the change from "" -> "-prerelease" because at the
time master still had CVC4_EXTRAVERSION set to "-prerelease". This
commit fixes CVC4_EXTRAVERSION.

[unconstrained] Fix gathering of visited-once vars (#4652)

Fixes #4644. This commit fixes an issue where the set `d_unconstrained`
in the unconstrained simplification pass was not computed correctly. The
problem was that visiting the same term multiple times did not remove
the variables appearing in that term from the visited-once set. A simple
example that triggers the issue is the following:

```
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= a b)))
(assert (= a (= a b)))
(check-sat)
```

After running `UnconstrainedSimplifier::visitAll()` on both assertions,
we end up with `[b]` as our `d_unconstrained` set. We end up inferring
the substitution `(= a b) --> b` and get `(not b)` and `b`, which is
unsat even though the original problem is sat.

This commit fixes the issue by visiting all the children of a node if we
visit a node for a second time. This makes sure that we remove any
children from the visisted-once set.

(proof-new) Updates to proof node manager (#4617)

Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities.

It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode.

Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.

New C++ API: Remove examples for old API. (#4650)

This removes obsolete examples for the old API in preparation of making
the old API private. Examples for the new API are renamed from
*-new.cpp to *.cpp.

Add support for eqrange predicate (#4562)

This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.

(proof-new) Add REWRITE trust node kind. (#4624)

This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.

get-authors: Add alias for nafur. (#4646)

Allow for better interaction of Integer/Rational with mpz_class/mpq_class. (#4612)

(proof-new) Add proof-new to options file (#4641)

Adds proof-new as an option. This is required for adding code that is guarded by this option while we are in the process of merging work on the new proofs infrastructure.

Enabling the option currently throws an option exception.

Add trascendental function kinds to list of unevaluated operators (#4640)

Fixes #4636.

This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).

fix (#4637)

The help message of --bv-print-consts-as-indexed-symbols seems wrong to me, and this PR suggests a fix.

Use traversal iterators in IntToBv (#4169)

This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators.

Also, cleaned `childrenTypesChanged` a bit.

While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes).

Add Match utility function. (#4632)

(proof-new) Make static methods in re-elim (#4623)

In preparation for coarse-grained rule for re-elim to be used by the solver and proof checker.

(proof-new) CDProof inherits from ProofGenerator (#4622)

This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.

Add casc j10 scripts (#4621)

Adds scripts submitted to CASC competition.

Note that this version of CVC4 submitted to CASC was modified to allow models when --sort-inference is enabled, since model output is required.

(proof-new) Updates to strings term registry (#4599)

This makes it so that methods for constructing term registration lemmas are made into static methods, so that they can be used by both the term registry and proof checker.

Convert more uses of strings to words (#4584)

Towards theory of sequences.

This PR also adds support for sequences in default sygus grammars.

Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.

(proof-new) Split operator elimination from arithmetic (#4581)

This class will be undergoing further refactoring for the sake of proofs.

This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.

Clean the header file of TheoryStrings (#4272)

Now conforms to coding guidelines. For the sake of ensuring that the aspects related to the strategy were maintained in one place, I split this to its own file, strategy.h/cpp.

Update version information post 1.8 release (#4635)

Always rewrite boolean ITEs with constant then/else-branches (#4619)

Also adds better tracing and rewrites for binary AND/OR to account for reductions from constant ITEs.

An evaluation of master vs this commit, with 600s, no options, shows the impact of this commit to be negligible and mostly restricted to QF_LIA. Below there is a summary and a list of the unique solves.
```
 Benchmark |  Stat  Slvd   Tot   To Mo Err    Cpu[s]   Mem[MB] Uniq |  Stat  Slvd   Tot   To Mo Err    Cpu[s]   Mem[MB] Uniq |
   QF_ALIA |    ok   125   126    1  0   0    2382.6    5410.8    0 |    ok   125   126    1  0   0    2322.1    5211.8    0 |
     QF_AX |    ok   549   551    2  0   0    2381.4    2533.1    0 |    ok   549   551    2  0   0    2400.8    2676.4    0 |
    QF_IDL |    ok  1682  2193  511  0   0  399395.4  491490.3    3 |    ok  1682  2193  511  0   0  400813.9  491129.9    3 |
    QF_LIA |    ok  4419  6947 2521  7   0 1774140.9 2782838.1   27 |    ok  4409  6947 2531  7   0 1775886.7 2785165.7   17 |
   QF_LIRA |    ok     5     7    2  0   0    1209.9    3626.9    0 |    ok     5     7    2  0   0    1209.5    3707.2    0 |
    QF_LRA |    ok  1517  1648  131  0   0  134215.1  170443.1    3 |    ok  1516  1648  132  0   0  134819.6  169942.7    2 |
    QF_RDL |    ok   210   255   45  0   0   32896.0   23261.0    0 |    ok   210   255   45  0   0   32902.7   23312.5    0 |
     QF_UF |    ok  7444  7457   13  0   0   16156.4   74432.9    0 |    ok  7444  7457   13  0   0   16043.8   75067.6    0 |
  __totals |    ok 15951 19184 3226  7   0 2362777.7 3554036.2   33 |    ok 15940 19184 3237  7   0 2366399.2 3556213.8   22 |```
```
                                                                                                DIRECTORY |                         master |                         branch |
                                                                                                Benchmark |  Stat  RES Exit Cpu[s] Mem[MB] |  Stat  RES Exit Cpu[s] Mem[MB] |
       non_incremental_QF_IDL/asp-GraphPartitioning-rand_21_150_1235870252_0_k=3_v=10_e=20_unsat.gph.smt2 |    to    -    2  600.1   246.4 |    ok   20    0 596.71   245.9 |
                                              non_incremental_QF_IDL/asp-SchurNumbers-15.13.schur.lp.smt2 |    ok   10    0 533.64   243.8 |    to    -    2 600.07   246.8 |
                                            non_incremental_QF_IDL/job_shop-jobshop38-2-19-19-4-4-12.smt2 |    ok   10    0 586.13   221.5 |    to    -    2 600.09   216.8 |
                                               non_incremental_QF_IDL/queens_bench-n_queen-queen82-1.smt2 |    to    -    2 600.01   197.8 |    ok   10    0 570.36   198.9 |
                                          non_incremental_QF_IDL/schedulingIDL-tai_15x15_3_mkspan871.smt2 |    to    -    2  600.1   128.0 |    ok   10    0  586.8   127.8 |
                                          non_incremental_QF_IDL/schedulingIDL-tai_15x15_9_mkspan930.smt2 |    ok   10    0 575.55   124.4 |    to    -    2 600.07   122.6 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1007795.smt2 |    ok   10    0 334.96   386.7 |    to    -    2 600.02   335.5 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1008025.smt2 |    ok   10    0 180.57   384.6 |    to    -    2 600.02   338.6 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1107622.smt2 |    ok   10    0 310.68   349.2 |    to    -    2 600.01   341.3 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1275621.smt2 |    ok   10    0   5.59   232.0 |    to    -    2 600.04   407.4 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1360077.smt2 |    ok   10    0  422.4   667.7 |    to    -   11 591.94   663.2 |
                                             non_incremental_QF_LIA/arctic-matrix-constraint-1765766.smt2 |    to    -   11 598.02   656.8 |    ok   10    0   62.5   669.8 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-391798.smt2 |    ok   10    0    9.0   119.3 |    to    -    2 600.08   131.8 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-481231.smt2 |    ok   10    0 402.37   220.9 |    to    -    2 600.09   199.6 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-689472.smt2 |    ok   10    0  28.51   155.9 |    to    -    2 600.06   215.1 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-864173.smt2 |    ok   10    0 125.59   326.3 |    to    -   11 597.87   348.8 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-901628.smt2 |    to    -    2 600.04   225.5 |    ok   10    0 391.31   228.3 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-916576.smt2 |    to    -    2 600.01   244.4 |    ok   10    0  432.4   246.9 |
                                              non_incremental_QF_LIA/arctic-matrix-constraint-928134.smt2 |    ok   10    0 447.55   222.7 |    to    -    2 600.06   264.7 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-42.smt2 |    ok   10    0 579.39   414.9 |    to    -    2 600.07   417.4 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-27-47.smt2 |    to    -    2 600.02   604.2 |    ok   10    0 594.54   603.6 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-45-43.smt2 |    to    -    2 600.05   628.1 |    ok   10    0 588.25   627.6 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-46-47.smt2 |    ok   10    0 589.88   570.0 |    to    -    2 600.09   566.9 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-47.smt2 |    ok   20    0 590.89   599.9 |    to    -    2 600.01   598.4 |
                                        non_incremental_QF_LIA/nec-smt-large-checkpass_pwd-prp-54-50.smt2 |    ok   10    0 594.72   804.7 |    to    -   11 593.13   843.5 |
                                      non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-17-47.smt2 |    ok   20    0 593.29   524.2 |    to    -    2 600.08   522.8 |
                                      non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-20-48.smt2 |    to    -    2 600.02   562.5 |    ok   10    0 594.33   560.3 |
                                       non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-5-46.smt2 |    to    -    2 600.09   492.9 |    ok   10    0 576.02   491.9 |
                                      non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-52-47.smt2 |    to    -    2 600.02   532.2 |    ok   20    0  592.3   533.4 |
                                      non_incremental_QF_LIA/nec-smt-large-getoption_group-prp-53-48.smt2 |    ok   20    0 599.82   729.4 |    to    -    2 600.02   742.1 |
                                       non_incremental_QF_LIA/nec-smt-large-getoption_user-prp-41-47.smt2 |    to    -   11 589.46  1377.2 |    ok   20    0 580.82  1380.1 |
                                     non_incremental_QF_LIA/nec-smt-large-user_is_in_group-prp-23-46.smt2 |    to    -    2 600.08   633.5 |    ok   10    0 576.07   634.0 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1015084.smt2 |    ok   10    0 408.08   374.5 |    to    -    2 600.01   336.4 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1206577.smt2 |    ok   10    0 361.82   375.4 |    to    -   11 593.45   288.4 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1268455.smt2 |    ok   10    0 270.87   654.3 |    to    -    2 600.08   670.5 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1270163.smt2 |    to    -    2 600.02   410.4 |    ok   10    0 425.02   420.6 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1270998.smt2 |    ok   10    0 349.91   384.6 |    to    -    2 600.01   417.5 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1290859.smt2 |    to    -    2  600.1   365.9 |    ok   10    0 117.77   270.0 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1361831.smt2 |    to    -    2 600.07   431.0 |    ok   10    0 421.55   686.9 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1452366.smt2 |    to    -    2 600.04   439.4 |    ok   10    0  87.42   451.9 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1791895.smt2 |    to    -    2  600.1   480.3 |    ok   10    0 102.16   459.7 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-1908553.smt2 |    to    -    2 600.01   713.8 |    ok   10    0  22.22   394.9 |
                                           non_incremental_QF_LIA/tropical-matrix-constraint-2061672.smt2 |    ok   10    0   51.6   521.2 |    to    -    2 600.04   545.8 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-244431.smt2 |    ok   10    0 292.95    88.2 |    to    -    2 600.01    97.7 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-368069.smt2 |    to    -    2 600.05   135.3 |    ok   10    0 445.93   134.2 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-369883.smt2 |    ok   10    0 510.59   134.2 |    to    -    2 600.01   127.7 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-527358.smt2 |    ok   10    0 243.33   135.0 |    to    -    2 600.05   140.7 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-614657.smt2 |    ok   10    0 515.89   209.6 |    to    -    2 600.07   166.6 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-645054.smt2 |    ok   10    0  41.34   185.3 |    to    -    2 600.08   205.1 |
                                            non_incremental_QF_LIA/tropical-matrix-constraint-794687.smt2 |    ok   10    0 502.03   235.3 |    to    -    2 600.07   242.0 |
          non_incremental_QF_LRA/LassoRanker-CooperatingT2-sas2.t2.c_Iteration7_Loop_7-phaseTemplate.smt2 |    ok   20    0  593.7   591.3 |    to    -    2 600.03   614.7 |
 non_incremental_QF_LRA/LassoRanker-SV-COMP-aviad_true-termination.c_Iteration1_Loop_4-phaseTemplate.smt2 |    ok   10    0 594.16   738.5 |    to    -    2 600.03   701.6 |
             non_incremental_QF_LRA/LassoRanker-Ultimate-Collatz.bpl_Iteration1_Loop_2-pieceTemplate.smt2 |    to    -    2 600.09   711.5 |    ok   20    0 593.46   711.2 |
                                            non_incremental_QF_LRA/tropical-matrix-constraint-199552.smt2 |    ok   10    0 268.04    71.2 |    to    -    2 600.05    81.6 |
                                            non_incremental_QF_LRA/tropical-matrix-constraint-223827.smt2 |    to    -    2 600.06    91.9 |    ok   10    0 505.07    95.9 |```

Update info for 1.8 release (#4633)

Cleanup examples (#4634)

This commit removes examples from unsupported programming languages and
fixes a compilation issue in the sets-translate example. The issue
arised due to changes to the `DefineFunctionCommand` in commit
fd60da4a22f02f6f5b82cef3585240c1b33595e9 and wasn't detected by our CI
because the sets-translate example requires Boost.

Generalize atom collection in old proof code (#4626)

Before terms in assertions that are not sent to the SAT solver could be collected by the old proof code as atoms and thus expected to have a corresponding SAT variable. This commit fixes this by making the atom collection from assertions more conservative.

Bv to int elimination bugfix (#4435)

fix 1:
------
The wrong flag was checked in the traversal, causing an assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b37a15d509b8a11551401f/src/preprocessing/passes/bv_to_int.cpp#L247)
This is fixed in this PR. A test was added as well.

fix 2:
------
It is desirable that bv-to-bool runs before bv-to-int, but this was not the case, and is fixed in this PR.

Do not merge until after competition release (label added).

Add logic check for define-fun(s)-rec (#4577)

This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at
the level of the new API that checks whether the logic is quantified and
includes UF. To make sure that the parser actually executes that check,
this commit converts the `DefineFunctionRecCommand` command to use the
new API instead of the old one. This temporarily breaks the `exportTo`
functionality for `DefineFunctionRecCommand` but this is not currently
used within the CVC4 code base (and it seems unlikely that users use
commands).

Revert "[Python] Properly destroy CVC4 object (#3753)" (#4422)

This reverts commit bfa008a7ce13eff2f59b022e8c2d5d71d77f9ecb.

Improve memory management in Java bindings (#4629)

Fixes #2846. One of the challenges of the Java bindings is that the
garbage collector can delete unused objects at any time in any order.
This is an issue with CVC4's API because we require all `Expr`s to be
deleted before the corresponding `ExprManager`. In the past, we were
using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of
`ExprManager`. The problem is that we can have multiple instances of the
wrapper that internally all refer to the same `ExprManager`. This commit
implements a different approach where the Java wrappers hold an explicit
reference to the `ExprManager`. The commit also removes some unused or
unimportant API bits from the bindings.

Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)

Fixes #4620.

The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.

A general example of this unsoundness:

(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.

Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.

Improve polynomial anyterm grammar (#3566)

This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation.

This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).

Updates to NEWS. (#4628)

Simplify sygus conversion script. (#4627)

Update copyright headers.

Add missing REQUIRES to new regressions. (#4625)