Age | Commit message (Collapse) | Author | |
---|---|---|---|
2016-12-02 | Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ | ajreynol | |
--fmf-fun-rlv, fixes bug 723. | |||
2016-12-01 | Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 ↵ | ajreynol | |
and 763. | |||
2016-12-01 | Improvement and bug fix for str.indexof reduction, add regression. Other ↵ | ajreynol | |
minor changes. | |||
2016-11-30 | Fix parsing of BVROTR by CVC parser | Andres Notzli | |
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com. | |||
2016-11-28 | Merge pull request #112 from 4tXJ7f/fix_mult_distrib | Clark Barrett | |
Fix `MultDistrib` rewrite rule | |||
2016-11-22 | Fix smt2 and cvc printers for testers when output and input languages are ↵ | ajreynol | |
different. | |||
2016-11-21 | Fix `MultDistrib` rewrite rule | Andres 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-21 | Refactoring related to track instantiation option. | ajreynol | |
2016-11-18 | Removing some throw specifiers from OutputChannel. Fixes bug 716. | Tim King | |
2016-11-18 | Add support for set-logic ALL, fix compiler error in GCC 6.1 | Clark Barrett | |
2016-11-16 | Merge pull request #108 from timothy-king/smt2-parser-exception-leaks | Clark Barrett | |
Adding garbage collection for the Smt2 Parser for Commands when excep… | |||
2016-11-14 | relational solver code refactor and bug fixes | Paul Meng | |
2016-11-14 | Minor improvement to caching for extf bv inferences. | ajreynol | |
2016-11-13 | Adding garbage collection for the Smt2 Parser for Commands when exceptions ↵ | Tim King | |
are thrown. | |||
2016-11-12 | Merge pull request #107 from timothy-king/smt1-parser-exception-leaks | Clark Barrett | |
Adding garbage collection for the Smt1 Parser for Commands when… | |||
2016-11-12 | Merge pull request #106 from timothy-king/cvc-parser-exception-leaks | Clark Barrett | |
Adding garbage collection for the CVC Parser for Commands when except… | |||
2016-11-12 | Fixed 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-12 | Adding garbage collection for the Smt1 Parser for Commands when exceptions ↵ | Tim King | |
are thrown. | |||
2016-11-11 | Adding garbage collection for the CVC Parser for Commands when exceptions ↵ | Tim King | |
are thrown. | |||
2016-11-11 | Merge pull request #105 from timothy-king/delete-maxed-out | Tim King | |
Adding garbage collection of nodes with maxed out reference counts. | |||
2016-11-11 | Deleting the remaining commands in the Parser's queue within ~Parser(). | Tim King | |
2016-11-11 | Applying clang-format to parser.cpp. | Tim King | |
2016-11-11 | Speeding up the common branches for inc(). | Tim King | |
2016-11-11 | Enable eager bitblasting for QF_ABV when no stores are present. | Clark Barrett | |
2016-11-11 | Add simple inferences for extended bitvector functions, add a few related ↵ | ajreynol | |
options. Use bv2nat, int2bv as triggers. Add regressions. | |||
2016-11-10 | Adding garbage collection of nodes with maxed out reference counts. | Tim King | |
2016-11-10 | Added PtrCloser guards for constructNodePtr. This ensures garbage collection ↵ | Tim King | |
on type checking exceptions. | |||
2016-11-10 | Add option for enabling/disabling lazy extended function reduction in ↵ | ajreynol | |
bitvectors. | |||
2016-11-09 | Renaming the class PtrCloser to not cause confusion with unique_ptr. | Tim King | |
2016-11-09 | Merge branch 'master' into uniq-ptr | Tim King | |
2016-11-09 | Fix tptp parser memory leaks for include. | ajreynol | |
2016-11-08 | Minor fixes related to ExtTheory + incremental, fixes bug760. | ajreynol | |
2016-11-08 | Add a few options to separation logic and sets. Minor changes to separation ↵ | ajreynol | |
logic, change syntax for empty heap constraint. | |||
2016-11-07 | Changing 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-07 | Fixing a memory leak in the CnfStream unit tests. | Tim King | |
2016-11-07 | Fixing a memory leak in the eager bitblaster. | Tim King | |
2016-11-06 | Adds 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-06 | This 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-04 | Fix a few more minor memory leaks. | ajreynol | |
2016-11-03 | Make data points accurate in sep logic models. | ajreynol | |
2016-11-03 | Add priorities to getNextDecision. Properly handle case for finite types + ↵ | ajreynol | |
unbounded heaps in sep logic. Fix another simple memory leak in sygus. | |||
2016-11-02 | Fix back() of empty deque in context_mm_black test | Andres 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-02 | Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵ | ajreynol | |
Fix a few more memory leaks. | |||
2016-11-02 | Fix a few obvious memory leaks in sygus and quantifiers. Minor fix cvc3_compat. | ajreynol | |
2016-11-01 | Minor fix to cvc3_compat. | ajreynol | |
2016-11-01 | Make tuple and record names unique. Do not print internal datatype ↵ | ajreynol | |
declaration in cvc printer. | |||
2016-11-01 | Fix memory leak in TheorySetsRels. Minor cleanup. | ajreynol | |
2016-11-01 | Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ | ajreynol | |
ASAN failures with datatypes should now be mostly fixed. | |||
2016-11-01 | Revert change to datatypes API for passing pointers, instead make deep copy ↵ | ajreynol | |
during call to mkMutualDatatypes. | |||
2016-11-01 | Working memory leak free version, changes interface to pointers. | ajreynol | |