summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2014-06-14added rewriting to bv-pow2 passlianah
2014-06-14Evil bitvector preprocessing pass for simplifying powers of two.lianah
2014-06-14bv static learning and rewrites for power of 2 termslianah
2014-06-14more bv rewriteslianah
2014-06-14fix to inequality rewritelianah
2014-06-14added bv inequality rewritelianah
2014-06-14added bv inequality lemmasLiana Hadarean
2014-06-12Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2014-06-12fixing bv inequality solver explanation buglianah
2014-06-12added bvcomp case to bv to bool liftinglianah
2014-06-11added optionException for trying to use abc in an non-abc buildlianah
2014-06-11switched bv equality orderlianah
2014-06-11fixed unit tests failureslianah
2014-06-11fixing bv ackermanization cache buglianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback