Age | Commit message (Expand) | Author |
2016-04-20 | update from the master | PaulMeng |
2016-01-28 | Adding listeners to Options. | Tim King |
2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
2016-01-05 | Add SmtGlobals Class | Tim King |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-05-29 | changed resource step options to unsigned | lianah |
2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean |
2015-04-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
2014-11-17 | Resource-limiting work. | Liana Hadarean |
2014-11-07 | Fix memory issues in bitvector theory, which is now valgrind-clean (mostly re... | Morgan Deters |
2014-09-03 | check() optimization | Kshitij Bansal |
2014-08-18 | Making getEqualityStatus more powerful for bit-vector theory. | lianah |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-06-19 | added model generation to eager bit-blasting and turned abc off by default | lianah |
2014-06-15 | fixed bv bug due to applying equisatisfiable transformations in ppRewrite | lianah |
2014-06-14 | Evil bitvector preprocessing pass for simplifying powers of two. | lianah |
2014-06-14 | bv static learning and rewrites for power of 2 terms | lianah |
2014-06-14 | more bv rewrites | lianah |
2014-06-14 | added bv inequality rewrite | lianah |
2014-06-11 | fixing bv ackermanization cache bug | lianah |
2014-06-10 | Merging CAV14 paper bit-vector work. | lianah |
2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after final... | Morgan Deters |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-11-27 | General pre-release cleanup commit | Morgan Deters |
2013-09-30 | merged golden | Liana Hadarean |
2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
2013-07-16 | fixed seg fault when bv equality is turned off | Liana Hadarean |
2013-05-14 | added some extra options to the bit-vector theory | lianah |
2013-05-03 | changed the shifting bit-blasting to potentially be more efficient | lianah |
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 |