summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
2013-04-01fixed bug 502; now the core bv solver only gives the model for variables and ...lianah
2013-03-30changed option to run inequality solver by defaultLiana Hadarean
2013-03-27Added assertionClark Barrett
2013-03-27Updates to model-based array solverClark Barrett
2013-03-27reverted the core solver to do static slicing, added option --bv-core-solverlianah
2013-03-27fixed inequality checkDisequalities inefficiencylianah
2013-03-27fixed some model stufflianah
2013-03-27fixed model generation bug; commented out attempt at inequality propagationlianah
2013-03-26inequality solver now only splits on disequalities when completelianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26core theory currently disabledlianah
2013-03-26getModelValue implementation in bitvectorsDejan Jovanović
2013-03-26addingDejan Jovanović
2013-03-26fixed inequality bugs due to improper explanationlianah
2013-03-25cleaned up the bv subtheory interface; added check for inequality theory comp...lianah
2013-03-25getEqualityStatus now also queries the inequality solverlianah
2013-03-24added support for disequalities in the inequality solverLiana Hadarean
2013-03-24incremental inequality solver implementedlianah
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-23fixed some explanation problems for the core theory; still slowlianah
2013-03-21fixed more equality stufflianah
2013-03-21fixed compilation problemlianah
2013-03-21incorporated dejan's constant evaluation; now getting destruction seg faultlianah
2013-03-21disabled ineqlianah
2013-03-21added regression test for constant evallianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19merged dejan's stuffLiana Hadarean
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-19Adding evaluation of constant terms to the equality engine. Evaluation on a p...Dejan Jovanović
2013-03-19added the cpp file for the inequality graphLiana Hadarean
2013-03-19implementing more inequality graph stuff; work in progress doesn't compileLiana Hadarean
2013-03-18more work on inequality reasoning for bvlianah
2013-03-16started work on the inequality bv subtheorylianah
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-03-13post failed attempts at getting the incremental solver to worklianah
2013-03-06more slicer changes for incrementallianah
2013-02-26Merge branch '1.0.x'lianah
2013-02-26Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.xlianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-15Merge branch '1.0.x'Tim King
2013-02-14Removing BVDebug and replacing with Debug.Tim King
2013-02-13started working on incremental slicer - not compilinglianah
2013-02-11undid the caching that actually hurt performancelianah
2013-02-05Added path compression and caching for getBaseDecomposition.Liana Hadarean
2013-02-04Fixing regression failure. The only unfixed ones seem model related which wou...lianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback