summaryrefslogtreecommitdiff
path: root/src/theory/bv/Makefile.am
AgeCommit message (Expand)Author
2012-12-10ported my bv-core branch from svn to gitLiana Hadarean
2012-07-31Options merge. This commit:Morgan Deters
2012-07-14Type enumerator infrastructure and uninterpreted constant support. No suppor...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-15renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectivelyLiana 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-02-25slicing manager is not breaking the old regressions, time to syncDejan Jovanović
2011-02-17getting ready for slicing bitvectorsDejan Jovanović
2011-02-16updates for the rewriter, added some statisticsDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-09-24basic union find for bitvectorsDejan Jovanović
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-06-15fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)Morgan Deters
2010-06-15remove warnings about unknown #pragma GCC diagnostic on older compilersMorgan Deters
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback