summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2014-11-17added command line option for extractArith bv rewritelianah
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-12BV inequality graph TNode fix.Morgan Deters
2014-11-12Fix BV inequality solver caching.Morgan Deters
2014-11-07Remove some unused variables.Morgan Deters
2014-11-07Fix memory issues in bitvector theory, which is now valgrind-clean (mostly re...Morgan Deters
2014-10-29Added new, much faster, care graph computation for arraysClark Barrett
2014-10-23Fixed inefficiency in bit-vector rewrite rule.lianah
2014-10-14fix for memory leak in BVQuickChecklianah
2014-09-27Merge branch '1.4.x'Morgan Deters
2014-09-27Fix infinite loop in --bitblast-aig/--bv-aig-simp options.Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Fix bv options doc.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan Deters
2014-09-03check() optimizationKshitij Bansal
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
2014-08-05fixed bug575 for bv modelslianah
2014-08-05fixed bug575 for bv modelslianah
2014-07-10Merge remote-tracking branch 'origin/master' into segfaultfixKshitij Bansal
2014-07-04initialize variablesKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback