Age | Commit message (Expand) | Author |
2013-05-02 | merged master | lianah |
2013-04-30 | added bvule, bvsle operator elimination rulesl; added bvurem lemma generation | lianah |
2013-04-26 | Merge experimental decisionweight branch | Kshitij Bansal |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-03-27 | fixed model generation bug; commented out attempt at inequality propagation | lianah |
2013-03-26 | added model generation for bv subtheories and bv-inequality solver option | lianah |
2013-03-26 | getModelValue implementation in bitvectors | Dejan Jovanović |
2013-03-25 | cleaned up the bv subtheory interface; added check for inequality theory comp... | lianah |
2013-03-24 | added support for disequalities in the inequality solver | Liana Hadarean |
2013-03-19 | inequality reasoning works on small examples added to regressions (not increm... | Liana Hadarean |
2013-03-18 | more work on inequality reasoning for bv | lianah |
2013-03-16 | started work on the inequality bv subtheory | lianah |
2013-03-13 | post failed attempts at getting the incremental solver to work | lianah |
2013-02-04 | Fixing regression failure. The only unfixed ones seem model related which wou... | lianah |
2012-12-10 | ported my bv-core branch from svn to git | Liana Hadarean |
2012-12-05 | This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ... | Tim King |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
2012-06-12 | Changed bitvector theory rewriter so that equalities always get rewritten to | Clark Barrett |
2012-06-11 | fixing bitvector bugs | Dejan Jovanović |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović |
2012-05-16 | refactored TheoryBV bitblaster and equality engine into subtheories (similar ... | Liana Hadarean |
2012-05-15 | fixed QF_BV performance problem due to using CDList instead of CDQueue | Liana Hadarean |
2012-05-15 | several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a... | Liana Hadarean |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
2012-04-11 | merge from arrays-clark branch | Morgan Deters |
2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean |
2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
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-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-03-21 | more bugfixes, some basic propagation, and testcases to cover them | Dejan Jovanović |
2011-03-20 | more bugfixes for bitvectors | 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 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
2011-02-25 | slicing manager is not breaking the old regressions, time to sync | Dejan Jovanović |