summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-16exampleunsat_core_exampleAndres Notzli
2016-11-08Minor fixes related to ExtTheory + incremental, fixes bug760.ajreynol
2016-11-08Add a few options to separation logic and sets. Minor changes to separation ↵ajreynol
logic, change syntax for empty heap constraint.
2016-11-07Merge pull request #104 from timothy-king/disabling-out-of-memory-tests-on-asanTim King
Disabling out of memory tests unit tests when ASAN is enabled. ASAN f…
2016-11-07Disabling out of memory tests unit tests when ASAN is enabled. ASAN failures ↵Tim King
are too hard for the unit testing framework.
2016-11-07Changing ArrayStoreAll's constructor to delay allocation until it is done ↵Tim King
checking error conditions. This prevents a memory leak in exception throwing branches.
2016-11-07Fixing a memory leak in the CnfStream unit tests.Tim King
2016-11-07Fixing a memory leak in the eager bitblaster.Tim King
2016-11-06Merge pull request #102 from timothy-king/node-id-eqTim King
This switches the ZombieSet in the NodeManager to use NodeValue's id …
2016-11-06This switches the ZombieSet in the NodeManager to use NodeValue's id for ↵Tim King
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.
2016-11-05Merge pull request #101 from 4tXJ7f/fix_leakClark Barrett
Fix three leaks in unit tests
2016-11-04Fix three leaks in unit testsAndres Notzli
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.
2016-11-04Fix memory leak in node_black unit test.Clark Barrett
2016-11-04Fix a few more minor memory leaks.ajreynol
2016-11-03Make data points accurate in sep logic models.ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-03Merge pull request #100 from 4tXJ7f/fix_context_mm_blackTim King
Fix back() of empty deque in context_mm_black test
2016-11-02Fix back() of empty deque in context_mm_black testAndres Notzli
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.
2016-11-02Add missing regression.ajreynol
2016-11-02Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ajreynol
Fix a few more memory leaks.
2016-11-02Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat.ajreynol
2016-11-01Minor fix to cvc3_compat.ajreynol
2016-11-01Make tuple and record names unique. Do not print internal datatype ↵ajreynol
declaration in cvc printer.
2016-11-01Fix memory leak in TheorySetsRels. Minor cleanup.ajreynol
2016-11-01Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ajreynol
ASAN failures with datatypes should now be mostly fixed.
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy ↵ajreynol
during call to mkMutualDatatypes.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-31Minor refactoring in preparation for datatypes node cycle breaking.ajreynol
2016-10-28Add get instantiations utilities to API.ajreynol
2016-10-27Merge pull request #99 from 4tXJ7f/fix_dist_build3Clark Barrett
Fix typo in Makefile that makes distcheck fail
2016-10-26Fix typo in Makefile that makes distcheck failAndres Notzli
2016-10-26Enable bv2nat regressionsajreynol
2016-10-26Merge pull request #98 from 4tXJ7f/fix_dist_buildAndrew Reynolds
Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK build
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-10-23Fix TRAVIS_CVC4 + TRAVIS_CVC4_DISTCHECK buildAndres Notzli
This commit adds regress4 to the `test/regress/Makefile.am`.
2016-10-21Fix/add missing makefiles.ajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-19Merge pull request #97 from 4tXJ7f/fix_rewriteTim King
Fix minor bug and typo in boolean rewriter
2016-10-19Fix minor bug and typo in boolean rewriterfix_rewriteAndres Notzli
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.
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-10-13Initializes RoundingMode::roundNearestTiesToAway to a distinct value.Tim King
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-10-11- fixed a memory leak issue with context dependent data structurePaul Meng
- clean up
2016-10-08Adding initializers for structs internal to ite_utilities.Tim King
2016-10-05Added an option that allow empty dependencies when attempting to minimize ↵guykatzz
preprocessing holes
2016-10-02Removing the throw specifiers from theory_uf_type_rules.h.Tim King
2016-10-02Removing the throw specifiers from theory_fp_type_rules.h.Tim King
2016-10-02Removing the throw specifiers from theory_datatypes_type_rules.h.Tim King
2016-10-02Removing an unused member from TreeLog.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback