cmake: Disable unit tests if assertions are not enabled.

cmake: FindANTLR: Check if antlr3FileStreamNew is available.

cmake: configure.sh wrapper: Fixes for sh.

travis: Switch to cmake.

cmake: Do not build examples and unit and system tests by default.

cmake: configure.sh wrapper: Add --name option.

cmake: examples: Configure output directory per target.

cmake: Added java examples

cmake: configure.sh wrapper: Add --prefix for install directory.

cmake: Add some more documentation, cleanup.

cmake: Move helper functions to cmake/Helpers.cmake.

cmake: Added target examples (currently .cpp examples only)

cmake: Simplify build type configuration.

cmake: Refactor and clean up build profile printing.

cmake: Added target check

Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.

cmake: Add make install rule.

cmake: configure.sh wrapper: Fix handling of options with arguments.

cmake: Add module finder for Valgrind.

cmake: Various CMakeLists.txt fixes/cleanup.

cmake: Only build libcvc4 and libcvc4parser as libraries.

The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular  dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.

cmake: Move find_package to where it is actually needed.

cmake: configure.sh wrapper: Removed env vars help text.

cmake: configure.sh wrapper: Configurable build directory

cmake: configure.sh wrapper: Create build dirs for configurations

cmake: configure.sh wrapper: done (except: configurable build dir)

cmake: Updated and prettified configuration printing.

cmake: configure.sh wrapper: option parsing

cmake: Add ENABLE_DEBUG_CONTEXT_MM to enable the debug context memory manager.

cmake: Add ENABLE_BEST to enable best configuration of dependencies.

cmake: Add Java runtime as required dependency (required for ANTLR).

cmake: Add convenience wrappers for tag generation.

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.