summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2014-06-22Merge pull request #39 from mdeters/bv-warningslianah
2014-06-22Merge pull request #35 from mdeters/bv-kindslianah
2014-06-21Fix compiler warnings in BV-related code (unused vars mostly).Morgan Deters
2014-06-21fixed build failurelianah
2014-06-20Bit-vector kinds documentationMorgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19Fix compile errors with some versions of GCC.Morgan Deters
2014-06-19Minor fixes, spelling etc.Morgan Deters
2014-06-15core solver fixlianah
2014-06-15fixed bv bug due to applying equisatisfiable transformations in ppRewritelianah
2014-06-15fixed fuzzer assertion failures for bvlianah
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback