Merge pull request #98 from 4tXJ7f/fix_dist_build

Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build

New implementation of sets+cardinality.  Merge Paul Meng's relation solver as extension of sets solver, add regressions.

Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build

This commit adds regress4 to the `test/regress/Makefile.am`.

Fix/add missing makefiles.

Move slow regress0 benchmarks to regress1, increment regress1 through regress3.

Merge pull request #97 from 4tXJ7f/fix_rewrite

Fix minor bug and typo in boolean rewriter

Fix minor bug and typo in boolean rewriter

One of the rewrites in the boolean rewriter had the condition `n[0] ==
tt && n[0] == ff`, which could never be true. Another rewrite covers the
same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`.
This commit also fixes a minor typo.

Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.

Initializes RoundingMode::roundNearestTiesToAway to a distinct value.

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

This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.

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