[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.

 Split regular expression solver (#2891)

New C++ API: Fix include. (#2896)

BV: Fix typerules for rotate operators. (#2895)

Fix memory leak when using subsolvers (#2893)

ASAN was reporting memory leaks in regression tests that were using
subsolvers. First, I am going to describe the origin of the leaks and
then the solution implemented in this commit.

Recall an `Expr` stores the `NodeManager` that the internal node is
associated with. `Node::toExpr()` converts a `Node` to an `Expr` and
assumes that the active `NodeManager` (returned by
`NodeManager::currentNM()` is the one associated with the node. In
`ExportPrivate::exportInternal()`, when we were exporting a skolem, we
created a skolem in the target `NodeManager` by calling
`NodeManager::mkSkolem()` (`ExprManager`s do not support the creation of
skolems) but then we called `Node::toExpr()` on the resulting skolem
while the origin `NodeManager` was the active `NodeManager`. One of the
issues of having the wrong `NodeManager` in the `Expr` is that when the
`Expr` is destroyed and the internal node's refcount reaches zero in
destructor of `Expr`, then the node value associated with the node is
added to the set of zombie nodes (nodes waiting to be garbage collected
or resurrected) of the wrong `NodeManager`. The problem here is that the
set of zombie nodes uses the node id to hash and compare nodes. Node
ids, however, are only unique within a given `NodeManager`. Thus, if we
have two nodes with the same id from different `NodeManager`s and both
reach refcount zero in the context of the same `NodeManager`, only one
of them will end up in the set of zombies and thus only that one will be
freed.
Using a subsolver realiably triggered this issue.
`ExportPrivate::exportInternal()` stored the `Expr` with the wrong
`NodeManager` in an `ExprManagerMapCollection` which associates
variables in the original `ExprManager` with the variables in the target
`ExprManager`. When we created a subsolver, we created the
`ExprManagerMapCollection` before creating our subsolver, so it was
deleted after the subsolver and so deleting the
`ExprManagerMapCollection` deleted the last reference to `Expr`s holding
skolem nodes associated with the wrong `NodeManager`.

This commit fixes the issue by making sure that the correct
`NodeManager` is in scope when converting the skolem/bound variable
nodes to an `Expr`. It also swaps the creation order of
`ExprManagerMapCollection` and `ExprManager` to make sure that
`ExprManagerMapCollection` is deleted before the `ExprManager` that the
`Expr`s belong to. Additionally, the commit makes it harder to make a
similar mistake by asserting that the `Expr`s in the
`ExprManagerMapCollection` are associated with the expected
`ExprManager`s. Finally, it adds an assertion that tries to identify
such issues by checking whether the list of zombies contains a node with
the same id but located at a different address.

Strip non-matching beginning from indexof operator (#2885)

This commit adds a rewrite that strips endpoints from `str.indexof`
operators if they don't overlap with the string that is being searched
for using `stripConstantEndpoints()`. In addition to that, it makes
`stripConstantEndpoints()` slightly more aggressive by allowing it to
drop substring components that have zero overlap with the string that we
are looking at. Finally, the commit fixes the default argument for
`fullRewriter` of `checkEntailContains()` to be true instead of false,
which should allow for more rewriting opportunities.

Revisit strings extended function decomposition  (#2892)

Fix instantiation stat for fmf (#2889)

More fixes for PBE with datatypes (#2882)

fix help information on TPTP parsing (#2884)

Fix stripConstantEndpoints in strings rewriter (#2883)

`TheoryStringsRewriter::stripConstantEndpoints()` returns the stripped
endpoints in the vectors `nb` and `ne`. These endpoints were not
computed correctly if string literal had to be split. For example:

```
stripConstantEndpoints({ "ABC" }, { "C" }, {}, {}, 1)
```

returned `true` and only "A" for `nb` (instead of "AB") because we
mistakenly used the amount of overlap between "ABC" and "C" (which is
one) for the length of the stripped prefix.

This commit fixes the issue and adds several unit tests.

Use empty vector instead of false in query with null Expr assumption (#2876)

This solution is less confusing than using a `false` assumption.

 Fix bad comparison in RE solver's addMembership (#2880)

Rewrite selectors correctly applied to constructors (#2875)

Add more NEWS (#2859)

Sygus abduction feature (#2744)

Make declare-datatype(s) a standard, non-extended command in the Smt2 parser. (#2874)

Fix fairness issue with fast sygus enumerator (#2873)

New C++: Remove redundant mkBoundVar function.

New C++: Remove redundant mkVar function.

s

BitVector: Allow base 10 in constructor. (#2870)

Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)

Fixes #1715. We do not support the `--solve-int-as-bv=X` preprocessing
pass with logics other than pure QF_NIA/QF_LIA/QF_IDL. This commit adds
a corresponding check and throws an option exception if an incompatible
logic has been set.

Enable CryptoMiniSat-backed BV proofs (#2847)

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
   * Specifically, CNF proofs broke when proving tautological clauses.
     Now they don't.

New beta-reduction for HOL solving (#2869)

Adding capture avoiding substitution (#2867)

Fix non-variable function head elimination in UF. (#2864)

Fix function term set for theory strings compute care graph. (#2862)