cmake: Add library versioning for libcvc4.so.

cmake: Rebase with current master, add new tests/source files.

cmake: Add missing checks for cvc4autoconfig.h to ConfigureCVC4.cmake.

cmake: Use target specific includes for libcvc4.

Further, print definitions added with add_definitions(...).

cmake: Add missing dependency.

cmake: Add support for building static binaries/libraries.

cmake: Add options for specifying install directories for dependencies.

cmake: Add module finder for GLPK-cut-log.

cmake: Add module finder for ABC.

cmake: Compile Java tests and add to ctest if Java bindings are enabled.

cmake: Add SWIG support + Python and Java bindings.

cmake: Add dependencies for test targets and support for make coverage.

cmake: Various portfolio/default option fixes.

cmake: Enable parallel execution for test targets regress, units, systemtests.

cmake: Build unit tests only if -DENABLE_UNIT_TESTING=ON.

cmake: Added system tests and target make systemtests.

cmake: Added regression tests and target make regress.

cmake: Add portfolio support.

cmake: Add ASAN support.

cmake: Enable shared by default.

Further, force shared builds in case of unit tests.

cmake: Disable W-suggest-override for unit tests.

cmake: Add target units.

cmake: Removed obsolete CMakeLists file in test.

cmake: Add support for CxxTest.

cmake: Filter through and disable unused HAVE_* variables from autotools.

cmake: Do not set global output directories for binaries and libraries.

cmake: Fix some includes.

cmake: Added support for coverage and profiling.

cmake: Added 3-valued option handling (to enable detection of user-set options).

cmake: Add module finder for readline.

cmake: Generate token headers.

cmake: Added licensing options and warnings/errors.

cmake: Cleanup CMakeLists.txt files, remove SHARED.

cmake: Add build configurations.

cmake: Fixed compiler flag macros.

cmake: Add module finder for LFSC.

cmake: Add module finder for CaDiCaL.

cmake: Add module finder for CryptoMiniSat.

cmake: Add module finder for SymFPU.

cmake: Add module finder for CLN.

cmake: Add libsignatures for proofs.

cmake: Remove unused CMakeLists.txt

cmake: Generate cvc4autoconfig.h (options currently statically set).

cmake: Added missing dependency for src/util

cmake: Working build infrastructure.

TODO: cvc4autoconfig.h

cmake: Antlr parser generation done.

cmake: Generate trace and debug tags

cmake: .cpp generation done, .h generation not yet complete

cmake: Added initial build infrastructure.

Decision strategy: incorporate arrays. (#2495)

Add rewrites for str.contains + str.replace/substr (#2496)

Decision strategy: incorporate separation logic. (#2494)

Add two rewrites for string contains character (#2492)

 Refactor strings extended functions inferences (#2480)

This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type.

This is in preparation for working on solving equations and further inferences in this style.

New C++ API: Introduce new macro and exception for API checks. (#2486)

Fix issue with str.idof in evaluator (#2493)

Decision strategy: incorporate strings fmf. (#2485)

More aggressive caching of string skolems. (#2491)

Move and rename sygus solver classes (#2488)

fix assertion error (#2487)

Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)

Improvements and fixes for symmetry detection and breaking (#2459)

This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.

Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)

Decision strategy: incorporate cegis unif (#2482)

 Decision strategy: incorporate bounded integers (#2481)

Decision strategy: incorporate datatypes sygus solver. (#2479)

More aggressive skolem caching for strings, document and clean preprocessor (#2478)

Make strings model construction robust to lengths that are not propagated equal (#2444)

This fixes #2429.

This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value.  See explanation in comment.

We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms.  I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.

Regardless, the strings model construction should be robust to handle this case, which this PR does.

Follow redirects with cURL in contrib/get* scripts (#2471)

On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.

Remove broken dumping support from portfolio build (#2470)

Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:

- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.

This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously.  Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).

[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117

Remove unnecessary tracing from preprocessing (#2472)

With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.

Decision strategy: incorporate UF with cardinality constraints (#2476)

Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)

Refactor how assertions are added to decision engine (#2396)

Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.

Add Skolem cache for strings, refactor length registration (#2457)

This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).

It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.

Generalize CandidateRewriteDatabase to ExprMiner (#2340)

Fix #include for minisat headers in bvminisat. (#2463)

Uses information gain heuristic for building better solutions from DTs (#2451)

Simplify storing of transcendental function applications that occur in assertions (#2458)

 Decision strategy: incorporate CEGQI (#2460)

New C++ API: Try to fix (false positive) Coverity warnings. (#2454)

Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)

 Initial infrastructure for theory decision manager (#2447)

Fix for when strings process loop is disabled. (#2456)

Fixe compiler warning in line_buffer.cpp. (#2453)

Support model cores via option --produce-model-cores. (#2407)

This adds support for model cores, fixes #1233.

It includes some minor cleanup and additions to utility functions.

Avoid calling size() every iteration (#2450)

Fix global negate (#2449)

fix (#2446)

Set NodeManager to nullptr when  exporting vars (#2445)

PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.

Using a single condition enumerator in sygus-unif (#2440)

This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).

In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:

- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.

A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.

There is also small improvements for trace messages.

Refactor non-clausal simplify preprocessing pass. (#2425)

Squash implementation of counterexample-guided instantiation (#2423)

Add (str.replace (str.replace y w y) y z) rewrite (#2441)

Replace boost::integer_traits with std::numeric_limits. (#2439)

Further, remove redundant gmp.h include in options_handler.cpp.

Remove clock_gettime() replacement for macOS. (#2436)

Not needed anymore since macOS 10.12 introduced clock_gettime().

 Make isClosedEnumerable a member of TypeNode (#2434)

 Further simplify and fix initialization of ce guided instantiation (#2437)

Refactor and document quantifiers variable elimination and conditional splitting (#2424)

Minor improvements to interface for rep set. (#2435)