Deleting optional members of StrongSolverTheoryUF.

Disambiguating a vector insert warning coming from coverity scan.

Deleting a temporary in theory sets enumerator.

Deleting the intermediate command singleton.

Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.

Adding virtual destructors to several classes in expr.h .

Removing an unused iterator.

Fixing a potential use after free coming from a pop_back() call invalidating strictly earlier entries.

Integrating a working coverity_scan travis rule back into 

Remove duplicate code from my last commit

Fixing an error in the previous travis commit.

Updating the travis file for coverity scan.

Refactor, separate theory-specific counterexample-guided instantiation.

More refactoring of cbqi. Add a few regressions. Add option for qcf.

Merge pull request #92 from timothy-king/travis-cpp11

Adding a gnu++11 rule to travis.

Adding a gnu++11 rule to travis.

Minor fix for strings

In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly

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

Use matching heuristics for EPR instantiation.

Handling a corner case where a ROW's guard is a constant disequality.
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality

Let arith_proof print its own terms

More refactoring of cbqi, start developing new interface.

Further refactor cbqi.

Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.

Make sep pto a trigger kind, track in equality engines and term database.

Refactor setIncomplete in quantifiers.

Support for unique variable generation in node manager.

Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR

Minor changes to sep logic, epr, quantifier splitting.

Refactor prenex modes.

Remove old implementation of cbqi

Prefer non-cardinality constants in term models for sep logic.

Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry breaking in theory sep.

Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.

Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic.  Update logics on sep regressions.

Refactor seplog preprocess. Handle case where sep data type cannot be inferred.

Miniscope top level conjunctions for prenex normal form, allow one level miniscoping in prenex normal form.

Option for prenex normal form

Merge pull request #91 from timothy-king/no-throw

Relaxing the throw specifiers for the destructors for Node, TypeNode,…

Fix boolean term issue in invariants from sygus. Minor default options changes for cbqi.

Cleanup quantifier elimination in smt engine.

Updates to cbqi.  New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.

Relaxing the throw specifiers for the destructors for Node, TypeNode, the context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.

Removing the forward declaration of QuantInfo from rewrite_engine.h.

Cleaning up the dead FORIT macros.

Removing the usage of typeof from theory_sets_private.

Beautifying theory_model.h.

Removing BOOST_FOREACH from theory/sets/scrutinize.h.

Removing typeof from sets normal form and beautifying the file.

Removing typeof from command_executor_portfolio.cpp.

Removing typeof from didyoumean.cpp.

Basic support for EPR+CBQI. Minor cleanup.

Minor cleanup preprocessing, add ppNotifyAssertions.

Options for counterexample guided instantiation.

Fixed two bugs

Added fitsSignedLong and fitsUnsignedLong

Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.

Expression sharing on demand in LFSC (replace definitionally equivalent child arguments after successful comparison).

Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership.

Add a few more regressions.

Minor fixes to model construction to take singleton equivalence classes into account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.

Merge pull request #90 from 4tXJ7f/fewer_preproc_holes

Add support for fewer preprocessing holes

Add support for fewer preprocessing holes

This commit adds support for the --fewer-preprocessing-holes flag. This
flag changes the preprocessing part in proofs in two ways: it (1)
removes assertions that are just restating inputs and uses the inputs
directly instead and it (2) changes the form of the preprocessed
assertions to contain the input that they originate from.

The code in this commit is mostly taken from the proofs branch in Guy's
fork.

Minor change to strings, introduce proxy vars only when necessary.

Improvements to strings: work on propagations for reverse normal form processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.

Merge pull request #89 from 4tXJ7f/fix_proof_spaces

Fix missing/redundant spaces in proofs

Fixes for sep star rewrite.

Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

Merge pull request #88 from 4tXJ7f/fix_comments

Minor: add/fix comments, remove redundant includes

Minor: add/fix comments, remove redundant includes

Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.

Merge pull request #87 from 4tXJ7f/fix_oob_access

Fix out-of-bounds access in ExprManager

Prioritize inferences when processing normal forms in strings.

The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas L' that originated from L and were used in the unsat core

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

Bug fix involving negated lemmas

Fix bug 749.

Add the negative conjunction case

Fix out-of-bounds access in ExprManager

The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough
because the INC_STAT macro tries to access
`d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an
out-of-bounds access. Found bug with UBSan.

Proper instrumentation of the preprocessing phase

proper handling of ITEs

Proper handling of IFF lemmas in the unsat core.
Don't return duplicates in the unsat core

Added an option for a more aggressive weakest implicant optimization

If we can't find a weaker implicant, fail gracefully and return the original lemma

Merge pull request #86 from 4tXJ7f/fix_warnings

Fix warnings in src/proof

Fix warnings in src/proof

Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.

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

Bug fix:
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay

Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.

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

Letification of BV constants

Minor improvements to strings related to constant splitting, including a few options (disabled by default).

Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.

Bug fix

Propagate the usage of proof let maps into constant disequality proofs

Bug fix

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

cleanup

Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)