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.
Tim King [Tue, 27 Sep 2016 16:18:34 +0000 (09:18 -0700)]
Reverting part of the previous changes to unconstrained simplifier.
Tim King [Mon, 26 Sep 2016 04:34:40 +0000 (21:34 -0700)]
Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.
Tim King [Mon, 26 Sep 2016 04:34:03 +0000 (21:34 -0700)]
Adding missing break statements.
Tim King [Mon, 26 Sep 2016 04:03:39 +0000 (21:03 -0700)]
Closing an open file descriptor in MemoryMapFile.
Tim King [Mon, 26 Sep 2016 03:53:23 +0000 (20:53 -0700)]
Freeing memory in error handling code for bounded_token_buffer.
Tim King [Mon, 26 Sep 2016 03:46:26 +0000 (20:46 -0700)]
Deleting the eager bitblasting solver if present in TheoryBV.
Tim King [Mon, 26 Sep 2016 03:44:09 +0000 (20:44 -0700)]
Adding a destructor to QuantAntiSkolem.
Tim King [Mon, 26 Sep 2016 03:28:30 +0000 (20:28 -0700)]
Adding a destructor to TermDb.
Tim King [Mon, 26 Sep 2016 03:28:08 +0000 (20:28 -0700)]
Adding a destructor to CegqiOutputSingleInv.
Tim King [Mon, 26 Sep 2016 02:43:11 +0000 (19:43 -0700)]
Deleting optional members of StrongSolverTheoryUF.
Tim King [Mon, 26 Sep 2016 01:32:40 +0000 (18:32 -0700)]
Disambiguating a vector insert warning coming from coverity scan.
Tim King [Mon, 26 Sep 2016 01:20:52 +0000 (18:20 -0700)]
Deleting a temporary in theory sets enumerator.
Tim King [Mon, 26 Sep 2016 01:10:23 +0000 (18:10 -0700)]
Deleting the intermediate command singleton.
Tim King [Mon, 26 Sep 2016 00:30:23 +0000 (17:30 -0700)]
Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.
Tim King [Sun, 25 Sep 2016 23:18:34 +0000 (16:18 -0700)]
Adding virtual destructors to several classes in expr.h .
Tim King [Sun, 25 Sep 2016 22:52:57 +0000 (15:52 -0700)]
Removing an unused iterator.
Tim King [Sun, 25 Sep 2016 22:49:52 +0000 (15:49 -0700)]
Fixing a potential use after free coming from a pop_back() call invalidating strictly earlier entries.
Tim King [Sun, 25 Sep 2016 22:18:31 +0000 (15:18 -0700)]
Integrating a working coverity_scan travis rule back into
Paul Meng [Fri, 23 Sep 2016 22:43:05 +0000 (17:43 -0500)]
fixed a few bugs
ajreynol [Wed, 21 Sep 2016 14:10:18 +0000 (09:10 -0500)]
Remove duplicate code from my last commit
Tim King [Wed, 21 Sep 2016 07:07:32 +0000 (00:07 -0700)]
Fixing an error in the previous travis commit.
Tim King [Wed, 21 Sep 2016 06:50:49 +0000 (23:50 -0700)]
Updating the travis file for coverity scan.
ajreynol [Tue, 20 Sep 2016 22:46:13 +0000 (17:46 -0500)]
Refactor, separate theory-specific counterexample-guided instantiation.
ajreynol [Tue, 20 Sep 2016 21:02:14 +0000 (16:02 -0500)]
More refactoring of cbqi. Add a few regressions. Add option for qcf.
Tim King [Mon, 19 Sep 2016 03:31:41 +0000 (20:31 -0700)]
Merge pull request #92 from timothy-king/travis-cpp11
Adding a gnu++11 rule to travis.
Tim King [Sun, 18 Sep 2016 22:50:46 +0000 (15:50 -0700)]
Adding a clang format file for the project.
Adds a single example of applying this clang-format.
Tim King [Wed, 31 Aug 2016 04:31:59 +0000 (21:31 -0700)]
Adding a gnu++11 rule to travis.
ajreynol [Sun, 18 Sep 2016 22:21:17 +0000 (17:21 -0500)]
Minor fix for strings
guykatzz [Sat, 17 Sep 2016 00:18:56 +0000 (17:18 -0700)]
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
guykatzz [Sat, 17 Sep 2016 00:10:51 +0000 (17:10 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4
ajreynol [Sat, 17 Sep 2016 00:06:05 +0000 (19:06 -0500)]
Use matching heuristics for EPR instantiation.
Guy [Fri, 16 Sep 2016 23:26:30 +0000 (16:26 -0700)]
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
Guy [Fri, 16 Sep 2016 22:43:47 +0000 (15:43 -0700)]
Let arith_proof print its own terms
ajreynol [Fri, 16 Sep 2016 17:47:23 +0000 (12:47 -0500)]
More refactoring of cbqi, start developing new interface.
ajreynol [Thu, 15 Sep 2016 23:44:04 +0000 (18:44 -0500)]
Further refactor cbqi.
ajreynol [Thu, 15 Sep 2016 21:10:20 +0000 (16:10 -0500)]
Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.