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)

Improve INSTALL instructions. (#2866)

Use zero slope tangent planes for transcendental functions (#2803)

Properly handle lambdas in relevant domain (#2853)

 Add getFreeVariables method to node algorithm (#2852)

Disable DCO signing for organization members.

Implement proper semantics for TPTP predicate is_rat. (#2861)

 Fix substitution step in ho matching (#2825)

Generalize sygus-rr-verify for fast enumerator (#2829)

check for null assumption in query and replace with false (#2858)

The default assumption argument in query was a null `Expr`, but the implementation asserted that the assumption is not null:

declaration: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.h#L593
implementation: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3548

The change is to simply check if the assumption is null and replaces it with the `false` expression if it is.

It should be `false` not `true` because it is negated in checkSatisfiability (when it's a query) as seen here: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3607

Note: I couldn't find a clean way to make `false` the default argument of assumption, because the expression manager is non-static.

Add statistics for proof gen./checking time, size (#2850)

This commit adds a statistic that records the total size of all proofs
generated by an instance of `SmtEngine`. The commit also moves
`SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know
the complete type of `d_stats` (and the separate file for that method
didn't seem that useful). Additionally, it changes
`smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime`
that only measures the time spent in LFSC and adds a statistic
`proof::ProofManager::proofProductionTime` that measures the proof
production time separately (also works with `get-proof`/`--dump-proof`).

Remove spurious data member. (#2857)

Fix public headers for make install. (#2856)

This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4.
Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).

Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)

 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)

ErProof class with LFSC output (#2812)

* ErProof class with LFSC output

* Created a TraceCheckProof class
   * parsable from text
* Created an ErProof class
   * constructible from a TraceCheckProof
   * writable as LFSC
* A bunch of unit tests

* Reponded to Mathias's first set of comments.

Credits to Mathias for many of the fixes!

* Responed to Andres's first set, fixed tests

I accidentally deleted a "!" last time, causing stuff to fail.

* Use Configuration::isAssertionBuild

* Clarified comment

* Responded to Andres's 2nd review

* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.

Use string stream for proofs instead of tmp files (#2841)

This commit changes CVC4 to use a string stream instead of a temporary
files for proof checking. Note: This change requires a version of LFSC
that supports checking streams (see
https://github.com/CVC4/LFSC/pull/14).

Tested: `make check` passed, changing `holds` to `xholds` in the proof
produced by proof_manager.cpp makes the proofs fail.

ClangFormat: Disable DerivePointerAlignment (#2842)

The option `DerivePointerAlignment` tries to automatically determine the
pointer alignment used by the input. In our case, we would eventually
like the code base to be consistent throughtout, so this commit disables
that option.

New C++ API: Remove redundant declareFun function. (#2837)

Rewrite simple regexp pattern to str.contains (#2827)

New C++ API: Remove redundant mkTerm function. (#2836)

Delete temporary proof files when aborting CVC4 (#2834)

CVC4 was not deleting temporary proof files when crashing or being
terminated externally. This commit uses an early `unlink()` to remove
the files as soon as CVC4 terminates.

New C++ API: Unit tests for declare* functions. (#2831)

Make stripConstantEndpoints() less aggressive (#2830)

Add rewrite for contains + const strings replace (#2828)

Fix corner case in stripConstantEndpoints (#2824)

`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.

Fix warning due to catching polymorphic exceptions (#2821)

New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

Strings: Remove redundant replace rewrite (#2822)

Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.

Extended DRAT signature to operational DRAT (#2815)

* Extended DRAT signature to operational DRAT

The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.

The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).

You can run the new AND old DRAT tests by running

```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Apply suggestions from code review (Yoni)

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

Avoid using ProofManager in non-proof CMS build (#2814)

PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.

Strings: Strengthen multiset reasoning (#2817)

This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.

 Fix tuple and record CVC printing (#2818)

 Fix parsing of overloaded parametric datatype selectors (#2819)

New README (markdown). (#2797)

Fix missing-override warning (#2811)

`TLazyBitblaster::setProofLog()` was defined even though the method was
not virtual before PR #2808 and `TBitblaster` was implementing the same
method. After that PR, which made the method virtual, GCC complained
about a missing `override` keyword for `setProofLog()`. However, the
method should have been removed (see
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247299617)).
This commit removes the function definition.

Extract DIMACS Printing (#2800)

Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.

However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.

At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.

Strings: Introduce checkEntailContains() (#2809)

 Fix ABC build (#2808)

PR #2786 introduced a pure virtual method `TBitblaster::getSatSolver()`.
`AigBitblaster` was missing the implementation of that method. This
commit adds an implementation that simply returns the underlying SAT
solver. Note: The method is currently only used for proofs and CVC4 does
not support proofs in combination with ABC. To make this explicit, the
commit also adds a check in `SmtEngine::setDefaults()` that makes sure
that we are not trying to produce proofs with `--bitblast-aig` (before
the commit, we just crashed with an assertion failure/null pointer
dereference).

Add option to print BV constants in binary (#2805)

This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.

Update NEWS file (#2804)

Bugfix: LFSC clause equality (#2801)

* Bugfix: LFSC clause equality

My implementation of clause equality had an undocumented assumption that
the clauses didn't have any duplicate literals. Now that assumption is
gone, and the tests suite has been expanded.

* Added an empty clause test

* Typo fix: Yoni

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Yoni's comments

* Remove a duplicate clause_eq test.
* Add an ordering clause_eq test.
* Improve the documentation of clause_eq.

Extended Resolution Signature (#2788)

* Extended Resolution Signature

While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form

    new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)

This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:

   1. Introducing a **fresh** variable, defined in the form above
   2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
      clauses in the form of two clauses, and a cnf with $$ n $$ clauses
   3. An axiom for unrolling the proof of the cnf into proofs of the
      original clauses.

* Addressing Yoni's comments

1. Added a new (trivial) test
2. Improved a bunch of documentation

* Update proofs/signatures/er.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Removed references to RATs from the signature

There are still a few references in the header comment.

* Aside on continuations

* Scrap the elision annotations

Fix constant contains ITOS rewrite (#2799)

CMake: Fix search for static libraries (#2798)

When configuring CVC4 with `--static`, we change
`CMAKE_FIND_LIBRARY_SUFFIXES` to prefer static libraries (`*.a`) over
shared ones. However, instead of prepending `.a` to the list of
`CMAKE_FIND_LIBRARY_SUFFIXES`, we created a single element with `.a` and
the previous list.

Output of `message("${CMAKE_FIND_LIBRARY_SUFFIXES}")` before the change:

```
.a .tbd;.dylib;.so;.a
```

After the change:

```
.a;.tbd;.dylib;.so;.a
```

On macOS, both the static and the shared library of GMP are available
(when installed via homebrew) and before the change, CMake would pick the
shared library when compiling with `--static --no-static-binary`. This
commit fixes that issue.

Strings: Add option to change loop process mode (#2794)

This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.

 Fix unsound double abs rewrite rule for FP (#2792)

 Only check disequal terms with sygus-rr-verify (#2793)

ClausalBitvectorProof (#2786)

* [DRAT] ClausalBitvectorProof

Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)

It fits into the `BitvectorProof` class hierarchy like this:

```
              BitvectorProof
              /            \
             /              \
ClausalBitvectorProof  ResolutionBitvectorProof
```

This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
   * CnfStream
   * SatSolver (specifically the BvSatSolver)
   * CnfProof
   * TheoryProof
   * TheoryBV
   * Both bitblasters

And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.

This means that references to and interactions with (R)BVP were
pervasive.

Nevertheless, an SMT developer must persist.

The change summary:
  * Create a subclass of BVP, called ClausalBitvectorProof, which has
    most methods stubbed out.
  * Make a some modifications to BVP and ResolutionBitvectorProof as the
    natural division of labor between the different classes becomes
    clear.
  * Go through all the components in the first list and try to figure
    out which kind of BVP they should **actually** be interacting with,
    and how. Make tweaks accordingly.
  * Add a hook from CryptoMinisat which pipes the produced DRAT proof
    into the new ClausalBitvectorProof.
  * Add a debug statement to ClausalBitvectorProof which parses and
    prints that DRAT proof, for testing purposes.

Test:
  * `make check` to verify that we didn't break any old stuff, including
    lazy BB, and eager BB when using bvminisat.
  * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
  -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
     1. It crashed with "Unimplemented"
     2. Right before that it prints out the (textual) DRAT proof.

* Remove 2 unneeded methods

* Missed a rename

* Typos

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments

* Reorder members of TBitblaster

LFSC LRAT Output (#2787)

* LFSC ouput & unit test

* Renamed lrat unit test file

* s/DRAT/LRAT/

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments

1. Extracted a filter whitespace function.
2. Added @param annotations.

* Addressing Yoni's comments

Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.

LratInstruction inheritance (#2784)

While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.

While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.

This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.

Fixed linking against drat2er, and use drat2er (#2785)

* Fixed linking against drat2er/drat-trim

We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.

Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.

I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.

* Combined the two libs, per Mathias

* drat2er configured gaurds

New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)

New C++ API: Get rid of mkConst functions (simplify API). (#2783)

Do not rewrite 1-constructor sygus testers to true (#2780)

[BV Proofs] Option for proof format (#2777)

We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!

My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`

and that I could not provide random other option values.

Clause proof printing (#2779)

* Print LFSC proofs of CNF formulas

* Unit Test for clause printing

* Added SAT input proof printing unit test

* Fixed cnf_holds reference. Proofs of CMap_holds

There were references to clauses_hold, which should have been references
to cnf_holds.

Also added a function for printing a value of type CMap_holds, and a
test for this function.

LFSC drat output (#2776)

* LFSC drat output

* Addressed Mathias' review

Addressing Mathias' review with the following changes:
* Added a few blank lines
* Added a unit test for LRAT output as LFSC