(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)

BV: Fix querying equality status in lazy bit-blaster. (#4618)

Fixes #4076.

In the lazy bit-blaster, when querying the equality status, if the SAT
solver has a full model, it is queried for the model values of the
operands of the equality. However, the check if the bit-blaster has a
full model did not consider the case where no assertions have yet been
added, which leads to querying values of bits that are still unassigned
in the SAT solver.

Co-authored-by: <mathias.preiner@gmail.com>

Fix regressions in regress1 after #4613. (#4616)

(proof-new) Add quantifiers proof checker (#4593)

Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.

This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.

(proof-new) Update proof node, add proof node algorithm utility file. (#4600)

Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.

Support AND/OR definitions in lambda to array rewriting (#4615)

This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR.

This also improves tracing and makes a few parts of the code adhere to code guidelines.

BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)

Fixes #4075.

BV: Add missing type check for INT_TO_BITVECTOR. (#4613)

Fixes #4130.
This further makes an attempt at more consistent error printing.

 Do RE derivation inference only for concrete constant RE (#4609)

The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.

Move sygus datatype utility functions to their own file (#4595)

Separates them from the core datatype utilities.

Code move only.

Update to consistent policy for removed terms in quantifier bodies. (#4602)

(proof-new) Term conversion proof generator utility (#4603)

This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.

(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)