Age | Commit message (Expand) | Author |
2012-03-26 | More cleaning up. | Dejan Jovanović |
2012-03-25 | sat_module.h,cpp -> sat_solver.h,cpp (as intended) | Dejan Jovanović |
2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean |
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
2012-02-29 | This should fix the debian build fails: | Liana Hadarean |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2012-02-20 | portfolio merge | Morgan Deters |
2011-12-08 | Disable a BV rewriter statistic (after checking with Liana) that was static, | Morgan Deters |
2011-11-01 | Improvements to header installation on user machines. Internally, we can | Morgan Deters |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-10-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-28 | variety of visibility fixes (should clean up some of the many warnings on Mac... | Morgan Deters |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-08-27 | Removing Theory::registerTerm() as discussed in the meeting. Now pre-register... | Dejan Jovanović |
2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
2011-05-02 | updates for bitvectors | Dejan Jovanović |
2011-04-25 | Weekend work. The main points: | Morgan Deters |
2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
2011-03-26 | fix for bug 253, was propagating an asserted literal | Dejan Jovanović |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-03-22 | updating debug output usage to eliviate impact of bug 252 | Dejan Jovanović |
2011-03-21 | more bugfixes, some basic propagation, and testcases to cover them | Dejan Jovanović |
2011-03-21 | fixing a bug in the BV rewrite, off by one error when merging constants | Dejan Jovanović |
2011-03-20 | again a typo | Dejan Jovanović |
2011-03-20 | more bugfixes for bitvectors | Dejan Jovanović |
2011-03-20 | fixing the failure from last nigth, due to using a reference to an element in... | Dejan Jovanović |
2011-03-20 | missed one case | Dejan Jovanović |
2011-03-20 | commit for the version of bitvectors that passes all the unit tests | Dejan Jovanović |
2011-02-26 | Commit to fix bug 241 (improper "using namespace std" in a header). This cau... | Morgan Deters |
2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
2011-02-26 | adding the variables count to the statistics in the expr manager | Dejan Jovanović |
2011-02-25 | slicing manager is not breaking the old regressions, time to sync | Dejan Jovanović |
2011-02-17 | getting ready for slicing bitvectors | Dejan Jovanović |
2011-02-16 | updates for the rewriter, added some statistics | Dejan Jovanović |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-11-16 | Added Theory::presolve(). | Tim King |
2010-11-15 | Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer | Morgan Deters |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ... | Morgan Deters |
2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti... | Morgan Deters |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-09-24 | equality triggers for the equality engine | Dejan Jovanović |
2010-09-24 | basic union find for bitvectors | Dejan Jovanović |
2010-09-20 | bitvector rewriting for the core theory and testcases | Dejan Jovanović |
2010-07-27 | Adding optional 'check' parameter to getType() methods | Christopher L. Conway |
2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett |
2010-07-04 | enable arrays | Morgan Deters |
2010-07-03 | With this commit come a number of changes to build system to support | Morgan Deters |