Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences.

Temporary reverting commit 477e72b (proofs as default build) until we fix nightly builds.

Minor improvements to strings. Refactor rewriter. Enable fairness for multiple sorts in UF finite model finding by default.

Default builds are now proof enabled.

Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648)

Minor improvements, add endpoint eq inference to strings.

More improvements to strings rewriter for regexps, contains, indexof, replace and others.  Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.

Fixes related to explanations for cycles, sym inferences. Minor fixes and improvements.

Improvements to rewriter for regexp, contains, indexof. Improvements and fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.

Evaluate extended operators on partially concrete arguments. More aggressive rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms.

More improvements to strings. More aggressive inference of constant eqc, reductions based on congruence, precheck for cycles.

Refactor strings, bug fix inferences vs lemmas.

Fix for fmf+incremental. Restrict cbqi to literals from ce body.  Add regressions.

Improve quantifiers engine wrt incremental presolve. Add regressions.

Minor fix

Minor fixes to strings, add regressions.

Add missing regression

Fix bug for trivial extf inferences in strings. Improve caching for splits in strings. Other improvements.

Improved handling of extended operators.  Do preprocess on memberships eagerly, only process contains/memberships that have non-constant arguments.  Cleanup.

Lazy preprocessing of extended operators in strings.  Add regressions. Fixes bug 613.

Better organization of quantifiers modules, promote full saturation to module. Add heuristics for cbqi LIA instantiation with coefficients.

Clear term caches for quantifiers + incremental, fixes bug 674.  Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.

Counterexample-guided instantiation for datatypes.  Make sygus parsing more liberal.

Improve ITE redundant branch elimination in quantifiers.

Fix for sets segfault (reported by Ravi Kandhadai)

fix involves sets getModelValue handling the case when element theory
doesn't have model

Fix bug in quantifiers engine where model construction could be skipped.

More work mixing UF and sygus.

Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quantified formulas with non-constant polarity.

Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.

Fix bug related to quantifiers + incremental, thanks John Backes for the bug report.  Other minor cleanup.

Minor cleanup related to codatatypes.

Models for codatatypes. Fixes bug 662.

Normalization of codatatype constants, codatatype now has a fair enumerator.

Fix bug 670.  Minor.

Fix bug in strings rewriter regarding lengths of substr terms.

Working towards a fair enumerator for codatatypes.

Improve quantifiers rewriter, minor refactoring.

Working fix for bugs 610 and 643 regarding check-model with preprocessed quantified formulas.

Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.

Fix bugs 605 and 667.

fix regressions

Merge remote-tracking branch 'origin/master'

Fixed but with getAssertions

Minor improvement to sygus sol reconstruction.

Improvements to sygus, register equivalent terms based on rewrites of original conjecture, set default invariant template mode to post-condition.

Do ITE term bookkeeping when solving Sygus inputs.  Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.

Modify slow regressions.

Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds.  Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.

Use zero in cbqi when not using infinities.

Added threshold for core bv cardinality lemmas

Fix for bv core cardinality lemma generation

eager bit-blasting gives models for boolean variables too (fixes bug618)

Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.

Minor changes related to codatatypes for 1.5 release.

Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi.  Enable redundant ITE branch elimination in quantifiers rewriter.

better handling for conflicting options with nonlinear arith (bug 646)

Fix bug 649 (errors to regular output channel)

From SMTLIB standard:

  "Regular output, including error messages, is printed on the
   regular output channel..."

For CVC language, the behavior is unchanged (i.e. errors go
to stderr by default).

fix to bug659 due to algebraic solver model building

fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero

Make cbqi robust to term ITE removal.  Separate vts infinities for int/real.

fix bug 605

Implementation of model-based projection in cbqi, cleanup, add regressions.

fix for bug663

More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.

Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.

Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datatypes.

Support for default grammar for datatypes in sygus. Support vts for infinity.

Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.

Sygus support for inductive datatypes.

Implement virtual term substitution for non-nested quantifiers.  Fix soundness bug in strings related to explaining length terms.

Disable bug590.smt2

minor change to the last fix

Merge branch 'master' of https://github.com/CVC4/CVC4

Hotfix for substr function.

Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions.  Dump synth by default in sygus, update regressions.  Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

Fix for BOOST_SED_CPP for gcc-5.

Squashed merge of SygusComp 2015 branch.

Add option --full-saturate-quant-rd.  Fix option --register-quant-body-terms.

fix bug 650

Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching.  Avoid unecessary delta lemmas.  Update casc scripts.

On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script.

Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence.  Update casc 25 FOF script.

fix sets-translate

fix smt2 parameterized sort printing

Module to infer alpha equivalence of quantified formulas.  Minor clean up of options.

Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.

Do not assert fail for fmf empty domains. Fixes bug 644.

Add --user-pat=interleave. Remove unused lte inst strategy.

Avoid completion for large finite types.  Fix bug for --fmf-fun.

Make array basis term a skolem (avoids crashing in fmf).

Changing options for QF_AUFNIA to avoid bug

Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyProof().

Handing the case in replay where a cut is directly in conflict with an existing bound.

Fixes for shared term normalization in replay for constraint construction.

Turning off aggressive arith ite simplifications during incremental solving.

Robust check to avoid store all instantiations. Fix prior commit for sort inference.

Changing the run script for master for the application track.

Restricting TheoryArith to computeRelevantTerms.

Disable sort inference for SMT COMP

Fixed bug in iteSimp