| Age | Commit message (Expand) | Author |
|---|
| 2013-03-19 | inequality reasoning works on small examples added to regressions (not increm... | Liana Hadarean |
| 2013-03-16 | started work on the inequality bv subtheory | lianah |
| 2013-03-13 | post failed attempts at getting the incremental solver to work | lianah |
| 2013-03-06 | more slicer changes for incremental | lianah |
| 2013-02-26 | Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x | lianah |
| 2013-02-26 | fix for bv crash in incremental mode; this is a temporary fix for bug 493 | lianah |
| 2013-02-14 | Removing BVDebug and replacing with Debug. | Tim King |
| 2013-02-04 | Fixing regression failure. The only unfixed ones seem model related which wou... | lianah |
| 2013-01-31 | done fixing slicer bugs. | lianah |
| 2013-01-28 | compiling implementation of new slicer finished; need to add debugging inform... | lianah |
| 2013-01-14 | fixed more minor bugs | lianah |
| 2013-01-10 | fixed most bugs and added paranoid assertions | lianah |
| 2013-01-10 | minor bug fixes | Liana Hadarean |
| 2012-12-11 | fixed some slicer bugs; set up bv theory to run bit-blaster to check for corr... | Liana Hadarean |
| 2012-12-10 | ported my bv-core branch from svn to git | Liana Hadarean |
| 2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
| 2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
| 2012-10-03 | implemented collectModelInfo for TheoryBV | Liana Hadarean |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-06-14 | fix for clark's bug | Dejan Jovanović |
| 2012-06-12 | Changed bitvector theory rewriter so that equalities always get rewritten to | Clark Barrett |
| 2012-06-11 | fixing bitvector bugs | Dejan Jovanović |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
| 2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett |
| 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 |
