Eliminating a signed vs. unsigned comparison.

Changing getTearDownIncremental() to return the type of options::tearDownIncremental.

Adding a destructor to InstantiationNotify.

Adding a destructor to RepBoundExt.

Reordering sep and sets in Makefile.theories.

Merge pull request #119 from 4tXJ7f/smt_v2_5

Switch from SMT-LIB v2.0 to v2.5 for smt2 files

Switch from SMT-LIB v2.0 to v2.5 for smt2 files

As mentioned in bug 741, CVC4 was parsing `.smt2` files using the
SMT-LIB v2.0 standard by default. This commit switches to v2.5.

Made tear-down-incremental more like it used to be: when tear-down value
is 1, it does not automatically enable incremental mode.

Merge pull request #118 from 4tXJ7f/fix_emp

Fix split-find-unsat-w-emp test

Merge pull request #117 from 4tXJ7f/fix_order

Fix initialization order

Fix split-find-unsat-w-emp test

Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the
split-find-unsat-w-emp test, this commit fixes that.

Merge branch 'master' into fix_order

Merge pull request #116 from 4tXJ7f/fix_mult

Fix (inactive) `MultSlice` rewrite

Fixing a use after free bug in Polynomial::denominatorLCM.

Fix initialization order

This commit addresses the following warning:

```
warning: field 'd_negOne' will be initialized after field 'd_pivots'
[-Wreorder]
```

Fix (inactive) `MultSlice` rewrite

The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.

Enable remaining cardinality benchmarks

Add missing regression

Add sets regression, fixes bug 754.  Minor fix to regexp in strings.

Added cardinality to cvc language, fixes bug 753. Throw logic exception when using cardinality on sets with finite element type.

Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.

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

Turned off nonClausalSimplify when using fewerPreprocessingHoles.
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.

Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.

Fix nf exp tracking for non-linear string equalities, fixes bug 768.

Improve bounds for global heap in sep, refactor preprocessing. Minor improvement to sets.

Added "dump=raw-benchmark" option for dumping all user commands exactly as received.

Fix unit test for datatypes, add interface functions to datatypes.

Fix for bug 734

Cleaning up Statistics::copyFrom to avoid casts.

Initializing the d_pivots variable.

Merge pull request #95 from 4tXJ7f/fix_sierra_build

Revert "Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a…

Merge pull request #113 from 4tXJ7f/remove_extract_rule

Remove wrong `ExtractMultLeadingBit` rule

Bug fixes and refactoring of parametric datatypes, add some regressions.

Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.

Fix build on macOS Sierra

Before this fix, the build died with `ar: no archive members specified
when linking the empty libreplacements.la.` because macOS Sierra does
not require the replacements anymore. With this fix, `ffs.c` and
`strtok_r.c` are always getting compiled (even when they are empty) to
prevent the error. Also removed the unused
`CVC4_NEEDS_REPLACEMENT_FUNCTIONS` from `configure.ac` and added an
`#ifndef HAVE_FFS` to `ffs.c` for consistency with `strtok_r.c`.

Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 and 763.

Improvement and bug fix for str.indexof reduction, add regression. Other minor changes.

Remove wrong `ExtractMultLeadingBit` rule

The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.

Merge pull request #115 from 4tXJ7f/bug766

Fix parsing of BVROTR by CVC parser

Merge pull request #114 from 4tXJ7f/add_unit_test

Add unit test for `MultDistrib` rule

Fix parsing of BVROTR by CVC parser

This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.

Add unit test for `MultDistrib` rule

This unit test checks that the issue fixed by commit
c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved.

Merge pull request #112 from 4tXJ7f/fix_mult_distrib

Fix `MultDistrib` rewrite rule

Fix smt2 and cvc printers for testers when output and input languages are different.

Merge pull request #111 from 4tXJ7f/fix_test_includes

Remove unused, libstdc++-exclusive include

Fix `MultDistrib` rewrite rule

The assertion in the `MultDistrib` rule would fail when doing:

```
Node expr = d_nm->mkNode(BITVECTOR_MULT, mkNode(BITVECTOR_SUB, x, y), z);
if (RewriteRule<MultDistrib>::applies(expr))
  RewriteRule<MultDistrib>::apply(expr);
```

When checking which side to distribute over, the code only checked for
`BITVECTOR_PLUS` instead of `BITVECTOR_PLUS` or `BITVECTOR_SUB` in
contrast to the other conditions in
`RewriteRule<MultDistrib>::applies()` and the assert.

NOTE: I was only able to reproduce this issue when testing the rewrite
rule in isolation. The rule `SubEliminate` generally seems to turn the
`BITVECTOR_SUB` node into a `BITVECTOR_PLUS` node before the rewriter
tries `MultDistrib`.

Remove unused, libstdc++-exclusive include

The file `ext/stdio_filebuf.h` does not seem to be available in libc++,
which made compilation of the unit tests for macOS unnecessarily
complicated given that it is not used anyway.

Refactoring related to track instantiation option.

Fix for unit test after changing default "all supported" logic name.

Removing some throw specifiers from OutputChannel. Fixes bug 716.

Merge pull request #110 from 4tXJ7f/fix_makefiles

Fix Makefiles in test

Modified a couple of regressoins to use ALL/QF_ALL instead of ALL_SUPPORTED/QF_ALL_SUPPORTED

Add support for set-logic ALL, fix compiler error in GCC 6.1

Fix Makefiles in test

With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.

Merge pull request #108 from timothy-king/smt2-parser-exception-leaks

Adding garbage collection for the Smt2 Parser for Commands when excep…

Merge pull request #109 from PaulMeng/master

relational solver code refactor and bug fixes

relational solver code refactor and bug fixes

Minor improvement to caching for extf bv inferences.

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

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.