Merge pull request #100 from 4tXJ7f/fix_context_mm_black

Fix back() of empty deque in context_mm_black test

Fix back() of empty deque in context_mm_black test

The `testPushPop()` test case does a pop out of scope at the end that
lead to UB in `ContextManager::pop()` because it did a `deque::back()`
on an empty deque without checking. This commit adds an assertion in the
`ContextManager` and checks that the test case triggers the assertion.

Add missing regression.

Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. Fix a few more memory leaks.

Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.

Minor fix to cvc3_compat.

Make tuple and record names unique. Do not print internal datatype declaration in cvc printer.

Fix memory leak in TheorySetsRels.  Minor cleanup.

Revert change to Datatypes API to return vector of DatatypeTypes, as before.  ASAN failures with datatypes should now be mostly fixed.

Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.

Working memory leak free version, changes interface to pointers.

Minor refactoring in preparation for datatypes node cycle breaking.

Add get instantiations utilities to API.

Merge pull request #99 from 4tXJ7f/fix_dist_build3

Fix typo in Makefile that makes distcheck fail

Fix typo in Makefile that makes distcheck fail

Enable bv2nat regressions

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.