Age | Commit message (Expand) | Author |
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-24 | Minor code cleanup. | 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-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
2013-10-09 | fixed options::proof() segfault | lianah |
2013-09-30 | merged golden | Liana Hadarean |
2013-09-24 | Reduce compiler dependencies on substitutions.h, | Clark Barrett |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
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-07-16 | fixed bug520 | Liana Hadarean |
2013-07-16 | Minor bugfixes to model-building | Morgan Deters |
2013-05-14 | added some extra options to the bit-vector theory | lianah |
2013-05-07 | added type checking rule to check for bit-vector constants of size 0 | lianah |
2013-05-07 | one more fix for rewrites | lianah |
2013-05-07 | fixed bv rewrite blow-up | lianah |
2013-05-06 | fixed bv rewrite rule bug | Liana Hadarean |
2013-05-03 | changed the shifting bit-blasting to potentially be more efficient | lianah |
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 |