Age | Commit message (Expand) | Author |
2012-05-16 | equality status for bitvectors can now look into the sat solver to check for ... | Dejan Jovanović |
2012-05-16 | refactored TheoryBV bitblaster and equality engine into subtheories (similar ... | Liana Hadarean |
2012-05-15 | fixed QF_BV performance problem due to using CDList instead of CDQueue | Liana Hadarean |
2012-05-15 | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively | Liana Hadarean |
2012-05-15 | fixing warnings, grr | Dejan Jovanović |
2012-05-15 | several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a... | Liana Hadarean |
2012-05-13 | fixing build warnings | Dejan Jovanović |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
2012-04-11 | merge from arrays-clark branch | Morgan Deters |
2012-04-06 | processing assertions in bit-vectors even when in fullcheck (needed for sharing) | Dejan Jovanović |
2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean |
2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-08-27 | Removing Theory::registerTerm() as discussed in the meeting. Now pre-register... | Dejan Jovanović |
2011-05-02 | updates for bitvectors | Dejan Jovanović |
2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
2011-03-26 | fix for bug 253, was propagating an asserted literal | Dejan Jovanović |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-03-22 | updating debug output usage to eliviate impact of bug 252 | Dejan Jovanović |
2011-03-21 | more bugfixes, some basic propagation, and testcases to cover them | Dejan Jovanović |
2011-03-20 | more bugfixes for bitvectors | Dejan Jovanović |
2011-03-20 | commit for the version of bitvectors that passes all the unit tests | Dejan Jovanović |
2011-02-26 | Commit to fix bug 241 (improper "using namespace std" in a header). This cau... | Morgan Deters |
2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
2011-02-25 | slicing manager is not breaking the old regressions, time to sync | Dejan Jovanović |
2011-02-17 | getting ready for slicing bitvectors | Dejan Jovanović |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-09-24 | equality triggers for the equality engine | Dejan Jovanović |
2010-09-24 | basic union find for bitvectors | Dejan Jovanović |
2010-09-20 | bitvector rewriting for the core theory and testcases | Dejan Jovanović |