summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-03-19Refactor the theory specific parts of definition expansion into the theory so...Martin Brain
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2013-12-24Minor code cleanup.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-10-09fixed options::proof() segfaultlianah
2013-09-30merged goldenLiana Hadarean
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-22Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru...Andrew Reynolds
2013-07-16fixed seg fault when bv equality is turned offLiana Hadarean
2013-07-16fixed bug520Liana Hadarean
2013-07-16Minor bugfixes to model-buildingMorgan Deters
2013-05-14added some extra options to the bit-vector theorylianah
2013-05-07added type checking rule to check for bit-vector constants of size 0lianah
2013-05-07one more fix for rewriteslianah
2013-05-07fixed bv rewrite blow-uplianah
2013-05-06fixed bv rewrite rule bugLiana Hadarean
2013-05-03changed the shifting bit-blasting to potentially be more efficientlianah
2013-05-02* splitLemma to request atomsDejan Jovanović
2013-05-02merged masterlianah
2013-05-01removed tracing code causing slowdown; cleaned up some codelianah
2013-05-01added back BitwiseEq rulelianah
2013-04-30fixed merge conflictslianah
2013-04-30merged cvc4 masterlianah
2013-04-30updated the author namelianah
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt...lianah
2013-04-30added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-30added some bv rewrite ruleslianah
2013-04-30innd examples are solved fast, but destruction assertion faillianah
2013-04-30fixed compile errorLiana Hadarean
2013-04-30uncompiling new bv to bool liftinglianah
2013-04-30finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-30more work on boolean liftingLiana Hadarean
2013-04-30started work on bv1 to boolean liftinglianah
2013-04-30updated the author namelianah
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt...lianah
2013-04-26Merge experimental decisionweight branchKshitij Bansal
2013-04-25added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-21added some bv rewrite ruleslianah
2013-04-18Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-04-17innd examples are solved fast, but destruction assertion faillianah
2013-04-16fixed compile errorLiana Hadarean
2013-04-16uncompiling new bv to bool liftinglianah
2013-04-12finished implementing bv to bool lifting and added --bv-to-bool optionlianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback