Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.

More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi=gen-ev for interpreted operators.

Fix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf-fun.

Fix compiler errors due to unbalanced throw specifiers.

Merge branch 'master' into google

Whitespace difference

A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).

Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

Merge pull request #73 from kbansal/parser-dont-tokenize

Parser dont tokenize

Changes needed to compile at Google, plus some bug fixes from Google.

Fix file permissions

Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.

Adding an example of a tester in SMT2.

Farkas proof coefficients.

This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.

Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
  To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
  There was a way to use a row twice in the construction of the conflicts.
  This was violating an assumption in the Tableau when constructing the intermediate rows.

Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
  before they are converted to externally understandable conflicts and propagations in the form
  of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
  to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
  vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
to the impliedByX (and similar functions).
For example,this is now longer both:
  void setAssertedToTheTheory(TNode witness);
  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
  There is just:
    void setAssertedToTheTheory(TNode witness, bool inConflict);

Patch for Kshitij's fix on requriePhase

Merge pull request #72 from kbansal/decision-requirephase

https://www.starexec.org/starexec/secure/details/job.jsp?id=6972

The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.

Fix option --quant-fun-wd.  Add mk_starexec script to contrib.

Handle (degenerate) case of synthesis conjectures for constants.  Disable delta lemmas.

disable failing sygus tests

update comment

string parser builtinop changes

bv parserchanges cleanup

fp builtinop parser changes

fp reorder tokens to match other occurences

THEORY_INTS parser changes

THEORY_REAL_INTS parser changes

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.

disable string reqressions timing out after change

DE requests respect requirePhase

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.