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

Fix for assertion failure:
smt_engine.cpp:1992: Rewriter::rewrite(d_assertions[i]) == d_assertions[i]
when --ite-simp and --repeat-simp are on

Fix for sort inference involving mixed Int/Real equalities.

A return value for an ApproxGLPK::loadVB() failure case was incorrect.

Avoid instantiating with array constants.

Ensure mkRep instantiation strategies do not violate types.

sync options of default-assertions run script with default

Fix crash in non-linear cbqi.

In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBack is already in conflict. This is needed as it can be called multiple times on the same constraint.

Make sygus an output language.  Parse declare-fun in sygus.  Minor improvements to robustness of sygus parsing.

Accelerate sygus solution reconstruction for constants and id functions.  Minor changes to sygus type registration.  Print sygus let solutions assuming fixed variable names.

remove runscripts from master meant for experimental submission

Avoid naming conflicts in sygus, refactor. Add missing regression.  Detect Start grammar. Add regression.

Handle duplicate operators in sygus grammars.  Parse sygus quoted literals. Add regression.

Update experimental scripts.  Support top-level non-terminals in sygus grammars.  Allow -N in sygus terms.  Minor bug fix in datatypes_sygus. Add regression.

Bug fix parsing constant constructor sygus.

Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus.  Bug fix sygus argument generalization.  Add regressions.

Parse support for sygus LetGTerm.

bump thread stack size to 1 GB

Bug fix instantiations for fmf-bound-int.  Disable nested pre-skolemization for non-UF logics.  Update SMT COMP scripts accordingly.

make comment precise

move delete beyond ifdef CVC4_COMPETITION_MODE

pcvc4 with assertions

update run script for assertions/scrambled run

assertions runscript (for testing) derived from current stable (default) script

for experimental, use incremental instead of teardown for all logics for testing purposes

move decision to use teardown or not to logics

Fix for last commit.

rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}

sync exerimental scripts with regular ones

Minor changes to smt comp script for quantified arith.  Add option --cbqi-sat whether to disable sat for quantified arith.

experimental run scripts

runscript thread stack 256

Refactoring of sygus parsing, properly parse Constant/Variable constructors.

application smtcomp

Flatten sygus grammars during parsing. Remove duplicate operators from grammars.

Add casc 25 tfn script.  Change tff script to output instantiations. Work towards parsing non-flattened sygus grammars.

When proof enabled, disable uf sym break. Add regression.

Do not enforce dt fairness when single invocation sygus.

changed resource step options to unsigned

added options for controlling resource step-count for various solving stages

Merge pull request #75 from Dunedune/master

Added missing LogicException to throws in method lemma.

Add missing regression

Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.

Added throw LogicException to method lemma.

Fixes related to cbqi + E-matching.

Avoid ensureLiteral on unpreprocessed formulas in cbqi.

Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.

Added Finn Haedicke as a contributor.

Merge pull request #74 from finnhaedicke/namespace_minisat

moved Minisat namespace into CVC4

Allow sygus with no syntactic restrictions for LIA.  Add regressions.

Add missing regression.

Support for arbitrary constants/variables in Sygus grammars.

Minor improvements to infrastructure. Minor changes to default options. Add tff script. Minor additions to sygus.

Add casc25 fnt script.

Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competition scripts (in progress).

Fix smt2 printing of fun-def. Simplification of mbqi interface.

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

Fixed problem with private/public header clash

Disambiguate namespaces in options, fix permissions

Updating failing unit tests.

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.