summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.h
AgeCommit message (Expand)Author
2014-08-18Making getEqualityStatus more powerful for bit-vector theory.lianah
2014-07-01Update copyrights.Morgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19Minor fixes, spelling etc.Morgan Deters
2014-06-14Evil bitvector preprocessing pass for simplifying powers of two.lianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
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-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-05-02merged masterlianah
2013-04-30added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-26Merge experimental decisionweight branchKshitij Bansal
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-27fixed model generation bug; commented out attempt at inequality propagationlianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26getModelValue implementation in bitvectorsDejan Jovanović
2013-03-25cleaned up the bv subtheory interface; added check for inequality theory comp...lianah
2013-03-24added support for disequalities in the inequality solverLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-18more work on inequality reasoning for bvlianah
2013-03-16started work on the inequality bv subtheorylianah
2013-03-13post failed attempts at getting the incremental solver to worklianah
2013-02-04Fixing regression failure. The only unfixed ones seem model related which wou...lianah
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-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-13Fixes lots of problems in bv rewrite rules and adds lots of assertionsClark Barrett
2012-06-12Changed bitvector theory rewriter so that equalities always get rewritten toClark Barrett
2012-06-11fixing bitvector bugsDejan Jovanović
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-05-24Separating the subtheory implementations in the bitvector theory.Dejan Jovanović
2012-05-16refactored TheoryBV bitblaster and equality engine into subtheories (similar ...Liana Hadarean
2012-05-15fixed QF_BV performance problem due to using CDList instead of CDQueueLiana Hadarean
2012-05-15several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a...Liana Hadarean
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback