| Age | Commit message (Expand) | Author |
|---|
| 2013-05-02 | * splitLemma to request atoms | Dejan Jovanović |
| 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 | updated the author name | 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 | innd examples are solved fast, but destruction assertion fail | lianah |
| 2013-04-30 | fixed compile error | Liana Hadarean |
| 2013-04-30 | uncompiling new bv to bool lifting | lianah |
| 2013-04-30 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
| 2013-04-30 | more work on boolean lifting | Liana Hadarean |
| 2013-04-30 | started work on bv1 to boolean lifting | lianah |
| 2013-04-30 | updated the author name | 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-18 | Merge branch 'master' of https://github.com/CVC4/CVC4 | lianah |
| 2013-04-17 | innd examples are solved fast, but destruction assertion fail | lianah |
| 2013-04-16 | fixed compile error | Liana Hadarean |
| 2013-04-16 | uncompiling new bv to bool lifting | lianah |
| 2013-04-12 | finished implementing bv to bool lifting and added --bv-to-bool option | lianah |
| 2013-04-11 | Fixes for getModelVal in bv theory | Clark Barrett |
| 2013-04-10 | fixed getModelValue to only query the value of leaves and evaluate more compl... | lianah |
| 2013-04-10 | more work on boolean lifting | Liana Hadarean |
| 2013-04-09 | started work on bv1 to boolean lifting | 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-04-01 | Merging some cleanup work: | Morgan Deters |
| 2013-04-01 | fixed bug 502; now the core bv solver only gives the model for variables and ... | lianah |
| 2013-03-30 | changed option to run inequality solver by default | Liana Hadarean |
| 2013-03-27 | Added assertion | Clark Barrett |
| 2013-03-27 | Updates to model-based array solver | Clark Barrett |
| 2013-03-27 | reverted the core solver to do static slicing, added option --bv-core-solver | lianah |
| 2013-03-27 | fixed inequality checkDisequalities inefficiency | lianah |
| 2013-03-27 | fixed some model stuff | lianah |
| 2013-03-27 | fixed model generation bug; commented out attempt at inequality propagation | lianah |
| 2013-03-26 | inequality solver now only splits on disequalities when complete | lianah |
| 2013-03-26 | added model generation for bv subtheories and bv-inequality solver option | lianah |
| 2013-03-26 | core theory currently disabled | lianah |
| 2013-03-26 | getModelValue implementation in bitvectors | Dejan Jovanović |
| 2013-03-26 | adding | 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 |
