Improve error message. (#2124)

Use evaluator in sygus sampler. (#2117)

* Use evaluator for sygus sampler.

* Format

New C++ API: Implementation of Result. (#2112)

Remove comment about model value hack (#2118)

This fixes #821.

For some background, some special cases were added to equality engine and theory engine a few years ago to handle constants properly. As a result of these changes, a comment in the code was added about a HACK for getModelValue, but the code is completely reasonable looking to me (it says that the model value of a constant is itself). This PR removes that comment.

From what I can tell issue #821 can be closed.

 sygusComp2018: optimization for invariance test (#2104)

Fix stale reference in MiniSat when generating UC (#2113)

In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.

Do not rename uninterpreted constants (#2098)

Split and document ceg theory instantiators (#2094)

Header for new C++ API. (#1697)

Synthesize candidate-rewrites from standard inputs (#1918)

sygusComp2018: add scripts. (#2103)

sygusComp2018: Add evaluator (#2090)

This commit adds the Evaluator class that can be used to quickly
evaluate terms under a given substitution without going through the
rewriter. This has been shown to lead to significant performance
improvements on SyGuS PBE problems with a large number of inputs because
candidate solutions are evaluated on those inputs. With this commit, the
evaluator only gets called from the SyGuS solver but there are
potentially other places in the code that could profit from it.

Add casc j9 tfn script (#2100)

 Disable uf symmetry breaker in incremental mode (#2091)

Fix assertion for relational triggers (#2096)

 Do not dagify printing over binders (#2093)

Remove unnecessary code in register quantifier internal (#2092)

Minor improvements in SMT2 and CVC printers (#2089)

This commit adds support for string concatenation, charat, and length
operators in the CVC printer and support for re.nostr, re.allchar, and
insert into a set in the SMT2 printer.

Bump library version to 1.7-prerelease.

Cutting release 1.6.

More updates to NEWS for 1.6.

Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.

Bump library version.

Update copyright year in configuration.cpp:copyright().

Updated copyright headers.

Do not use git blame -C in get-authors (too many false positives).

Fix update-copyright script for files without a header.

Added Makai and Yoni to get-authors script.

Remove parentheses for prefix ops without args (#2082)

In the CVC printer, function definitions without arguments are printed
like constants but when actually using that function we were printing in
the form of `x()`.

For example:

```
(set-logic QF_BV)
(define-fun x1480 () Bool true)
(define-fun x2859 () Bool true)
(define-fun x2387 () Bool x2859)
(check-sat)
```

Was dumped as:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```

This commit removes these parentheses when prefix functions with zero arguments
are printed, so the example above becomes:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```

Fix warnings and enable -Wnon-virtual-dtor warning (#2079)

This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.

Check unsat cores in regressions also without LFSC (#1955)

When moving the LFSC checker out of the CVC4 repository in commit
dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0, we disabled checking unsat
cores when CVC4 was compiled without LFSC due to the complexity of the
regression script. This commit changes the new(-ish) Python regression
script to check unsat cores even when CVC4 was compiled without LFSC.
This is done by having two separate flags, --with-lfsc and
--enable-proof, for the regression script that mirror the configuration
flags. The regression script performs unsat cores and proofs checks
based on those flags.

Additionally, this commit changes the regression script to check proofs
and unsat cores in two independent runs. Testing them in a single run
masked issues #1953 and #1954.

Updated installation instructions to mention autogen.sh (#1477)

Resolve CVC4_USE_SYMFPU in headers at config-time (#2077)

As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions
in floatingpoint.h, which was problematic when installing the header
files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and
simply including the header files in another project would be missing
that definition. This commit moves floatingpoint.h to a template file
floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at
configure-time when generating floatingpoint.h (this is the same
solution that integer.h and rational.h use). I have tested the fix with
the examples provided in #2013 and they work.

Disable solving non-linear BV literals by default (#2070)

Workaround for incremental unsat cores (#1962)

This commit implements a workaround for computing unsat cores while
doing incremental solving to address #1349. Currently, our resolution
proofs do not handle clauses with a lower-than-assertion-level correctly
because the resolution proofs for them get removed when popping the
context but the SAT solver keeps using them. The workaround changes the
behavior of the SAT solver to add clauses always at the current level if
incremental solving and unsat cores are enabled. This makes sure that
all learned clauses are removed when we pop below the level that they
were learned at. This may degrade performance because the SAT solver has
to relearn clauses.

Fix simple regexp consume (#2066)

Disable unconstrainedSimp pass when proofs enabled (#1976)

Currently, we may end up enabling the unconstrainedSimp pass when proofs
are enabled because the check that this pass is disabled happens before
a check for automatically enabling it. This lead to issues when running
for example on regress0/aufbv/bug00.smt with --check-proofs. This commit
moves the code for automatically enabling the pass to only be run if
proofs and unsat cores are disabled. Note: This commit is mostly a
simple code move but formatting in setDefaults was a bit off, so there
are a lot of formatting changes.

Fix strip constant endpoint for ITOS in strings rewriter (#2067)

Fix equality conflicts reported by FP (#2064)

Disable test that fails in competition mode (#2063)

Commit 106e764a04e4099cc36d13de9cec47cbf717b6cc missed one test case.
This commit disables that test case for the competition build.

Add flag to skip regression if feature enabled (#2062)

This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.

Reset decisions at SAT level after solving (#2059)

Some quick background: CVC4 has two primary contexts: the assertion
context (which corresponds to the push/pops issued by the user) and the
decision/SAT context (which corresponds to the push/pops done by the
user and each decision made by MiniSat.

Before 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77, we had an additonal
push/pop when doing the actual solving. With these removed, it could
happen that we get a wrong result when doing incremental solving:

```
...
; check-sat call returns sat, the decision level in the SAT solver is
; non-zero at this point
(check-sat)
; Solver::addClause_() determines that we cannot add the clause to the
; SAT solver directly because the decision level is non-zero (i.e. the
; clause is treated like a theory lemma), thus it is added to the lemmas
; list.
(assert false)
; The solver stores some information about the current state, including
; the value of the "ok" flag in Solver, which indicates whether the
; current constraints are unsatisfiable. Note that "ok" is true at this
; point.
(push)
; Now, in Solver::updateLemmas(), we add clauses from the lemmas list.
; The problem is that empty clauses (which "false" is after removing "false"
; literals) and unit clauses are not added like normal clauses. Instead,
; the empty clause, essentially just results in the "ok" flag being set to
; false (unit clauses are added to the decision trail).
(check-sat)
; Here, the solver restores the information stored during
; (push), including the "ok" flag, which is now true again.
(pop)
; At this point, the solver has "forgotten" about (assert false) since
; the "ok" flag is back to true and it answers sat.
(check-sat)
```

There are multiple ways to look at the problem and to fix it:

- One could argue that an input assertion should always be added
directly to the clauses in the SAT solver, i.e. the solver should
always be at decision level 0 when we are adding input clauses. The
advantage of this is that it is relatively easy to implement,
corresponds to what the original MiniSat code does (it calls
Solver::cancelUntil(0) after solving), and is no worse than what we had
before commit 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (push/pop do a
strict superset of what resetting the decision at the current assertion
level does). The disadvantage is that we might throw away some useful work.

- One could argue that is fine that (assert false) is treated like a
theory lemma. The advantage being that it might result in more efficient
solving and the disadvantage being that it is much trickier to
implement.

Unfortunately, it is not quite clear from the code what the original
intention was but we decided to implement the first solution. This
commit exposes a method in MiniSat to reset the decisions at the current
assertion level. We call this method from SmtEngine after solving.
Resetting the decisions directly after solving while we are still in
MiniSat does not work because it causes issues with datastructures in
the SMT solver that use the decision context (e.g.
TheoryEngine::d_incomplete seems to be reset too early, resulting in us
answering sat instead of unknown).

Disable BV-abstraction in the competition script. (#2061)

Look for cryptominisat5_simple, not cryptominisat5 (#2058)

If the boost program_options library is missing, CryptoMiniSat5 only
builds a cryptominisat5_simple binary and omits the cryptominisat5,
which has more command-line options. We do not use the binary anyway, so
this commit changes the cryptominisat.m4 script to look for the
cryptominisat5_simple binary, which is always generated.

Remove invalid assertion (#1993). (#2057)

Clear pending inferences during datatypes splitting (#2056)

Only enable transcendentals if logic is N[I]RAT (#2052)

Move assertion. (#2051)

[SMT-COMP] Add new logics to run-scripts (#2022)

Enable cegqi (with model values) for floating point by default (#2023)

Regressions: Support for requiring CVC4 features (#2044)

This commit adds supprt for the `REQUIRES` directive in our regression
benchmarks. This directive can be used to enable certain benchmarks only
if CVC4 has been configured with certain features enabled.

 Fix assertion involving unassigned Boolean eqc in model (#2050)

Fix corner case of mixed int/real cegqi. (#2046)

Fix BV-abstraction check to consider SKOLEM. (#2042)

Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.

Fix preinitialization pass for finite model finding (#2047)

Fix quantified bv variable elimination (#2039)

Fix quantifiers conflict lemma handling (#2043)

Apply preprocessing to counterexample lemmas in CEGQI  (#2027)

 Use monomial sum utility to solve for quantifiers macros (#2038)

Reduce before preregister. (#2025)

Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)

Ignore license key in set-info command. (#2021)

Fix for issue #2002 (#2012)

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)