| Age | Commit message (Expand) | Author |
|---|
| 2013-05-02 | merged master | lianah |
| 2013-05-01 | removed tracing code causing slowdown; cleaned up some code | lianah |
| 2013-05-01 | added back BitwiseEq rule | lianah |
| 2013-04-30 | fixed merge conflicts | lianah |
| 2013-04-30 | merged cvc4 master | lianah |
| 2013-04-30 | added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt... | lianah |
| 2013-04-30 | added bvule, bvsle operator elimination rulesl; added bvurem lemma generation | lianah |
| 2013-04-30 | added some bv rewrite rules | lianah |
| 2013-04-30 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
| 2013-04-30 | added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt... | lianah |
| 2013-04-26 | Merge experimental decisionweight branch | Kshitij Bansal |
| 2013-04-25 | added bvule, bvsle operator elimination rulesl; added bvurem lemma generation | lianah |
| 2013-04-21 | added some bv rewrite rules | lianah |
| 2013-04-12 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
| 2013-04-03 | * changing the bitblast-eager to bitblast on pre-register | Dejan Jovanović |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-27 | reverted the core solver to do static slicing, added option --bv-core-solver | lianah |
| 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-26 | fixed inequality bugs due to improper explanation | lianah |
| 2013-03-25 | cleaned up the bv subtheory interface; added check for inequality theory comp... | lianah |
| 2013-03-25 | getEqualityStatus now also queries the inequality solver | lianah |
| 2013-03-23 | non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing) | lianah |
| 2013-03-21 | disabled ineq | lianah |
| 2013-03-21 | added regression test for constant eval | lianah |
| 2013-03-20 | generalized bv inequality reasoning to handle both strict and non-strict ineq... | lianah |
| 2013-03-19 | fixed reversed concat in core theory | Liana Hadarean |
| 2013-03-19 | inequality reasoning works on small examples added to regressions (not increm... | Liana Hadarean |
| 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-03-06 | more slicer changes for incremental | lianah |
| 2013-02-26 | Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x | lianah |
| 2013-02-26 | fix for bv crash in incremental mode; this is a temporary fix for bug 493 | lianah |
| 2013-02-14 | Removing BVDebug and replacing with Debug. | Tim King |
| 2013-02-04 | Fixing regression failure. The only unfixed ones seem model related which wou... | lianah |
| 2013-01-31 | done fixing slicer bugs. | lianah |
| 2013-01-28 | compiling implementation of new slicer finished; need to add debugging inform... | lianah |
| 2013-01-14 | fixed more minor bugs | lianah |
| 2013-01-10 | fixed most bugs and added paranoid assertions | lianah |
| 2013-01-10 | minor bug fixes | Liana Hadarean |
| 2012-12-11 | fixed some slicer bugs; set up bv theory to run bit-blaster to check for corr... | Liana Hadarean |
| 2012-12-10 | ported my bv-core branch from svn to git | Liana Hadarean |
| 2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
| 2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
| 2012-10-03 | implemented collectModelInfo for TheoryBV | Liana Hadarean |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
