summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ajreynol
--fmf-fun-rlv, fixes bug 723.
2016-12-01Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵ajreynol
and 763.
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other ↵ajreynol
minor changes.
2016-11-30Fix parsing of BVROTR by CVC parserAndres Notzli
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
2016-11-28Merge pull request #112 from 4tXJ7f/fix_mult_distribClark Barrett
Fix `MultDistrib` rewrite rule
2016-11-22Fix smt2 and cvc printers for testers when output and input languages are ↵ajreynol
different.
2016-11-21Fix `MultDistrib` rewrite ruleAndres Notzli
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`.
2016-11-21Refactoring related to track instantiation option.ajreynol
2016-11-18Removing some throw specifiers from OutputChannel. Fixes bug 716.Tim King
2016-11-18Add support for set-logic ALL, fix compiler error in GCC 6.1Clark Barrett
2016-11-16Merge pull request #108 from timothy-king/smt2-parser-exception-leaksClark Barrett
Adding garbage collection for the Smt2 Parser for Commands when excep…
2016-11-14relational solver code refactor and bug fixes Paul Meng
2016-11-14Minor improvement to caching for extf bv inferences.ajreynol
2016-11-13Adding garbage collection for the Smt2 Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-12Merge pull request #107 from timothy-king/smt1-parser-exception-leaksClark Barrett
Adding garbage collection for the Smt1 Parser for Commands when…
2016-11-12Merge pull request #106 from timothy-king/cvc-parser-exception-leaksClark Barrett
Adding garbage collection for the CVC Parser for Commands when except…
2016-11-12Fixed a bug in cdhashmap in which doubly-linked list was not properly ↵Clark Barrett
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).
2016-11-12Adding garbage collection for the Smt1 Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-11Adding garbage collection for the CVC Parser for Commands when exceptions ↵Tim King
are thrown.
2016-11-11Merge pull request #105 from timothy-king/delete-maxed-outTim King
Adding garbage collection of nodes with maxed out reference counts.
2016-11-11Deleting the remaining commands in the Parser's queue within ~Parser().Tim King
2016-11-11Applying clang-format to parser.cpp.Tim King
2016-11-11Speeding up the common branches for inc().Tim King
2016-11-11Enable eager bitblasting for QF_ABV when no stores are present.Clark Barrett
2016-11-11Add simple inferences for extended bitvector functions, add a few related ↵ajreynol
options. Use bv2nat, int2bv as triggers. Add regressions.
2016-11-10Adding garbage collection of nodes with maxed out reference counts.Tim King
2016-11-10Added PtrCloser guards for constructNodePtr. This ensures garbage collection ↵Tim King
on type checking exceptions.
2016-11-10Add option for enabling/disabling lazy extended function reduction in ↵ajreynol
bitvectors.
2016-11-09Renaming the class PtrCloser to not cause confusion with unique_ptr.Tim King
2016-11-09Merge branch 'master' into uniq-ptrTim King
2016-11-09Fix tptp parser memory leaks for include.ajreynol
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-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-06Adds a C++05 version of unique_ptr. Used this to solve a garbage collection ↵Tim King
problem caused by memory leaks of heap allocated Parsers.
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-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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback