Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
src/options/quantifiers_options

- fixed a memory leak issue with context dependent data structure
- clean up

Adding initializers for structs internal to ite_utilities.

Added an option that allow empty dependencies when attempting to minimize preprocessing holes

Removing the throw specifiers from theory_uf_type_rules.h.

Removing the throw specifiers from theory_fp_type_rules.h.

Removing the throw specifiers from theory_datatypes_type_rules.h.

Removing an unused member from TreeLog.

Removing the throw specifiers from theory_bv_type_rules.h.

Removing the throw specifiers from Cardinality.

Removing the throw specifiers from Result.

Merge pull request #93 from timothy-king/clang-format

Adding a clang format file for the project.

Removing the throw specifiers from SExpr.

Removing the throw specifiers from SubrangeBounds.

Incorporate non-bv parts of ajr/bvExt branch

Address some coverity warnings, add another stat.

Minor cleanup and additions to quantifiers statistics.

Fix the merge of kbansal/card branch (2039eab).

A bug was introduced in the cleanup process as preparation for the merge
(theory_sets_private.cpp, lines 2502-2508 in this commit).

Removing an unused iterator.

Reverting part of the previous changes to unconstrained simplifier.

Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.

Adding missing break statements.

Closing an open file descriptor in MemoryMapFile.

Freeing memory in error handling code for bounded_token_buffer.

Deleting the eager bitblasting solver if present in TheoryBV.

Adding a destructor to QuantAntiSkolem.

Adding a destructor to TermDb.

Adding a destructor to CegqiOutputSingleInv.

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 

fixed a few bugs

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 clang format file for the project.

Adds a single example of applying this clang-format.

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

fixed type checking and computing for PRODUCT and JOIN

Minor changes to sep logic, epr, quantifier splitting.

refactored the code, added more benchmarks and minor fixes

fixed capitalized "kind"

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.

Computed members for tp and product rels even they are not used in
membership constraints

also computed members for relations that do not have explicit membership
constraints

added more benchmarks

more fix for TC inference

fixed TC inference from graph constructed from a relation and the null
issue with TC explanation

Basic support for EPR+CBQI. Minor cleanup.

minor fix

Minor cleanup preprocessing, add ppNotifyAssertions.

Options for counterexample guided instantiation.

Merge remote-tracking branch 'origin/master'

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.