Proposal for adding map utility functions to CVC4. (#2232)

* Proposal for adding map utility functions to CVC4.

Disable argument relevance for sygus by default (#2288)

Add debug test for sygus subcall verify calls. (#2287)

Move uf model code from uf to quantifiers (#2095)

Do beta-reduction in expandDefinitions (#2286)

Require Swig 3 (#2283)

Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h

Simplify and improve the sygus parser (#2266)

Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304

This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.

As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.

It also removes some unnecessary code for converting builtin kinds to their total versions.

This is work towards #2197.  We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.

Document/refactor datatypes sygus simple symmetry breaking (#2233)

 Fix simple reg exp consume rewrite (#2281)

Delete functions instead of using CVC4_UNDEFINED (#1794)

C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.

 Wait to do sygus qe preprocess until full effort check  (#2282)

Fix inference of pre and post conditions for non variable arguments. (#2237)

Make output of flushInformation and safeFlushInformation consistent. (#2280)

Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273)

Make flat form inferences optional in strings (#2277)

Add RegLan to smt2/sygus parsers. (#2276)

 Move sygus quantifier elimination step for non-ground-single-invocation to sygus (#2269)

Remove support for Enum sygus syntax. (#2264)

Fixes for sygus inference (#2238)

This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize

 Fixes and improvements for single invocation inference (#2261)

Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)

 Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)

Add rewrite for BITVECTOR_ITE with const children. (#2271)

Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)

Eliminate option for sygus UF evaluation functions (#2262)

Fix printing statistics in case of signals. (#2267)

 Add timer for BV inequality solver. (#2265)

Parse standard separation logic inputs (#2257)

Improve CEGQI heuristics involving equality and multiple instantiations (#2254)

Fix candidate rewrite utilities for non-first-class types (#2256)

Make strings robust to regular expression variables. (#2255)

The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one.

However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.).  This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases.

It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed).

This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers.

Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child. (#2259)

 Remove references to deprecated propagate as decision feature (#2258)

Remove Subversion build info (#2250)

Fix API call for reg exp. (#2248)

Improvements and fixes in cegqi arithmetic (#2247)

This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.

It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.

This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.

Remove outdated references to TLS (#2245)

Fix issues with printing parametric datatypes in smt2 (#2213)

Fix wrong evaluation of STRING_STOI (#2252)

Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)

 InteractiveShell: Remove redundant options argument. (#2244)

New C++ API: Fixed ownership of options object. (#2243)

Fix issues with bv2nat (#2219)

This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.

 Fix assertion in conjecture generator (#2246)

Makes minor improvements and removes the need to have the assertion (which was incorrect).

This fixes the nightlies.

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)