Move si solution reconstruction to own file, make more robust. Other refactoring.

Handle missing cases for single inv solution reconstruction.  Minor fixes. Refactor.

Minor clean up

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

Improved string performance, thanks to Peter's benchmarks.

Improved string performance, thanks to Peter's benchmarks.

Working version of sygus solution reconstruction from single inv cegqi.  Heuristics to fit syntax.

Initial draft of solution reconstruction into syntax for single inv cegqi.

Work on solution reconstruction for single inv.  Fix compiler error found by Tim regarding Trace.isOn

Refactor sygus_util to TermDb.  Initial work on solution reconstruction into syntax for single inv properties.

Start work on simplifying single inv solutions.  Minor.

Simple variable elimination for single inv properties.  Relax conditions for partial inst variables for LTE.

Solutions for single invocation conjectures.

Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring.  Do not apply exhaustive tester inference for sygus datatypes.

Representative programs must be minimal size, minor fixes, improvements to ITE handling in sygus.

Generalization of sygus lemmas based on arguments and content.

Bug fix fairness for commutative operators in sygus.  Minor.

Lemmas instead of conflicts in sygus sym break (do not expand explanations).  Minor improvements to sygus splitting.

Generalize conflict clauses in sygus sym break, merge caches, refactor.  Preparation for single invocation properties.  Set output lang to SMT2 for sygus.

Apply sygus search space narrowing for all subprograms of current global state.

Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module.  Refactor QuantifiersEngine registration and check.

Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas.

Add module for sygus search space narrowing based on global state.

Minor refactor CEGQI.

Always miniscope nested quantifiers.  Disable miniscoping when cegqi enabled.  Simplify option names.

Recognize when synthesis conjectures are in single invocation fragment.

Output solutions for synthesis conjectures with --dump-synth.  Minor refactor of previous commit.

Generalize sygus search space narrowing to arbitrary theory rewriting.

Variable patterns only look at eligible terms.  Minor refactoring of quantifiers check for sat.

Add --lte-restrict-inst-closure option.  Push dt.size fairness constraints inside splitting lemmas for sygus.

Refactor sygus arg nf.  Minor improvements.

CEGQI fairness based on term height.  Fix sygus-nf fairness bug for wrongly applied selectors.

Rework inst-closure.

Narrow sygus search space based on NNF and rewriting constant arguments.

Add option --lte-partial-inst.  Remove inst-closure.

Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators.

Avoid redundant constant arguments for SygusNormalForm. Refactor.

Initial work on sygusNormalForm.

Mark datatypes as sygus.  Add option to normalize sygus terms in search.  Add sygus regressions.

Handle miniscoping of conjunctions in synthesis properties.  Refactor construction of sygus datatypes.  Expand define-fun in evaluators.

Adding tests for get-value output for arithmetic.

Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.

Adding an additional search path to configure.ac for cxxtestgen to reflect the cxxtest git repository.

Avoid name conflicts for multiple synth-fun.

Linearize multiplication by constants in sygus grammars. Handle unary minus integer numerals.  Refactor to smt2.cpp.

Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments.  Handle ground properties in sythesis conjectures.

Minor: Ensure indexed terms are in EE.  Add support for bv constants in sygus parser.

sygus input language and benchmark

Fix #line numbering.

Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).

Remove private #include.

Fix typo.

Remove old .orig files that were added to the repository.

adjusted to both v2.0 and v2.5 string literals

blocked unprintable characters in string literals;
disabled string literal test case for smtlib v2.5

switch ascii encoding to unsigned char

patch to the last commit

bug fix, thanks to Pierre's report

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

added initial AX rules;
fixed a bug for empty string in regex

added initial AX rules;
fixed a bug for empty string in regex

Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter

Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

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

bug fix for constant regular expression model building

bug fix for constant regular expression model building

Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.

Add misc trigger options.

Fix oversight in dumping assertions in preprocessing.

Add cvc parsing support for cardinality constraints.  Bug fix for enumerating elements to meet cardinality lower bounds.

Minor fixes to language bindings. (Resolves #607.)

Option to enable/disable cyclicity check in datatypes.

bug fix, thanks to Guy's example.

Better error description (related to bug 605).

Cleanup.

Added string constant in java api example.

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

Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

Fix dt.size care graph.

Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).

clean up and improve intersection

Fix valgrind-flagged error about uninitialized value.

Fix segfault in lambdas when constructed via API.

Fix UnsatCore in language bindings.

Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

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

Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.

disable inter cache

Synchronize conjecture generation with E-matching.  Minor fix to --full-saturate-quant.

add intersection rewriting

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

add more regexp rewriting

add more functions for regular expressions

add more regexp rewriting

add more functions for regular expressions

Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.

added number of resource units used as a stat

Throw error when pattern is not list of terms.

Change default option to --inst-when=full-last-call (interleave instantiation and theory combination).  Fix inefficiency in NNF, enable by default.  Set best defaults for --mbqi=abs.

Disable constants sharing in eq engine, disable hack in theory engine.  Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine.