Clark Barrett [Mon, 28 Nov 2016 21:54:02 +0000 (13:54 -0800)]
Merge pull request #112 from 4tXJ7f/fix_mult_distrib
Fix `MultDistrib` rewrite rule
ajreynol [Tue, 22 Nov 2016 19:26:26 +0000 (13:26 -0600)]
Fix smt2 and cvc printers for testers when output and input languages are different.
Tim King [Tue, 22 Nov 2016 07:25:25 +0000 (23:25 -0800)]
Merge pull request #111 from 4tXJ7f/fix_test_includes
Remove unused, libstdc++-exclusive include
Andres Notzli [Tue, 22 Nov 2016 02:07:45 +0000 (18:07 -0800)]
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`.
Andres Notzli [Tue, 22 Nov 2016 01:17:05 +0000 (17:17 -0800)]
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.
ajreynol [Mon, 21 Nov 2016 15:52:52 +0000 (09:52 -0600)]
Refactoring related to track instantiation option.
Clark Barrett [Fri, 18 Nov 2016 23:28:47 +0000 (15:28 -0800)]
Fix for unit test after changing default "all supported" logic name.
Tim King [Fri, 18 Nov 2016 23:17:31 +0000 (15:17 -0800)]
Removing some throw specifiers from OutputChannel. Fixes bug 716.
Clark Barrett [Fri, 18 Nov 2016 23:20:00 +0000 (15:20 -0800)]
Merge pull request #110 from 4tXJ7f/fix_makefiles
Fix Makefiles in test
Clark Barrett [Fri, 18 Nov 2016 23:09:07 +0000 (15:09 -0800)]
Modified a couple of regressoins to use ALL/QF_ALL instead of ALL_SUPPORTED/QF_ALL_SUPPORTED
Clark Barrett [Fri, 18 Nov 2016 23:01:59 +0000 (15:01 -0800)]
Add support for set-logic ALL, fix compiler error in GCC 6.1
Andres Notzli [Fri, 18 Nov 2016 02:24:47 +0000 (18:24 -0800)]
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.
Clark Barrett [Wed, 16 Nov 2016 23:54:48 +0000 (15:54 -0800)]
Merge pull request #108 from timothy-king/smt2-parser-exception-leaks
Adding garbage collection for the Smt2 Parser for Commands when excep…
PaulMeng [Wed, 16 Nov 2016 19:22:02 +0000 (13:22 -0600)]
Merge pull request #109 from PaulMeng/master
relational solver code refactor and bug fixes
Paul Meng [Tue, 15 Nov 2016 02:09:07 +0000 (20:09 -0600)]
relational solver code refactor and bug fixes
ajreynol [Mon, 14 Nov 2016 21:42:15 +0000 (15:42 -0600)]
Minor improvement to caching for extf bv inferences.
Tim King [Mon, 14 Nov 2016 04:34:10 +0000 (20:34 -0800)]
Adding garbage collection for the Smt2 Parser for Commands when exceptions are thrown.
Tim King [Sun, 13 Nov 2016 09:05:26 +0000 (01:05 -0800)]
Switching a large allocation to be heap allocated.
Tim King [Sun, 13 Nov 2016 08:33:40 +0000 (00:33 -0800)]
Deleting a parsed Command in the interactive_shell_black test.
Clark Barrett [Sat, 12 Nov 2016 23:27:13 +0000 (15:27 -0800)]
Merge pull request #107 from timothy-king/smt1-parser-exception-leaks
Adding garbage collection for the Smt1 Parser for Commands when…
Clark Barrett [Sat, 12 Nov 2016 23:25:42 +0000 (15:25 -0800)]
Merge pull request #106 from timothy-king/cvc-parser-exception-leaks
Adding garbage collection for the CVC Parser for Commands when except…
Clark Barrett [Sat, 12 Nov 2016 17:16:33 +0000 (09:16 -0800)]
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).
Tim King [Sat, 12 Nov 2016 08:05:36 +0000 (00:05 -0800)]
Adding garbage collection for the Smt1 Parser for Commands when exceptions are thrown.
Tim King [Sat, 12 Nov 2016 06:13:22 +0000 (22:13 -0800)]
Adding garbage collection for the CVC Parser for Commands when exceptions are thrown.
Tim King [Sat, 12 Nov 2016 00:44:19 +0000 (16:44 -0800)]
Merge pull request #105 from timothy-king/delete-maxed-out
Adding garbage collection of nodes with maxed out reference counts.
Tim King [Sat, 12 Nov 2016 00:25:05 +0000 (16:25 -0800)]
Deleting successfully parsed commands in the parser_black unit test.
Tim King [Sat, 12 Nov 2016 00:04:51 +0000 (16:04 -0800)]
Deleting the remaining commands in the Parser's queue within ~Parser().
Tim King [Fri, 11 Nov 2016 23:46:29 +0000 (15:46 -0800)]
Applying clang-format to parser.cpp.
Tim King [Fri, 11 Nov 2016 22:46:30 +0000 (14:46 -0800)]
Speeding up the common branches for inc().
Clark Barrett [Fri, 11 Nov 2016 22:41:51 +0000 (14:41 -0800)]
Enable eager bitblasting for QF_ABV when no stores are present.
ajreynol [Fri, 11 Nov 2016 18:59:13 +0000 (12:59 -0600)]
Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.
Tim King [Thu, 10 Nov 2016 23:56:19 +0000 (15:56 -0800)]
Fixing a delete vs free mismatch in parser_builder_black.h.
Tim King [Thu, 10 Nov 2016 23:22:49 +0000 (15:22 -0800)]
Adding garbage collection of nodes with maxed out reference counts.
Tim King [Thu, 10 Nov 2016 17:40:23 +0000 (09:40 -0800)]
Added PtrCloser guards for constructNodePtr. This ensures garbage collection on type checking exceptions.
ajreynol [Thu, 10 Nov 2016 14:55:14 +0000 (08:55 -0600)]
Add option for enabling/disabling lazy extended function reduction in bitvectors.
Tim King [Thu, 10 Nov 2016 01:04:02 +0000 (17:04 -0800)]
Merge pull request #103 from timothy-king/uniq-ptr
Adds a C++05 version of unique_ptr. Used this to solve a garbage coll…
Tim King [Wed, 9 Nov 2016 22:09:25 +0000 (14:09 -0800)]
Renaming the class PtrCloser to not cause confusion with unique_ptr.
Tim King [Wed, 9 Nov 2016 21:46:43 +0000 (13:46 -0800)]
Merge branch 'master' into uniq-ptr
ajreynol [Wed, 9 Nov 2016 19:01:20 +0000 (13:01 -0600)]
Fix tptp parser memory leaks for include.
ajreynol [Tue, 8 Nov 2016 16:35:46 +0000 (10:35 -0600)]
Minor fixes related to ExtTheory + incremental, fixes bug760.
ajreynol [Tue, 8 Nov 2016 16:09:53 +0000 (10:09 -0600)]
Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.
Tim King [Tue, 8 Nov 2016 00:04:57 +0000 (16:04 -0800)]
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…
Tim King [Mon, 7 Nov 2016 21:38:53 +0000 (13:38 -0800)]
Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures are too hard for the unit testing framework.
Tim King [Mon, 7 Nov 2016 19:44:52 +0000 (11:44 -0800)]
Changing ArrayStoreAll's constructor to delay allocation until it is done checking error conditions. This prevents a memory leak in exception throwing branches.
Tim King [Mon, 7 Nov 2016 19:10:17 +0000 (11:10 -0800)]
Fixing a memory leak in the CnfStream unit tests.
Tim King [Mon, 7 Nov 2016 18:24:11 +0000 (10:24 -0800)]
Fixing a memory leak in the eager bitblaster.
Tim King [Mon, 7 Nov 2016 06:27:00 +0000 (22:27 -0800)]
Adds a C++05 version of unique_ptr. Used this to solve a garbage collection problem caused by memory leaks of heap allocated Parsers.
Tim King [Mon, 7 Nov 2016 05:24:06 +0000 (21:24 -0800)]
Merge pull request #102 from timothy-king/node-id-eq
This switches the ZombieSet in the NodeManager to use NodeValue's id …
Tim King [Mon, 7 Nov 2016 00:05:29 +0000 (16:05 -0800)]
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.
Clark Barrett [Sat, 5 Nov 2016 14:39:09 +0000 (07:39 -0700)]
Merge pull request #101 from 4tXJ7f/fix_leak
Fix three leaks in unit tests
Andres Notzli [Sat, 5 Nov 2016 01:21:38 +0000 (18:21 -0700)]
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.
Clark Barrett [Sat, 5 Nov 2016 04:07:15 +0000 (21:07 -0700)]
Fix memory leak in node_black unit test.
ajreynol [Fri, 4 Nov 2016 21:28:20 +0000 (16:28 -0500)]
Fix a few more minor memory leaks.
ajreynol [Thu, 3 Nov 2016 22:31:05 +0000 (17:31 -0500)]
Make data points accurate in sep logic models.
ajreynol [Thu, 3 Nov 2016 20:09:12 +0000 (15:09 -0500)]
Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.
Tim King [Thu, 3 Nov 2016 15:32:27 +0000 (08:32 -0700)]
Merge pull request #100 from 4tXJ7f/fix_context_mm_black
Fix back() of empty deque in context_mm_black test
Andres Notzli [Wed, 2 Nov 2016 23:55:37 +0000 (16:55 -0700)]
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.
ajreynol [Wed, 2 Nov 2016 20:02:07 +0000 (15:02 -0500)]
Add missing regression.
ajreynol [Wed, 2 Nov 2016 19:58:36 +0000 (14:58 -0500)]
Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. Fix a few more memory leaks.
ajreynol [Wed, 2 Nov 2016 17:42:25 +0000 (12:42 -0500)]
Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.
ajreynol [Tue, 1 Nov 2016 21:47:24 +0000 (16:47 -0500)]
Minor fix to cvc3_compat.
ajreynol [Tue, 1 Nov 2016 20:39:39 +0000 (15:39 -0500)]
Make tuple and record names unique. Do not print internal datatype declaration in cvc printer.
ajreynol [Tue, 1 Nov 2016 19:31:41 +0000 (14:31 -0500)]
Fix memory leak in TheorySetsRels. Minor cleanup.
ajreynol [Tue, 1 Nov 2016 19:23:30 +0000 (14:23 -0500)]
Revert change to Datatypes API to return vector of DatatypeTypes, as before. ASAN failures with datatypes should now be mostly fixed.
ajreynol [Tue, 1 Nov 2016 18:33:38 +0000 (13:33 -0500)]
Revert change to datatypes API for passing pointers, instead make deep copy during call to mkMutualDatatypes.
ajreynol [Tue, 1 Nov 2016 18:20:49 +0000 (13:20 -0500)]
Working memory leak free version, changes interface to pointers.
ajreynol [Mon, 31 Oct 2016 15:45:27 +0000 (10:45 -0500)]
Minor refactoring in preparation for datatypes node cycle breaking.
ajreynol [Fri, 28 Oct 2016 22:14:04 +0000 (17:14 -0500)]
Add get instantiations utilities to API.
Clark Barrett [Thu, 27 Oct 2016 17:11:22 +0000 (10:11 -0700)]
Merge pull request #99 from 4tXJ7f/fix_dist_build3
Fix typo in Makefile that makes distcheck fail
Andres Notzli [Wed, 26 Oct 2016 23:04:21 +0000 (16:04 -0700)]
Fix typo in Makefile that makes distcheck fail
ajreynol [Wed, 26 Oct 2016 22:10:28 +0000 (17:10 -0500)]
Enable bv2nat regressions
Andrew Reynolds [Wed, 26 Oct 2016 21:26:57 +0000 (16:26 -0500)]
Merge pull request #98 from 4tXJ7f/fix_dist_build
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
ajreynol [Wed, 26 Oct 2016 21:23:58 +0000 (16:23 -0500)]
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Andres Notzli [Mon, 24 Oct 2016 00:14:14 +0000 (17:14 -0700)]
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
This commit adds regress4 to the `test/regress/Makefile.am`.
ajreynol [Fri, 21 Oct 2016 19:21:05 +0000 (14:21 -0500)]
Fix/add missing makefiles.
ajreynol [Fri, 21 Oct 2016 19:01:17 +0000 (14:01 -0500)]
Move slow regress0 benchmarks to regress1, increment regress1 through regress3.
Tim King [Wed, 19 Oct 2016 16:40:12 +0000 (09:40 -0700)]
Merge pull request #97 from 4tXJ7f/fix_rewrite
Fix minor bug and typo in boolean rewriter
Andres Notzli [Wed, 19 Oct 2016 09:58:59 +0000 (02:58 -0700)]
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.
ajreynol [Thu, 13 Oct 2016 22:44:19 +0000 (17:44 -0500)]
Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.
Tim King [Thu, 13 Oct 2016 18:30:17 +0000 (11:30 -0700)]
Initializes RoundingMode::roundNearestTiesToAway to a distinct value.
Tim King [Thu, 13 Oct 2016 07:22:24 +0000 (00:22 -0700)]
Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"
This reverts commit
3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to
5f415d4585134612bc24e9a823289fee35541a01.
Paul Meng [Tue, 11 Oct 2016 18:54:20 +0000 (13:54 -0500)]
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Paul Meng [Tue, 11 Oct 2016 18:43:28 +0000 (13:43 -0500)]
- fixed a memory leak issue with context dependent data structure
- clean up
Tim King [Mon, 3 Oct 2016 05:01:27 +0000 (22:01 -0700)]
Adding initializers for structs internal to ite_utilities.
guykatzz [Thu, 6 Oct 2016 06:39:48 +0000 (23:39 -0700)]
Added an option that allow empty dependencies when attempting to minimize preprocessing holes
Tim King [Mon, 3 Oct 2016 04:20:09 +0000 (21:20 -0700)]
Removing the throw specifiers from theory_uf_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:19:22 +0000 (21:19 -0700)]
Removing the throw specifiers from theory_fp_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:17:50 +0000 (21:17 -0700)]
Removing the throw specifiers from theory_datatypes_type_rules.h.
Tim King [Mon, 3 Oct 2016 04:16:28 +0000 (21:16 -0700)]
Removing an unused member from TreeLog.
Tim King [Mon, 3 Oct 2016 04:15:01 +0000 (21:15 -0700)]
Removing the throw specifiers from theory_bv_type_rules.h.
Tim King [Mon, 3 Oct 2016 01:08:29 +0000 (18:08 -0700)]
Removing the throw specifiers from Cardinality.
Tim King [Sat, 1 Oct 2016 22:40:30 +0000 (15:40 -0700)]
Removing the throw specifiers from Result.
Tim King [Sat, 1 Oct 2016 22:12:20 +0000 (15:12 -0700)]
Merge pull request #93 from timothy-king/clang-format
Adding a clang format file for the project.
Tim King [Sat, 1 Oct 2016 21:06:20 +0000 (14:06 -0700)]
Removing the throw specifiers from SExpr.
Tim King [Sat, 1 Oct 2016 20:50:32 +0000 (13:50 -0700)]
Removing the throw specifiers from SubrangeBounds.
ajreynol [Sat, 1 Oct 2016 12:08:45 +0000 (07:08 -0500)]
Incorporate non-bv parts of ajr/bvExt branch
ajreynol [Thu, 29 Sep 2016 22:48:33 +0000 (17:48 -0500)]
Address some coverity warnings, add another stat.
ajreynol [Thu, 29 Sep 2016 21:01:34 +0000 (16:01 -0500)]
Minor cleanup and additions to quantifiers statistics.
Kshitij Bansal [Wed, 28 Sep 2016 16:03:08 +0000 (12:03 -0400)]
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).
Tim King [Tue, 27 Sep 2016 16:20:11 +0000 (09:20 -0700)]
Removing an unused iterator.