Strings: Make EXTF_d inference more conservative (#2740)

Arith Constraint Proof Loggin (#2732)

* Arith Constraint Proof Logging

Also a tiny documentation update.

* Debug.isOn check around iterated output

* reference iteratees

Enable BV proofs when using an eager bitblaster (#2733)

* Enable BV proofs when using and eager bitblaster

Specifically:
   * Removed assertions that blocked them.
   * Made sure that only bitvectors were stored in the BV const let-map
   * Prevented true/false from being bit-blasted by the eager bitblaster

Also:
   * uncommented "no-check-proofs" from relevant tests

* Option handler logic for BV proofs

BV eager proofs only work when minisat is the sat solver being used by
the BV theory.

Added logic to the --proof hanlder to  verify this or throw an option
exception.

* Bugfix for proof options handler

I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.

* Clang-format

Fix use-after-free due to destruction order (#2739)

A test for PR #2737 was failing even though the PR only added dead code.
This PR fixes the issue by fixing two use-after-free bugs:

- `ResolutionBitVectorProof` has a `Context` and a
`std::unique_ptr<BVSatProof>` member. The `BVSatProof` depends on the
`Context` and tries to access it (indirectly) in its constructor but
because the context was declared after the proof, the context was
destroyed before the proof, leading to a use-after-free in a method
called from the proof's destructor. This commit reorders the two
members.
- `TLazyBitblaster` was destroyed before the `LFSCCnfProof` in
`BitVectorProof` because `SmtEngine`'s destructor first destroyed the
theory engine and then the proof manager. This lead to a use-after-free
because `LFSCCnfProof` was using the `d_nullContext` of
`TLazyBitblaster`, which got indirectly accessed in `LFSCCnfProof`'s
destructor. This commit moves the destruction of `ProofManager` above
the destruction of the theory engine.

The issues were likely introduced by #2599. They went undetected because
our nightlies' ASAN check does not use proofs due to known memory leaks
in the proof module of CVC4.

I have tested this PR up to regression level 2 with ASAN with leak
detection disabled.

 Take into account minimality and types for cached PBE solutions (#2738)

Apply extended rewriting on PBE static symmetry breaking. (#2735)

Enable regular expression elimination by default. (#2736)

Seems to have no impact on Norn, and is helpful for a number of applications.

 Skip non-cardinality types in sets min card inference (#2734)

Bit vector proof superclass (#2599)

* Split BitvectorProof into a sub/superclass

The superclass contains general printing knowledge.

The subclass contains CNF or Resolution-specific knowledge.

* Renames & code moves

* Nits cleaned in prep for PR

* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof

Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.

* Unique pointers, comments, and code movement.

Adjusted the distribution of code between BVP and RBVP.
  Notably, put the CNF proof in BVP because it isn't
  resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
  BVP's pointer to a CNF proof
  RBVP's pointer to a resolution proof

BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`

* clang-format

* Undo manual copyright modification

* s/superclass/base class/

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public

* Andres's Comments

Mostly cleaning up (or trying to clean up) includes.

* Cleaned up one header cycle

However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.

* Added single _s to header gaurds

* Fix Class name in debug output

Credits to Andres

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original  ordering

Optimizations for PBE strings (#2728)

 Infrastructure for sygus side conditions (#2729)

Combine sygus stream with PBE (#2726)

Improve interface for sygus grammar cons (#2727)

Information gain heuristic for PBE (#2719)

Optimize re-elim for re.allchar components (#2725)

Improve skolem caching by normalizing skolem args (#2723)

In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.

Generalize sygus stream solution filtering to logical strength (#2697)

Improve cegqi engine trace. (#2714)

Make (T)NodeTrie a general utility (#2489)

This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.

Fix coverity warnings in datatypes (#2553)

This caches some information regarding tester applications and changes int -> size_t in a few places.

Lazy model construction in TheoryEngine (#2633)

Reduce lookahead when parsing string literals (#2721)

LRA proof signature fixes and a first proof for linear polynomials (#2713)

* LRA proof signature fixes and a first proof

The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.

* Add dependency info to signatures

I chose to indicate shallow dependencies only.

Use https for antlr3.org downloads (#2701)

This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.

Move ss-combine rewrite to extended rewriter (#2703)

We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.

Add rewrite for (str.substr s x y) --> "" (#2695)

This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.

Cache evaluations for PBE (#2699)

Quickly recognize when PBE conjectures are infeasible (#2718)

Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.

This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.

After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.

Obvious rewrites to floating-point < and <=. (#2706)

Support string replace all (#2704)

 Fix type enumerator for FP (#2717)

Fix real2int regression. (#2716)

Change lemma proof step storage & iterators (#2712)

Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.

Also added an iterator for the proof steps, and << implementations

 Clausify context-dependent simplifications in ext theory (#2711)

Fix E-matching for case where candidate generator is not properly initialized (#2708)

 Expand definitions prior to model core computation (#2707)

cmake: Require boost 1.50.0 for examples. (#2710)

cmake: Add option to explicitely enable/disable static binaries. (#2698)

Evaluator: add support for str.code (#2696)

Adding default SyGuS grammar construction for arrays (#2685)

Fix collectEmptyEqs in string rewriter (#2692)

 Fix for itos reduction (#2691)

Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)

Change default sygus enumeration mode to auto (#2689)

Fix coverity warnings in sygus enumerator (#2687)

New C++ API: Split unit tests. (#2688)

Increasing coverage (#2683)

This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.

API: Fix assignment operators (#2680)

The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.

Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.

configure.sh: Fix option parsing to match --help (#2611)

Allow partial models with optimized sygus enumeration (#2682)

 Implement option to turn off symmetry breaking for basic enumerators (#2686)

Improves the existing implementation for sygus-active-gen=basic.

Refactor default grammars construction (#2681)

fixes to regression docs (#2679)

Add optimized sygus enumeration (#2677)

Record assumption info in AssertionPipeline (#2678)

Minor improvement to sygus trace (#2675)

CMake: Set RPATH on installed binary (#2671)

Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.

Do not use lazy trie for sygus-rr-verify (#2668)

Fail for SWIG 3.0.8 (#2656)

Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588

Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.

CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)

Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.

[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36

Only build CryptoMiniSat library, no binary (#2657)

This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.

Recover from wrong use of get-info :reason-unknown (#2667)

Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.

Remove antlr_undefines.h. (#2664)

Is not required anymore since we don't use autotools anymore.

Add substr, contains and equality rewrites (#2665)

Disable dumping test for non-dumping builds (#2662)

Travis: run examples and avoid building them twice (#2663)

`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.

BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)

Simplifications based on the special const is now delegated down, only
the concat is pulled up.

BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const. (#2647)

Sygus streaming non-implied predicates (#2660)

Remove autotools build system. (#2639)

Fix util::Random for macOS builds (#2655)

Add helper to detect length one string terms (#2654)

This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.

This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.

Add OptionException handling during initialization (#2466)

The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:

1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes

This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor).  Finally,
the commit adds a simple regression test for invalid dump tags.

cmake: Run regression level 2 for make check. (#2645)

Non-implied mode for model cores (#2653)

Non-contributing find replace rewrite (#2652)

Improve reduction for str.to.int (#2636)

Introducing internal commands for SyGuS commands (#2627)

Constant length regular expression elimination (#2646)

 Skip sygus-rr-synth-check regressions when ASAN on (#2651)

This commit disables three regressions when using an ASAN build. The
regressions are all leaking memory when invoking the subsolver (see
issue #2649). Debugging the issue will take a while but is not very
critical since this feature is currently only used by CVC4 developers
but it prevents our nightly builds from going through.

Show if ASAN build in --show-config (#2650)

This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.

In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.

Sygus query generator (#2465)

 Fix context-dependent for positive contains reduction (#2644)

BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)

Match:       `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`

Match:       `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`

Match:       `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`

On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
          | CVC4-base                              | CVC4-concatpullup-or                     |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38992 13844  25148  1082  28  984887.4 | 39028 13845  25183  1046 28  974819.1 |
```

cmake: Add CxxTest include directory to unit test includes. (#2642)

BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones (#2596).

BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).

BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0 (#2596).

BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).

Improve strings reductions including skolem caching for contains (#2641)

Improve reduction for int.to.str (#2629)

Option for shuffling condition pool in CegisUnif (#2587)

cmake: Generate git_versioninfo.cpp on build time. (#2640)

Delay initialization of theory engine (#2621)

This implements solution number 2 for issue #2613.

Add more (str.replace x y z) rewrites (#2628)

Fix fp-bool.sy grammar and require symfpu (#2631)

Reset input language for ExprMiner subsolver (#2624)

Improvements to rewrite rules from inputs (#2625)

 Add rewrites for str.replace in str.contains  (#2623)

This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.

 Fix heuristic for string length approximation (#2622)