Age | Commit message (Expand) | Author |
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
2012-06-13 | Fixed definition of bvsmod | Clark Barrett |
2012-06-13 | Fixes more problems in bv rewrites | Clark Barrett |
2012-06-13 | Fixes lots of problems in bv rewrite rules and adds lots of assertions | Clark Barrett |
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 | OK, now the rewrite issues are fixed | Clark Barrett |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-11 | Fix for array bug with decision heuristic | Clark Barrett |
2012-06-10 | Fixed one more bug in rewriter | Clark Barrett |
2012-06-10 | Added a very fruitful assertion to the rewriter: checks that rewriting after ... | Clark Barrett |
2012-06-10 | fixes for bug347 | Dejan Jovanović |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
2012-05-31 | Fixed bug in bv: one more case where non-shared equality was getting propagated | Clark Barrett |
2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett |
2012-05-29 | Enabled SolveEq bv rewrite | Clark Barrett |
2012-05-28 | Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV | Clark Barrett |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the regr... | Dejan Jovanović |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-17 | Fixed bug 338: | Liana Hadarean |
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-29 | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers... | Tim King |
2012-03-28 | fixed faulty bv rewrite rule | Liana Hadarean |
2012-03-26 | More cleaning up. | Dejan Jovanović |
2012-03-25 | sat_module.h,cpp -> sat_solver.h,cpp (as intended) | Dejan Jovanović |
2012-03-22 | Merged updated version of the bitvector theory: | Liana Hadarean |
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
2012-02-29 | This should fix the debian build fails: | Liana Hadarean |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2012-02-20 | portfolio merge | Morgan Deters |
2011-12-08 | Disable a BV rewriter statistic (after checking with Liana) that was static, | Morgan Deters |
2011-11-01 | Improvements to header installation on user machines. Internally, we can | Morgan Deters |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-10-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-28 | variety of visibility fixes (should clean up some of the many warnings on Mac... | Morgan Deters |