Make conjecture generator's uf term enumeration safer (#2172)

This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.

Make candidate rewrite match filtering handle polymorphic operators properly (#2236)

Currently, the discrimination tree index used for candidate rewrite rule filtering based on matching does not properly distinguish polymorphic operators, which leads to type errors. This makes the index handle them correctly.

Fixes #1923.

Improvements and tests for the API around separation logic (#2229)

- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
  obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
  to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use

Remove hasAssertions() method from eager BV solver. (#2239)

Fix option handler for lazy/bv-sat-solver combinations. (#2225)

Further, unifies all *limitHandler and *limitPerHandler to limitHandler.

Add support for incremental eager bit-blasting. (#1838)

Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.

Fix several spelling errors (#2231)

Storing a std::pair<Key,Data> on CDOhash_map.

Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing.

Require argument description for non-{bool,void} options. (#2228)

Not adding the argument description for non-{bool,void} options is now an error.

Further, adds missing argument descriptions.

Fix issues related to cxxtest in configure.ac (#2226)

Fixes #2188. There were two issues related to cxxtest in configure.ac:

- `AC_PATH_PROGS` was used wrong (the third argument is a value to
  assign to the first argument and cannot be used for arbitrary
  commands)
- The `test` command always executes both sides of an "and" (`-a`), so
  `basename` was called without arguments when `CXXTESTGEN` was empty

This commit fixes both issues.

Make Python a required CVC4 dependency. (#2227)

Python is required for generating the options code. The dependency is now
required. Now autoconf searches for a Python version >= 2.7 and sets the
corresponding environment variables. mkoptions.py is now called with $(PYTHON).

This fixes the broken competition and windows nightly builds.

Fix for candidate rewrite rule filtering. (#2220)

 Make check-synth robust for assertions that are not the synth conjecture (#2217)

Fix Node::hasFreeVar for function variables (#2216)

A Node has free variables if its operator has free variables.

Fix CryptoMiniSat config to allow system versions. (#2223)

New C++ API: Enable examples. (#2222)

Removing unused CDTrailHashmap. (#2221)

Disabling bvLazyRewriteExtf in the right place (#2214)

Changing CDInsertHashMap to store <const Key, const Data> pairs. This is in preparation for adding map utility functions. (#2209)

Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for deprecating CDTrailHashMap. (#2207)

Fix rewriter for lambda (#2211)

The rewriter for lambda is currently too aggressive, there are cases like:

lambda xy. x = y

that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:

lambda fv_1 fv_2. fv_1 = y

where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.

To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).

Some parts of the code were formatted as a result.

 Fix a few issues in the sygus sampler related to evaluation (#2215)

Avoid explicit dependency on Python 3 (#2195)

New C++ API: Third batch of commands (SMT-LIB). (#2212)

New C++ API: Second batch of commands (SMT-LIB). (#2201)

Changing ArithIteUtils to use CDInsertHashMap. (#2206)

 This is 1/3 PRs for deprecating CDTrailHashMap.

Removing support for CDHashMap::iterator's postfix increment. (#2208)

 Move reg exp rewrites from prerewrite to postrewrite (#2204)

Performing clang-format on the original change-set of #2194 (#2203)

Use CryptoMiniSat 5.6.3. (#2205)

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)