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)

 Refactor printing of parameterized operators in smt2 (#2609)

Improve reasoning about empty strings in rewriter (#2615)

 Fix partial operator elimination in sygus grammar normalization (#2620)

 Fix string ext inference for rewrites that introduce negation (#2618)

Fix default setting of CegisUnif options (#2605)

cmake: Use gcovr instead lcov for coverage report generation. (#2617)

Fix compiler warnings (#2602)

Synthesize rewrite rules from inputs (#2608)

Fix cegis so that evaluation unfolding is not interleaved. (#2614)

Optimize regular expression elimination (#2612)

Add length-based rewrites for (str.substr _ _ _) (#2610)

 Support for basic actively-generated enumerators (#2606)

Random: support URNG interface (#2595)

Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.

Allow multiple synthesis conjectures. (#2593)

Fix compiler warnings. (#2601)

BV instantiator: Factor out util functions. (#2604)

Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).

Asan reported errors for the corresponing unit test because of this.

 BV inverter: Factor out util functions. (#2603)

Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).

 Fix string register extended terms (#2597)

A regress2 benchmark was failing, due to a recent change in our strings rewriter.

The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.

The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.

This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.

Cmake: Fix ctest call for example/translator. (#2600)

example/translator expects an input file to translate but none was provided in the ctest call.
This caused the ctest call to hang and wait for input on stdin in some configurations (in
particular in the nightlies).

Address slow sygus regressions (#2598)

 Disable extended rewriter when applicable with var agnostic enumeration (#2594)

Fix unif trace (#2550)

 Fix cache for sygus post-condition inference (#2592)

Update default options for sygus (#2586)

Fix rewrite rule filtering. (#2591)

New C++ API: Add checks for Sorts. (#2519)

Infrastructure for string length entailments via approximations (#2514)

Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590)

With older versions of CMake, skipped tests are reported as failures,
which is undesirable. This commit changes the CMakeLists file to only
use the `SKIP_RETURN_CODE` property if a newer version of CMake is used.

Fix end constraint for regexp elimination (#2571)

Clean remaining references to getNextDecisionRequest and simplify (#2500)

Fix mem leak in sha1_collision example. (#2588)

Fix mem leak in sets_translate example. (#2589)

Simplify datatypes printing (#2573)

Fix compiler warnings. (#2585)

Fix regress (#2575)

Add actively generated sygus enumerators (#2552)

Make CegisUnif with condition independent robust to var agnostic (#2565)

Fix stale op list in sets (#2572)

Eliminate partial operators within lambdas during grammar normalization (#2570)

cmake: Display skipped tests as not run (#2567)

Currently, the run_regression.py script just returns 0 when we skip a
test due to a feature not supported by the current configuration.
Returning 0 marks those tests as passed. To make it more clear which
tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property
to the regression tests and changes the regression script to return 77
for skipped tests. The feature is supported since at least CMake 3.0 [0].
For backwards compatibility with autotools, returning 77 for skipped
tests is only active when `--cmake` is passed to the run_regression.py
script.

[0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html

Allow (_ to_fp ...) in strict parsing mode (#2566)

When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.

unit: Fix ASAN detection for GCC. (#2561)

Make registration of preprocessing passes explicit (#2564)

As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.

[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html

Fix documentation for `make regress`. (#2557)

cmake: Add examples to build-tests, add warning for disabling static build. (#2562)

Fix "catching polymorphic type by value" warnings (#2556)

When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.

cmake: Generate compile_commands.json on configure. (#2559)

cmake: Add build target build-tests to build all test dependencies. (#2558)

init scalar class members (coverity issues 1473720 and 1473721) (#2554)

Fix compiler warnings. (#2555)

 Fix dumping pre/post preprocessing passes (#2469)

This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.

Refactor preprocessing pass registration (#2468)

This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.

As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.

This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.

[0] https://llvm.org/docs/WritingAnLLVMPass.html

Add rewrite for solving stoi (#2532)

cmake: Ignore ctest exit code for coverage reports.

Stream concrete values for variable agnostic enumerators (#2526)

Rewrites for (= "" _) and (= (str.replace _) _) (#2546)

cmake: Only do Java tests when unit testing on (#2551)

Right now, we are adding the Java tests even when we are not building
unit tests. This commit changes the build system to only add the Java
tests when unit tests are enabled. There are two reasons for this
change:

- building a production version of CVC4 should not require JUnit
- it seems more intuitive (to me at least) to disable JUnit tests when
  unit tests are disabled

This change also simplifies building the Java bindings in our homebrew
formula.

cmake: Add CxxTest finder module to allow custom paths. (#2542)

Remove assertion. (#2549)

Infrastructure for using active enumerators in sygus modules (#2547)

Incorporate all unification enumerators into getTermList. (#2541)

Fix Taylor overapproximation for large exponentials (#2538)

 Fix homogeneous string constant rewrite (#2545)

Fix bug in getSymbols. (#2544)

cmake: Only print dumping warning if not disabled by user. (#2543)

Makes SyGuS parsing more robust in invariant problems (#2509)

cmake: Fix test target dependency issues. (#2540)

Enable quantified array regression. (#2539)

Symmetry breaking for variable agnostic enumerators (#2527)

cmake: New INSTALL.md for build and testing instructions. (#2536)