Improvements to sets + cardinality + quantifiers (#2200)

Adding API access methods to get heap/nil expressions when using separation logic (#2194)

 New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)

 Improve rewriter for regular expression concatenation (#2196)

Generalize symmetry detection for 1 symmetry variable mapped to n input variables  (#1888)

New C++ API: Implementation of Solver class: OpTerm handling. (#2164)

New C++ API: declare-datatype. (#2166)

 sygusComp2018: add regressions (#2191)

Fix warning in sygus PBE (#2190)

 sygusComp2018: Improvements to CEGIS loop (#2187)

Optimizations and fixes for computing whether a type is finite (#2179)

 sygusComp2018: refactor and improve sygus io utility (#2185)

Remove --no-check-proofs and --no-check-unsat-cores from a satisfiable test (#2184)

Cleanup and additions for candidate generator (#2173)

 sygusComp2018: minor changes to repair constant utility (#2110)

 sygusComp2018: pbe multi-enumerator fairness option (#2178)

Refactor sep-pre-skolem-emp preprocessing pass

Minor cleanup and fixes for conflict-based instantiation (#2123)

Do extended rewrite on results of quantifier elimination. (#2119)

 Purify applications of exp to transcendental arguments (#2097)

 sygusComp2018: update policies for solution reconstruction (#2109)

sygusComp2018: Improvements to datatypes sygus solver (#2177)

sygusComp 2018: updates to sygus term database (#2170)

Avoid ambiguous overloads in BitVector (#2169)

`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring

exportTo only if needed for --sygus-rr-synth-check (#2168)

sygusComp2018: update semantics for declare-fun in sygus. (#2102)

Fix and improve grammar normalization for any constant. (#2101)

Properly clean up assertion stack in CnfProof (#2147)

Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.

 sygusComp2018: optimization for collect model info (#2105)

New C++ API: Minor reorder. (#2163)

New C++ API: Implementation of datatype classes. (#2142)

New C++ API: Implementation of Solver class: Consts handling. (#2145)

Move rewrite to pass (#2128)

Add more sophisticated floating-point sampler (#2155)

This commit adds a floating-point sampler inspired by PyMPF [0]. It also
creates a new Sampler class that can be used for creating random values
of different sorts (currently BV and FP values).

[0] https://github.com/florianschanda/PyMPF

 sygusComp2018: improve extended rewriter for Bool (#2107)

Split ext theory to own file and document (#1809)

Feature/fp rewrite improvement (#2154)

New C++ API: Implementation of Solver class: Term handling. (#2144)

New C++ API: Implementation of Solver class: Sort handling. (#2143)

Add option for timeout for rewrite candidate check (#2156)

sygusComp2018: simplify beta reduction in uf rewriter. (#2106)

This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2).

I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.

 Make string length lemmas more robust to rewriting (#2150)

Minor changes to sygus-rr utilities to support floating point rewrites (#2148)

sygusComp2018: Improve string rewriter (#2141)

More cleanup in strings (#2138)

New C++ API: Implementation of datatype declaration classes. (#2136)

Reorganize candidate rewrite rule filtering (#2116)

Remove unused CDVector (#2139)

New C++ API: Implementation of OpTerm. (#2132)

Fix fmf-fun for non-equality function definitions (#2134)

Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.

New C++ API: Implementation of Term. (#2131)

New C++ API: Implementation of Kind maps. (#2130)

Fix datatypes example: nil constructor was missing. (#2135)

sygusComp2018: update sygus-related options setting in smt engine (#2108)

Remove miscellaneous dead and unused code from quantifiers (#2121)

Add regression test for issue #1986 (#2114)

The issue is not triggered anymore after PR #2059 but the test case is
good to have for changes in MiniSat code.

Refactor ApplySubsts preprocessing pass. (#2120)

New C++ API: Implementation of Sort. (#2122)

Remove some dead code from theory strings (#2125)

Add missing include (#2127)

Modify cegqi heuristic for finite datatypes  (#2126)

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)