Minor improvement to caching for extf bv inferences.

Switching a large allocation to be heap allocated.

Deleting a parsed Command in the interactive_shell_black test.

Merge pull request #107 from timothy-king/smt1-parser-exception-leaks

Adding garbage collection for the Smt1 Parser for Commands when…

Merge pull request #106 from timothy-king/cvc-parser-exception-leaks

Adding garbage collection for the CVC Parser for Commands when except…

Fixed a bug in cdhashmap in which doubly-linked list was not properly cleaned up on a call to obliterate.

Also, removed some experimental code and a unit test from cdmap_black that used it. This test created a CDList *in* context memory which seems like a very bad idea (and
it was improperly implemented resulting in a memory leak).

Adding garbage collection for the Smt1 Parser for Commands when exceptions are thrown.

Adding garbage collection for the CVC Parser for Commands when exceptions are thrown.

Merge pull request #105 from timothy-king/delete-maxed-out

Adding garbage collection of nodes with maxed out reference counts.

Deleting successfully parsed commands in the parser_black unit test.

Deleting the remaining commands in the Parser's queue within ~Parser().

Applying clang-format to parser.cpp.

Speeding up the common branches for inc().

Enable eager bitblasting for QF_ABV when no stores are present.

Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.

Fixing a delete vs free mismatch in parser_builder_black.h.

Adding garbage collection of nodes with maxed out reference counts.

Added PtrCloser guards for constructNodePtr. This ensures garbage collection on type checking exceptions.

Add option for enabling/disabling lazy extended function reduction in bitvectors.

Merge pull request #103 from timothy-king/uniq-ptr

Adds a C++05 version of unique_ptr. Used this to solve a garbage coll…

Renaming the class PtrCloser to not cause confusion with unique_ptr.

Merge branch 'master' into uniq-ptr

Fix tptp parser memory leaks for include.

Minor fixes related to ExtTheory + incremental, fixes bug760.

Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.

Merge pull request #104 from timothy-king/disabling-out-of-memory-tests-on-asan

Disabling out of memory tests unit tests when ASAN is enabled. ASAN f…

Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures are too hard for the unit testing framework.

Changing ArrayStoreAll's constructor to delay allocation until it is done checking error conditions. This prevents a memory leak in exception throwing branches.

Fixing a memory leak in the CnfStream unit tests.

Fixing a memory leak in the eager bitblaster.

Adds a C++05 version of unique_ptr. Used this to solve a garbage collection problem caused by memory leaks of heap allocated Parsers.

Merge pull request #102 from timothy-king/node-id-eq

This switches the ZombieSet in the NodeManager to use NodeValue's id …

This switches the ZombieSet in the NodeManager to use NodeValue's id for equality comparison. The previously used function NodeValueEq incorrectly identified VARIABLE nodes as being equal. This meant that on hash collisions these nodes could leak memory.

Merge pull request #101 from 4tXJ7f/fix_leak

Fix three leaks in unit tests

Fix three leaks in unit tests

The `testMultipleCollection` test case was allocating a
ListenerCollection without deleting it. The helper function
`countCommands` was not deleting the `Command`s returned from
`InteractiveShell::readCommand`. In the `testEmptyFileInput` and
`testSimpleFileInput` tests, the `filename` string was not deleted. This
commit fixes all issues.

Fix memory leak in node_black unit test.

Fix a few more minor memory leaks.

Make data points accurate in sep logic models.

Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.

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.