Floating point theory solver based on SymFPU (#1895)

* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.

* Enable the bit-vector theory when setting the logic, not in expandDefinition.

This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.

* Use symfpu to implement the literal floating-point objects.

* Add kinds for bit-blasted components.

* Print the new kinds.

* Typing rules for the new kinds.

* Constant folding for the component kinds.

* Add support for components to the theory solver.

* Add explicit equivalences between classification functions and equalities.

* Use symfpu to do symbolic conversions of floating-point operations.

* Implement conversions via (over-)approximation and refinement.

* Correct a copy and paste error in the generation of uninterpretted functions for conversions.

Add contrib/get-symfpu for downloading symfpu. (#1905)

Fix purification in SygusUnifRL (#1912)

Add regressions, change defaults. (#1911)

Flag to check invariance of entire values in sygus explain (#1908)

Small change for more sensible line breaking in the output of get-model. (#1910)

Remove obsolete unit test for ackermannization. (#1906)

With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.

Fix ackermannize preprocessing pass. (#1904)

Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.

Support multiple sets of command line args in regs (#1902)

This commit adds support for multiple sets of command line arguments for
regressions. Each use of a `COMMAND-LINE` directive is interpreted as a
separate set of command line arguments.

Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)

Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)

Sygus repair constants (#1812)

Static learn redundant operators in CegisUnif (#1899)

Add ITE to default Boolean sygus grammar (#1898)

Refactored BVAckermann preprocessing pass. (#1889)

Fix priority of decisions for cegis unif (#1897)

Piecing solutions together in CegisUnif (#1894)

Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)

Better option names for PBE (#1891)

Make symmetry-breaker-exp into a preprocessing pass (#1890)

Add the symmetry breaker module (#1847)

Refactor bv-abstraction preprocessing pass. (#1860)

Infrastructure for approximations in model output (#1884)

Support for str.<= and str.< (#1882)

Fix order of preprocessing pass registration. (#1887)

Classifying data in SygusUnifRL (#1886)

Infrastructure for CEGQI handled status  (#1873)

only lazy trie changes (#1885)

Add support for str.code (#1821)

Fix handling of TO_REAL in cvc printer (#1876)

Remove special case for record selector printing. (#1875)

Cegis unif register evaluation points (#1878)

Make --output-lang consistent with --lang (#1877)

Do not print tuples. (#1874)

Refactor bv-intro-pow2 preprocessing pass. (#1851)

Fix printing of multiple datatypes (#1872)

Move Lazy trie datastructure to its own file (#1871)

Preparation for further developing CegisUnif

Initialize cegis unif strategy (#1861)

Document datatypes sygus (#1818)

Sets subtypes (#1095)

Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.

Fix redundant internalPush calls. (#1865)

The SMT2 parser by default passes a true expression to the CheckSatCommand,
which results in checkSatisfiability (in SmtEngine) to always do an internal
push. As a consequence, the work of each check-sat was reset even though no
user level push/pop happened.

Fix warnings in proof code (#1850)

Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)

Option to interleave tangent plane inferences (#1833)

Link cegis unif with the enumeration manager (#1859)

Make CegisUnif default to Cegis when no unif used (#1836)

Fix cvc printer for nullary constructors (#1856)

Remove (dummy) SMT1 printer (#1854)

Support HORN logic string (#1849)

Initial support for string standard in smt lib 2.6 (#1848)

Cegis unif enumerator manager (#1837)

Improve tangent planes for transcendental functions (#1832)

Refactor real2int (#1813)

This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.

Remove dead code in bv-to-bool preprocessing pass (#1828)

Fixes Coverity issue 1468436. As Coverity correctly detects,
kind::BITVECTOR_XOR is dealt with in an if-statement before the switch
statement on kind. This is because kind::XOR is binary while
kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly
indicates).

Remove subsort symmetry breaking (#1807)

Fix 1156 (#1830)

Disable unsat-cores/proofs for slow regression (#1835)

Allow multiple functions in sygus unif approaches (#1831)

Make factoring inference more aggressive (#1825)

Refactor nonlinear check (#1814)

Improvements to simple transcendental function check model. (#1823)

Initial implementation of SygusUnifRL (#1829)

Make construct solution behavior specific to SygusIO (#1827)

Print function for equality status. (#1826)

Simplify tangent plane direction (#1824)

New module for synthesizing functions in a data-driven SyGuS approach (#1819)

Core improvements to extended rewriter (#1820)

Fix subgoal generation context (#1816)

Refactor array-proofs and uf-proofs (#1655)

This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.

Equality resolution in the extended rewriter (#1811)

Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)

Move candidate rewrite code to own file (#1804)

Add benchmark requiring subgoal generation with induction. Disable option. (#1806)

Remove nl solve subs option. (#1803)

Fix issue with multi-triggers that include variable triggers (#1810)

Draft smt comp 2018 for quantifiers and non-linear (#1808)

Improve sygus sampling for strings (#1802)

Remove unused cache.h (#1795)

Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)

Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.

 Reenable filtering based on ordering in sygus sampler (#1784)

Draft of casc j9 scripts (#1800)

Allow metadata lines in test files to have leading spaces (#1799)

Currently, lines like `;EXPECT: sat` instead of `; EXPECT: sat` cause problems. This PR fixes it.

Symmetry detection module (#1749)

Restrict test summary to first-level subfolders (#1797)

Adding config/tap-driver.sh to .gitignore  (#1792)

#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically.
The current PR prevents this file from being added to the untracked changes list when doing git status.

Refactor pbRewrites preprocessing pass (#1767)

This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.

Remove tap-driver.sh (#1791)

The autogen.sh script that we use causes the tap-driver.sh script to be
copied from automake installed on the system, so we do not have to
include it in our git repository. This also avoids ping-ponging between
different versions of the tap-driver script if different people have
different versions and commit them as part of their PRs.

Add timeout (option) to regression script (#1786)

This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.

Default timeout tested with regression level 2 on a debug build with
proofs.

Disable slow regression test (#1787)

Disable check proofs/unsat cores for two regs (#1785)

Disabling proof checking/unsat core checking for the two benchmarks in
question, reduces the time to run regressions significantly. After the
change, regression level 2 takes 7m30s to run on my machine and
regression level 1 takes just below 3m (16 threads). Individually, the
tests take over 7m each when checking proofs/unsat cores, so they add
significant overhead.

Make 256 the default cardinality for strings (#1783)

RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)

Skolemize candidate rewrite rule checks (#1777)

Make strings fmf apply to all but internally generated Skolems (#1780)

Fix type error with regexp (#1778)

Fix mk type const (#1776)

This was a new utility, only used so far by the extended rewriter in EqChain simplification.

Another fix for sygus rr stats. (#1768)

[Reg] Make status/unsat-core detection more robust (#1775)

This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.

Fix get-unsat-core detection in regression script (#1773)

Due to a typo in the regression script, the (get-unsat-core) command was
not recognized (the script was looking for (get-unsat-cores)), so it
tried to run a regression script containing (get-unsat-core) even when
CVC4 was compiled without proof support. This commit fixes the typo.

allowing --bool-to-bv without quantifiers (#1771)