| 2012-07-08 |
Morgan Deters | another signed-ness warning fix for newer GCC |
tree | commitdiff |
| 2012-07-08 |
Morgan Deters | Minor changes to avoid some warnings on GCC 4.7.1 ... |
tree | commitdiff |
| 2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
tree | commitdiff |
| 2012-07-07 |
Morgan Deters | Various fixes to documentation---typos, some incomplete... |
tree | commitdiff |
| 2012-07-06 |
Tim King | Adding std namespace to a couple of make_pair instances. |
tree | commitdiff |
| 2012-07-06 |
Tim King | Added virtual destructor to PpRewrite. |
tree | commitdiff |
| 2012-06-28 |
Clark Barrett | Fixed bug in bv rewriter that caused wrong answer in... |
tree | commitdiff |
| 2012-06-27 |
Tim King | Fixing a bug in proof production for the DioSolver. |
tree | commitdiff |
| 2012-06-27 |
Tim King | This adds TheoryArith::safeToReset(). This fixes bug... |
tree | commitdiff |
| 2012-06-27 |
Tim King | Adding access to simplex's ArithPriorityQueue to Theory... |
tree | commitdiff |
| 2012-06-27 |
Tim King | Improved debugging output. |
tree | commitdiff |
| 2012-06-27 |
Tim King | Improved debugging output. |
tree | commitdiff |
| 2012-06-27 |
Tim King | Adding reduce() to the ArithPriorityQueue. This reduces... |
tree | commitdiff |
| 2012-06-25 |
Tim King | Added a warning to arithmetic for a known dio solver... |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Reverting buggy rewriter code |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Fixed bug in rewriter |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Fix for slow array rewrite and minor bug fix in arrays... |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | small bug fix and performance fix in ite simplifier |
tree | commitdiff |
| 2012-06-17 |
Dejan Jovanović | fixing wrong assertion |
tree | commitdiff |
| 2012-06-17 |
Clark Barrett | Fix array bug causing incorrect answers |
tree | commitdiff |
| 2012-06-16 |
Dejan Jovanović | small change to equality assertions so that one doesn... |
tree | commitdiff |
| 2012-06-16 |
Kshitij Bansal | This is an attempt to fix the bug in the justification... |
tree | commitdiff |
| 2012-06-16 |
Dejan Jovanović | changing theoryOf in shared mode with arrays to move... |
tree | commitdiff |
| 2012-06-16 |
Tim King | Fixing if condition for trivial equalities in arithmeti... |
tree | commitdiff |
| 2012-06-15 |
Clark Barrett | Reverting rewrite rule to working version |
tree | commitdiff |
| 2012-06-15 |
Clark Barrett | Fixes some assertion failures |
tree | commitdiff |
| 2012-06-15 |
Clark Barrett | Fix for incompleteness bug with decision engine: repeat... |
tree | commitdiff |
| 2012-06-15 |
Tim King | Fixing mac compilation issues. |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | fixing the problems with the bvminisat. there was a... |
tree | commitdiff |
| 2012-06-14 |
Tim King | Fixing a case for explanation of non-normal form equali... |
tree | commitdiff |
| 2012-06-14 |
Tim King | Fixing a bug related to explaining propagations with... |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | fixes for the hasTerm issues in the shared database... |
tree | commitdiff |
| 2012-06-14 |
Clark Barrett | New substitutions implementation - fixes performance... |
tree | commitdiff |
| 2012-06-14 |
Tim King | Fixed arithmetic consistency issue. The simplex confli... |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | fix for clark's bug |
tree | commitdiff |
| 2012-06-14 |
Kshitij Bansal | fix quantifier non-bug |
tree | commitdiff |
| 2012-06-14 |
Clark Barrett | Removed an assertion, unneeded header file |
tree | commitdiff |
| 2012-06-14 |
Morgan Deters | The "no-tears-in-competition-mode" commit. Change... |
tree | commitdiff |
| 2012-06-14 |
Kshitij Bansal | fix cout, fix statname, rm deadcode |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | changing to a more natural propagation order in uf... |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | some changes to the uf engine |
tree | commitdiff |
| 2012-06-14 |
Tim King | Brings the tuning branch into trunk. This includes... |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | * removing rewriteEquality from the rewriter |
tree | commitdiff |
| 2012-06-13 |
Tim King | Added witnesses to Constraints. |
tree | commitdiff |
| 2012-06-13 |
Tim King | - Added a loop to internally assert constraints that... |
tree | commitdiff |
| 2012-06-13 |
Tim King | Adds debugging output to theory_engine.cpp. |
tree | commitdiff |
| 2012-06-13 |
Dejan Jovanović | fix for bug 354 |
tree | commitdiff |
| 2012-06-13 |
Clark Barrett | Fixed failing assertion when EqualityEngine is in conflict |
tree | commitdiff |
| 2012-06-13 |
Clark Barrett | Fixed definition of bvsmod |
tree | commitdiff |
| 2012-06-13 |
Clark Barrett | Fixes more problems in bv rewrites |
tree | commitdiff |
| 2012-06-13 |
Clark Barrett | Fixes lots of problems in bv rewrite rules and adds... |
tree | commitdiff |
| 2012-06-12 |
Morgan Deters | Fix some compile warnings (but they never showed up... |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Fixed fuzzing bug |
tree | commitdiff |
| 2012-06-12 |
Tim King | Fix to yesterday's change in arithmetic. |
tree | commitdiff |
| 2012-06-12 |
Dejan Jovanović | bufixes and the bugs |
tree | commitdiff |
| 2012-06-12 |
Dejan Jovanović | conflicts from theories are removable |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Changed bitvector theory rewriter so that equalities... |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt... |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Fixed failing assertion in arrays for bug 347 |
tree | commitdiff |
| 2012-06-12 |
Morgan Deters | minor cleanup, and replace a "private:" in equality... |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Adding constant propagation code - needs more testing... |
tree | commitdiff |
| 2012-06-11 |
Tim King | Fix to term normalization of integer equalities. Adds... |
tree | commitdiff |
| 2012-06-11 |
Tim King | Fixing type comparision assertion in getEqualityStatus(). |
tree | commitdiff |
| 2012-06-11 |
Dejan Jovanović | fixing bitvector bugs |
tree | commitdiff |
| 2012-06-11 |
Morgan Deters | mark a quantifiers global var as "static" so we can... |
tree | commitdiff |
| 2012-06-11 |
Clark Barrett | OK, now the rewrite issues are fixed |
tree | commitdiff |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
tree | commitdiff |
| 2012-06-11 |
Clark Barrett | Fix for array bug with decision heuristic |
tree | commitdiff |
| 2012-06-11 |
Clark Barrett | Fixed bug 352 |
tree | commitdiff |
| 2012-06-10 |
Clark Barrett | Fixed one more bug in rewriter |
tree | commitdiff |
| 2012-06-10 |
Clark Barrett | Added a very fruitful assertion to the rewriter: checks... |
tree | commitdiff |
| 2012-06-10 |
Dejan Jovanović | adding an assertion to trigger the problem of bug349... |
tree | commitdiff |
| 2012-06-10 |
Dejan Jovanović | fixes for bug347 |
tree | commitdiff |
| 2012-06-09 |
Morgan Deters | Dagification of output expressions. |
tree | commitdiff |
| 2012-06-07 |
Dejan Jovanović | fixing the wrong results. arrays equality adaptor had... |
tree | commitdiff |
| 2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization... |
tree | commitdiff |
| 2012-06-07 |
Clark Barrett | Fixed performance issue with ite_simplifier on some... |
tree | commitdiff |
| 2012-06-07 |
Dejan Jovanović | fixing some bugs in propagation of disequalities |
tree | commitdiff |
| 2012-06-06 |
Clark Barrett | Fixed assertion failures |
tree | commitdiff |
| 2012-06-06 |
Dejan Jovanović | disabling a super-expensive assertions to speed up... |
tree | commitdiff |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
tree | commitdiff |
| 2012-06-06 |
Clark Barrett | Fixed problem causing crash at destruction time |
tree | commitdiff |
| 2012-06-05 |
Clark Barrett | More clean-up |
tree | commitdiff |
| 2012-06-05 |
Clark Barrett | Fixed a performance issue with unconstrained simplifier |
tree | commitdiff |
| 2012-06-05 |
Clark Barrett | Adding missing files... |
tree | commitdiff |
| 2012-06-04 |
Clark Barrett | Added preprocessing pass that propagates unconstrained... |
tree | commitdiff |
| 2012-05-31 |
Clark Barrett | Fixed bug in bv: one more case where non-shared equalit... |
tree | commitdiff |
| 2012-05-30 |
Clark Barrett | Added BitwiseEq bitvector rewrite |
tree | commitdiff |
| 2012-05-30 |
Clark Barrett | Fixed problem with array queue growing too large |
tree | commitdiff |
| 2012-05-30 |
Morgan Deters | remove unused/broken check build target |
tree | commitdiff |
| 2012-05-29 |
Morgan Deters | removing now-unused TheoryEngine::setLogic() interface... |
tree | commitdiff |
| 2012-05-29 |
Clark Barrett | Enabled SolveEq bv rewrite |
tree | commitdiff |
| 2012-05-28 |
Clark Barrett | Added some BV rewrites, fixed bugs in array theory... |
tree | commitdiff |
| 2012-05-27 |
Dejan Jovanović | some reordering to keep invariants |
tree | commitdiff |
| 2012-05-27 |
Dejan Jovanović | Committing the work on equality engine, I need to see... |
tree | commitdiff |
| 2012-05-27 |
Clark Barrett | Another expensive function call in a Debug line |
tree | commitdiff |
| 2012-05-25 |
Kshitij Bansal | init bug fix |
tree | commitdiff |
| 2012-05-25 |
Clark Barrett | Checking in fix for bug 340 - somehow didn't get checke... |
tree | commitdiff |
| 2012-05-24 |
Dejan Jovanović | Separating the subtheory implementations in the bitvect... |
tree | commitdiff |
| 2012-05-24 |
Dejan Jovanović | Significant changes to the internals of the equality... |
tree | commitdiff |
| next |
projects / cvc5.git / history