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

Fix handling of Boolean term variables (#4550)

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

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

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

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

Fix lifetime and copy issues with NodeDfsIterable (#4569)

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

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

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

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

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

## Issue

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

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

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

## Solution

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

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

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

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

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

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

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

Wrap Result in Python API (#4473)

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

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

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

Add sygus datatype substitution utility method (#4390)

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

Fix abduction with datatypes (#4566)

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

Theory strings preprocess (#4534)

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

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

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

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

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

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

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

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

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

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

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

Fixes #4437.

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

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

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

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

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

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

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

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

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

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

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

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

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

Fixes #4476.

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

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

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

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

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

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

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

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

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

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

This includes some formatting changes.

Set theoryof-mode after theory widening (#4545)

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

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

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

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

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

Incorporate sequences into the word interface (#4543)

Also renames a function mkWord -> mkWordFlatten.

Do not cache operator eliminations in arith (#4542)

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

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

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

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

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

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

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

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

Add the sequence type (#4539)

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

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

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

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

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

Add the Expr-level sequence datatype (#4526)

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

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

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

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

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

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

Convert more uses of strings to words (#4527)

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

Issue found by coverity.

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

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

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

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

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

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

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