Fixes for quantifiers + incremental (#2009)

[SMT-COMP] Print non-(un)sat output to stderr (#2019)

In the SMT-COMP runscript, we are currently discarding output on stdout
that is not "sat" or "unsat" when using `trywith` (this is not the case
with `finishwith`). Due to this, our tests might miss cases where CVC4
fails and prints an error on stdout when using `trywith`. This commit
changes the script to print output other than "sat" or "unsat" to
stderr.

Normalize negated bit-vector terms over equalities. (#2017)

Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)

Draft run script for strings smt comp 2018. (#2016)

 Make user's SMT2 version override file version (#2004)

Disable minisat elimination when nonlinear is enabled (#2006)

Track input language in a single place (#2003)

Builtin evaluation functions for sygus (#1991)

Fix cegqi assertions for quantified non-linear cases. (#1999)

Fix no-cbqi-innermost option name in run script (#1994)

Update SymFPU. (#1992)

Reenable repair const (#1983)

MiniSat: Be more careful about running proof code (#1982)

In `addClause_()`, we were checking the condition `ca[confl].size() ==
1` regardless if proofs were enabled or not, even though both branches
of the if statement only do something when proofs are enabled. This lead
to issue #1978 occurring even when not generating proofs. Note: This
commit is *not* a fix for #1978 but it makes sure that the issue does
not occur when not generating proofs/unsat cores.

Add QF_BV configuration for SMTCOMP'18. (#1981)

Fix various nl assertions. (#1980)

Fix (#1979)

Improve simple constant symmetry breaking for sygus (#1977)

Fix compiler warnings (#1959)

Fix (#1975)

Fixes for non-linear check model (#1974)

Fix nl regression for unsat cores. (#1973)

Remove spurious assertion in nonlinear extension (#1972)

Towards better symbolic enumeration in SyGuS (#1971)

Add notions of evaluated kinds in TheoryModel (#1947)

Remove ProofProxy (#1965)

Generalize check-model in NonLinearExtension for quadratic equations (#1892)

Set same options for proofs as for unsat cores (#1957)

In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.

Repair constants using symbolic constructors (#1960)

Parse error for sygus grammar term with multiple let bodies (#1961)

Disable symmetry breaker for unsat cores (#1958)

Currently, --check-unsat-cores fails for one of our regressions. It
turns out that the issue is due to preprocessing done by the symmetry
breaker.  The symmetry breaker does not add dependencies and thus the
generated unsat core is incomplete/wrong. This commit disables the
symmetry breaker when we are generating unsat cores (it was previously
only disabled when generating proofs). Fixes issue #1953.

Make sygus infer find function definitions (#1951)

Infrastructure for strings strategies (#1883)

Add SymFPU licensing information. (#1952)

Improvements in parsing and printing related to mixed int/real (#1879)

This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary.  This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).

Infrastructure to mark unused sygus strategies  (#1950)

Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)

Refactor sygus eval unfold (#1946)

Remove Eclipse project files (#1928)

No one of the core devs is currently using Eclipse, so the Eclipse
project files are essentially useless since they are not guaranteed to
be up-to-date.

Fix compiler warning in hashsmt example (#1927)

Previously, we were using delete for an array allocated on the heap,
which caused a warning. @dddejan fixed this and other issues in PR #1909
but after @ajreynol fixed the other issues in a separate PR and to not
waste @dddejan's time, I am submitting this fix separately (note: the
fix is slightly different in that it changes the array to a vector,
making a delete[] unnecessary).

Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)

Fix file extension (#1919)

* Fix file extension

* Update Makefile

changing default (#1944)

Cache isInterpretedFinite (#1943)

Cegis unif defaults to cegis when no unif (#1942)

Unified fairness scheme for cegis unif (#1941)

Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937)

Fix debugPrint and add regress. (#1934)

Option to force return values of Bool functions to be constant in CegisUnif (#1930)

Cegis-specific infrastructure (#1933)

Internal propagation for refinement lemmas (#1932)

Improve the separation resolution scheme in cegis unif (#1931)

Refactor static learning preprocessing pass (#1857)

Refactoring get enumerator values in construct candidate for cegis unif (#1926)

adding regressions (#1925)

Building and refining solutions with dynamic condition generation in CegisUnif (#1920)

Fix free variables in cbqi preregister inst. (#1921)

Fix annotations in regress2. (#1917)

Minor improvements to --nl-ext-purify (#1896)

 Incorporating dynamic condition enumeration into cegis unif (#1916)

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.