NA Tangent reverse implication (#3050)

 Minor cleaning of conflict-based instantiation (#2966)

Do not require sygus constructors to be flattened (#3049)

 Fix spurious assertion in get-value (#3052)

Optimization for negative concatenation membership. (#3048)

Optimization for strings normalize disequalities (#3047)

Prevent letification from shadowing variables (#3042)

Fixes #3005. When printing nodes, we introduce `let` expressions on the
fly. However, when doing that, we have to be careful that we don't
shadow existing variables with the same name. When quantifiers are
involved, we do not descend into the quantifiers to avoid letifying
terms with bound variables that then go out of scope (see #1863). Thus,
to avoid shadowing variables appearing in quantifiers, we have to
collect all the variables appearing in that term to make sure that the
let does not shadow them. In #3005, the issue was caused by a `let` that
was introduced outside of a quantifier and then was shadowed in the body
of the quantifier by another `let` introduced for that body.

DRAT-Optimization (#2971)

This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.

These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically,  proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:

## DRAT Optimization

The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.

## CNF Representation

The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.

## Small Fixes to Signatures

When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.

Add support for SWIG 4 (#3041)

SWIG 4 seems to change the name for `std::map<CVC4::Expr, CVC4::Expr>`
to include the implicit template argument for comparisons. To make the
code compatible with both SWIG 4.0.0 and older versions, this commit
creates an explicit instance of the template.

Enable proof checking for QF_LRA benchmarks (#2928)

Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).

Add check that result matches benchmark status (#3028)

This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`.  In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.

[SMT-COMP] No unconstrained simp for QF_LIA UC (#3039)

`--unconstrained-simp` is not compatible with unsat cores.

[SMT-COMP] Increase sequential portfolio times (#3038)

This year's timeout is 40min up from 20min last year. This commit scales
the timeouts accordingly.

[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)

We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.

Enable SymFPU assertions in production (#3036)

This commit enables SymFPU assertions in production. The reason for this
is that there are some known problems with certain bit-widths, so we
prefer to be conservative. The commit also updates the run scripts for SMT-COMP 2019 to use `--fp-exp` since we have those additional checks in place now.

[SMT-COMP 2019] Update run script for unsat cores (#3034)

`--unconstrained-simp` is not compatible with unsat cores, so this
commit removes it for QF_LRA. `--bitblast=eager` is not compatible with
unsat cores for QF_UFBV because the dependencies are not tracked
correctly in the Ackermannization preprocessing pass, so the commit
changes the script to use the lazy BV solver instead. Strings need some
additional options to use the correct theory symbols.

Add check for limit of number of node children (#3035)

This commit adds a check that makes sure that we do not try to create
nodes with more children than the maxmimum number. This can currently
happen when flattening nodes in QF_BV with lots of duplicate children.

Update QF_BV options for SMT-COMP 2019. (#3033)

 Require that FMF model basis terms are variables (#3031)

The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.

Fix rewriter for regular expression consume  (#3029)

Quote symbol when printing empty symbol name (#3025)

When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.

Avoid substituting Boolean term variables (#3022)

Fixes #3020. Boolean terms that appear in other terms, e.g. a Boolean
array index, are replaced by `BOOLEAN_TERM_VARIABLE`s to make sure that
they are handled properly in theory combination. When doing this
replacement, an equality of the form `(= <Boolean term> <Boolean term
variable)` is added to the assertions. The problem was that
`Theory::ppAssert()` would derive a substitution when this equality was
registered. The commit fixes the problem by not allowing to add
substitutions for `BOOLEAN_TERM_VARIABLE`s.

Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)

Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent.  The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.

[SMT-COMP 2019] Update run scripts to match tracks (#3018)

The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.

FP: Fix regression test and enable SymFPU on Travis. (#3013)

Update QF_NIA strategy (#3012)

[SMT-COMP2019] Better strings configuration (#3010)

Support for incremental bit-blasting with CaDiCaL (#3006)

This commit adds support for eager bit-blasting with CaDiCaL on
incremental benchmarks. Since not all CaDiCaL versions support
incremental solving, the commit adds a CMake check that checks whether
`CaDiCaL::Solver::assume()` exists.

Note: The check uses `check_cxx_source_compiles`, which is not very
elegant but I could not find a better solution (e.g.
`check_cxx_symbol_exists()` does not seem to support methods in classes
and `check_struct_has_member()` only seems to support data members).

Fix BV ITE rewrite (#3004)

The rewrite `BvIteConstChildren` assumes that `BvIteEqualChildren` has
been applied before it runs. However, with nested ITEs, it was possible
to violate that assertion. Given `bvite(c1, bvite(c2, 0, 0), bvite(c3,
0, 0))`, `BvIteEqualChildren` would rewrite that term to `bvite(c2, 0,
0)`. The `LinearRewriteStrategy` then ran `BvIteConstChildren` on
`bvite(c2, 0, 0)` which complained about the equal children. This commit
implements a simple fix that splits the `LinearRewriteStrategy` into two
strategies to make sure that if `BvIteEqualChildren` rewrites a node, we
drop back to the `Rewriter`. This ensures that the rewrites on the
rewritten node are invoked in the correct order.

Add the problematic input from issue 2183 as a regression test (#3008)

Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.

Fix iterators in Java API (#3000)

Fixes #2989. SWIG 3 seems to have an issue properly resolving
`T::const_iterator::value_type` if that type itself is a `typedef`.
This is for example the case in the `UnsatCore` class, which `typedef`s
`const_iterator` to `std::vector<Expr>::const_iterator`. As a
workaround, this commit changes the `JavaIteratorAdapter` class to take
two template parameters, one of which is the `value_type`. The commit
also adds a compile-time assertion that `T::const_iterator::value_type`
can be converted to `value_type` to avoid nasty surprises. A nice
side-effect of this solution is that explicit `typemap`s are not
necessary anymore, so they are removed. Additionally, the commit adds a
`toString()` method for the Java API of `UnsatCore` and adds examples
that show and test the iteration over the unsat core and the statistics.
Iterating over `Statistics` now returns instances of `Statistic` instead
of `Object[]`, which is a bit cleaner and requires less glue code.

cmake: Install JAR and JNI files for Java bindings. (#3002)

Default install paths are:
  - libcvc4jni.so in /usr/lib/
  - CVC4.jar in /usr/share/java/cvc4

Fixes #2990.

 BV: Do not enable abstraction when eager bit-blasting by default. (#3001)

Fix model of Boolean vars with eager bit-blaster (#2998)

When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.

Fix printing of bvurem (#2963)

Disable relational triggers (#2994)

Fixes for relational triggers (#2967)

Add support for re.all (#2980)

Simple optimizations to core strings theory. (#2988)

Fix re-elim-agg regressions (#2987)

 Use total versions of div/mod in re-elim-agg (#2986)

Fix concat-find regexp elimination (#2983)

Remove stoi solve rewrite (#2985)

Fix use of APPLY kind in examples (#2984)

Eliminate APPLY kind (#2976)

Optimization for evaluation with unfolding (#2979)

New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

Fix compiler warning. (#2975)

Do not use __ prefix for header guards. (#2974)

Fixes 2887.

Dco fix (#2973)

README: Remove project leaders, history.

CONTRIBUTING: Fix project leaders link.

[BV] An option for SAT proof optimization (#2915)

* [BV] An option for SAT proof optimization

The option doesn't **do** anything yet, but exists.

* CopyPaste Fix: BvOptimizeSatProof documentation

It was the documentation for a different option. Now it has been
updated.

* Fix Typos per Mathias' review.

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

Refactor normal forms in strings (#2897)

Add CONTRIBUTING file. (#2968)

Fail fast strategy for propagating instances (#2939)

 Less aggressive caching in equality engine when proofs are enabled (#2964)

Cache explanations in the equality engine (#2937)

More use of isClosure  (#2959)

Fix extended function decomposition (#2960)

Fixes #2958.

The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.

The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.

Add interface for term enumeration (#2956)

Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)

The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`.  This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.

References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)

Stratify enumerative instantiation (#2954)

Minor simplifications to theory quantifiers (#2953)

Check for rt library in configuration -- support for glibc<2.17 (#2854)

This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page.

Initial version of run scripts for SMT-COMP 2019 (#2951)

For now, they are just copies of the 2018 version of the scripts.

Referring to prerelease 1.8 (#2943)

 Eliminate Boolean ITE within terms, fixes 2947 (#2949)

Removing references to cvc4-bugs@... (#2945)

"prerelease -> release" in INSTALL (#2944)

Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.

fix copyright year in configuration file (#2942)

prerelease -> release (#2941)

Fix another corner case of datatypes+PBE (#2938)

fix fp issue (#2940)

SatClauseSetHashFunction (#2916)

* SatClauseHashFunction

Added to the same file as SatLiteralHashFunction.

* clang-format

Thanks Andres!

adding sygus news (#2934)

Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)

Update release notes and lib version (#2933)

Update copyright headers.

get-authors: Add GitHub user ayveejay -> Andrew V. Jones.

Fix combination of datatypes + strings in PBE (#2930)

FP: Fix wrong model due to partial assignment (#2910)

For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.

Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)

`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.

Update includes to use cvc4 top-level directory in examples (#2877)

Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well.

Move slow string regression to regress3 (#2913)

Modify strategy in sets+cardinality (#2909)

Apply empty splits more aggressively in sets+cardinality (#2907)

removing deprecated rewriting signature / example (#2906)

Fix freeing nodes with maxed refcounts (#2903)

Fix issues in cvc parser (#2901)

fix ex_bv.plf (#2905)

Update copyright headers.

update-copyright: Update to 2019.

get-authors: Exclude empty lines.

Fix warnings about wrong line numbers (#2899)

Fix a few warnings (#2898)

get-authors: Exclude common source code patterns. (#2900)

Exclude lines that #include header files and define namespaces.
Since we use git blame -C -M to determine the current top contributors,
git tries to match all #include and namespace definitions to an original
author, which is not accurate since these lines are usually not
copied over from other files.

update-copyright: Fix matching of excluded paths.

get-authors: Readd option -C to git blame command.