summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Expand)Author
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
2013-02-01merged master into branchlianah
2013-02-01minor changes.lianah
2013-01-31done fixing slicer bugs.lianah
2013-01-30fixed some more bugslianah
2013-01-29fixing slicer bugs.Liana Hadarean
2013-01-29fixeslianah
2013-01-28compiling implementation of new slicer finished; need to add debugging inform...lianah
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-25starting the slicer form scratch.lianah
2013-01-25minor changes trying to optimize the slicing codelianah
2013-01-14fixed more minor bugslianah
2013-01-10fixed most bugs and added paranoid assertionslianah
2013-01-10minor bug fixesLiana Hadarean
2013-01-10slicer bug fixingLiana Hadarean
2012-12-13more slicer bug fixeslianah
2012-12-12Merge pull request #2 from CVC4/1.0.xDejan Jovanović
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
2012-12-11fixed some slicer bugs; set up bv theory to run bit-blaster to check for corr...Liana Hadarean
2012-12-10ported my bv-core branch from svn to gitLiana Hadarean
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ...Tim King
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
2012-11-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
2012-11-13fixed failed bv regressions by refactoring out some rewrite rules from smt_en...Liana Hadarean
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-10-23fixed TheoryBV collectModel info to check for shared terms; this seems to fix...Liana Hadarean
2012-10-19BV theory model fixLiana Hadarean
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-09fixed bv rewriter to evaluate bvurem over constantsLiana Hadarean
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-03implemented collectModelInfo for TheoryBVLiana Hadarean
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-29* Numerous documentation fixes (fix doxygen warnings, add missing documentati...Morgan Deters
2012-08-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-08-01add isFinished() to type enumerators (so we don't rely on exception-throwing ...Morgan Deters
2012-08-01some fixes for Mac OSMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback