array theory builtinop

cleanup

dont tokenize bv operators (normal ones)

Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2

Fix for unconstrained bug.

Adding an example that violates an assertion during unconstrained simplification.

Making CVC4::theory::quantifiers::PrenexQuantMode public for now.

Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing.  Minor fix for conjecture generation for finite types.

Fix performance issue with variable triggers + instantiation restrictions.

Bug fix negative contains cache.

Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust.  Fix bug in conjecture generation for non-parameterized operators.

Removing the reference to THEORY_BOOL from the equality engine. This theory
id was used as an internal marker in a set of theories tagging reasons of a
propagated disequalities. Replaced it with THEORY_LAST which is not completely
kosher but is safe in the context being used.

Minor fixes for cegqi.

Merge pull request #71 from kbansal/const-are-triggers

change const are triggers from false to true in equality engines

Performance comparison:
   https://www.starexec.org/starexec/secure/details/job.jsp?id=6941

Bug opened for testcase that became much worse:
  http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621

Improvements and bug fixes related to cbqi/cegqi.  Minor fix for fmf with fun-def. Add skolemization options.

fix no return value warning

fix echo command in --tear-down-incremental

printer change for string smtlib2

change const are triggers from false to true in equality engines

Parsing support for define-fun-rec/define-funs-rec.

Decouple counter-example guided quantifier instantiation from Sygus.

Add requirePhase len(x) = 0.

Fixed proof unitialized memory and minor memory leaks.

Bug fix for BV

Patches for 32-bit ARM

Updating resize for occurence lists to properly resize the whole state.

Strings split on constant lengths, add length=0 to split lemma for empty string.

Minor fixes and improvements to cegqi-si for linear arithmetic.

CNF proofs.  Infrastructure for preprocessing proofs.  Updates to smt.plf signature.  Add regressions.

Minor fixes.  Extend cegqi-si to real arithmetic.

More work on arithmetic single invocation synthesis conjectures.

Revert "dummy commit to force nightly builds"

This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.

Robust strategy for single invocation LIA synthesis conjectures.  Add regressions.

Switch back to eager loop temporarily.

minor fix for internal string print

New trigger options.  --inst-no-entail on by default.  Misc cleanup.

dummy commit to force nightly builds

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

webget: curl follow redirect

Fix unit tests.

attempt to fix win32 builds

Minor cleanup, remove unused files.

Handle recursive singleton case for codatatypes, add regression.  Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

try curl before wget, workaround for issue with FTP PASV

Changing CXXFLAGS for custom cln installation in configure.ac.

Making sure the CVC4 flags do not get overwritten after being set.

Better support for solving multiple functions with cegqi-si.  Minor cleanup.

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