| 2012-06-18 |
Clark Barrett | Fix for slow array rewrite and minor bug fix in arrays... |
commit | commitdiff | tree |
| 2012-06-18 |
Clark Barrett | small bug fix and performance fix in ite simplifier |
commit | commitdiff | tree |
| 2012-06-18 |
Andrew Reynolds | fixed smt version 1 parser for quantifiers |
commit | commitdiff | tree |
| 2012-06-18 |
Kshitij Bansal | tracing code to make sure decision options are being... |
commit | commitdiff | tree |
| 2012-06-18 |
Kshitij Bansal | bugfix, enable only QF_LRA, not other arith |
commit | commitdiff | tree |
| 2012-06-18 |
Kshitij Bansal | QF_LRA, Quantifiers: enable use decision for (only... |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | Fixing bug 360. The driver wasn't exiting when there... |
commit | commitdiff | tree |
| 2012-06-17 |
Kshitij Bansal | QF_AUFLIA: enable use decision for (only for) stopping... |
commit | commitdiff | tree |
| 2012-06-17 |
Dejan Jovanović | fixing a problem due to lemmas produced while backtracking |
commit | commitdiff | tree |
| 2012-06-17 |
Kshitij Bansal | --decision=justification-stoponly : use decision engine... |
commit | commitdiff | tree |
| 2012-06-17 |
Dejan Jovanović | enabling theoryof=term for quantifiers with sharing |
commit | commitdiff | tree |
| 2012-06-17 |
Dejan Jovanović | fixing wrong assertion |
commit | commitdiff | tree |
| 2012-06-17 |
Clark Barrett | Removed assertion that can fail |
commit | commitdiff | tree |
| 2012-06-17 |
Dejan Jovanović | fixing makefile error that brakes build |
commit | commitdiff | tree |
| 2012-06-17 |
Clark Barrett | Fix array bug causing incorrect answers |
commit | commitdiff | tree |
| 2012-06-16 |
Dejan Jovanović | small change to equality assertions so that one doesn... |
commit | commitdiff | tree |
| 2012-06-16 |
Kshitij Bansal | Adding the failing QF_AUFLIA regression mentioned in... |
commit | commitdiff | tree |
| 2012-06-16 |
Kshitij Bansal | This is an attempt to fix the bug in the justification... |
commit | commitdiff | tree |
| 2012-06-16 |
Morgan Deters | updated build script for smt-comp submission |
commit | commitdiff | tree |
| 2012-06-16 |
Dejan Jovanović | changing theoryOf in shared mode with arrays to move... |
commit | commitdiff | tree |
| 2012-06-16 |
Tim King | Fixing if condition for trivial equalities in arithmeti... |
commit | commitdiff | tree |
| 2012-06-15 |
Kshitij Bansal | Bug fix in justification heuristic. Had to do with how |
commit | commitdiff | tree |
| 2012-06-15 |
Clark Barrett | Reverting rewrite rule to working version |
commit | commitdiff | tree |
| 2012-06-15 |
Clark Barrett | Fixes some assertion failures |
commit | commitdiff | tree |
| 2012-06-15 |
Clark Barrett | Fix for incompleteness bug with decision engine: repeat... |
commit | commitdiff | tree |
| 2012-06-15 |
Tim King | Fixing mac compilation issues. |
commit | commitdiff | tree |
| 2012-06-15 |
Kshitij Bansal | one bug fixed |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | WIP |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | fixing the problems with the bvminisat. there was a... |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | add failing regression, move error up |
commit | commitdiff | tree |
| 2012-06-14 |
Tim King | Fixing a case for explanation of non-normal form equali... |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | bug fixes in justification heuristic |
commit | commitdiff | tree |
| 2012-06-14 |
Tim King | Fixing a bug related to explaining propagations with... |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | enabling fixed bug345 case |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | fixes for the hasTerm issues in the shared database... |
commit | commitdiff | tree |
| 2012-06-14 |
Clark Barrett | New substitutions implementation - fixes performance... |
commit | commitdiff | tree |
| 2012-06-14 |
Tim King | Fixed arithmetic consistency issue. The simplex confli... |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | fix for clark's bug |
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | don't run rewriterules regressions by default; fixes... |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | fix quantifier non-bug |
commit | commitdiff | tree |
| 2012-06-14 |
Clark Barrett | Removed an assertion, unneeded header file |
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | some changes to make CVC4 work nicely with trace execut... |
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | making --simplification=none the default for quantified... |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | bug ifx, mv |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | restore destruction of stuff in driver |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | This commit: |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | failing quantifier |
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | The "no-tears-in-competition-mode" commit. Change... |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | fix cout, fix statname, rm deadcode |
commit | commitdiff | tree |
| 2012-06-14 |
Kshitij Bansal | add passing regression |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | changing to a more natural propagation order in uf... |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | some changes to the uf engine |
commit | commitdiff | tree |
| 2012-06-14 |
Tim King | Brings the tuning branch into trunk. This includes... |
commit | commitdiff | tree |
| 2012-06-14 |
Morgan Deters | bug 346 resolved |
commit | commitdiff | tree |
| 2012-06-14 |
Dejan Jovanović | * removing rewriteEquality from the rewriter |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | removing bug233 until morgan commits the actual file |
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | adding some regressions to the usual regressions runs... |
commit | commitdiff | tree |
| 2012-06-13 |
Tim King | Added witnesses to Constraints. |
commit | commitdiff | tree |
| 2012-06-13 |
Tim King | - Added a loop to internally assert constraints that... |
commit | commitdiff | tree |
| 2012-06-13 |
Tim King | Fixed whitespace warning on Makefile. |
commit | commitdiff | tree |
| 2012-06-13 |
Tim King | Adds debugging output to theory_engine.cpp. |
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | revisions to the "make submission" target |
commit | commitdiff | tree |
| 2012-06-13 |
Morgan Deters | Don't use the "inlined" feature of ANTLR 3.2, which... |
commit | commitdiff | tree |
| 2012-06-13 |
Kshitij Bansal | add passing regression |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | fix for bug 354 |
commit | commitdiff | tree |
| 2012-06-13 |
Clark Barrett | Fixed failing assertion when EqualityEngine is in conflict |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | enabling regressions from last night, all fixed |
commit | commitdiff | tree |
| 2012-06-13 |
Kshitij Bansal | enable some decision regressions |
commit | commitdiff | tree |
| 2012-06-13 |
Kshitij Bansal | Make d_result in DE context dependent |
commit | commitdiff | tree |
| 2012-06-13 |
Clark Barrett | Fixed definition of bvsmod |
commit | commitdiff | tree |
| 2012-06-13 |
Kshitij Bansal | decision regressions, all but one fail |
commit | commitdiff | tree |
| 2012-06-13 |
Clark Barrett | Fixes more problems in bv rewrites |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | !(*child_it).isConst() assertion fail |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | r2.node == response.node failure |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | r2.node == response.node failure |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | !current[0].isConst() failure |
commit | commitdiff | tree |
| 2012-06-13 |
Clark Barrett | Fixes lots of problems in bv rewrite rules and adds... |
commit | commitdiff | tree |
| 2012-06-13 |
Dejan Jovanović | benchmark to show that we don't rewrite bvsmod correctly |
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | Fix some compile warnings (but they never showed up... |
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but... |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | missing problems |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | wrong answer for bv |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Moved some things around in the preprocessor. Now... |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Fixed fuzzing bug |
commit | commitdiff | tree |
| 2012-06-12 |
Tim King | Fix to yesterday's change in arithmetic. |
commit | commitdiff | tree |
| 2012-06-12 |
Kshitij Bansal | bv reduced with decision: sat instead of unsat |
commit | commitdiff | tree |
| 2012-06-12 |
Kshitij Bansal | Assert fail equaility_engine.cpp: hasTerm(node) with... |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | bufixes and the bugs |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | conflicts from theories are removable |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Changed bitvector theory rewriter so that equalities... |
commit | commitdiff | tree |
| 2012-06-12 |
Kshitij Bansal | cleanup of exit mechanism when decisionEngine is on... |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt... |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Fixed failing assertion in arrays for bug 347 |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | more breakage in aufbv |
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | minor cleanup, and replace a "private:" in equality... |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Fixed compile error |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Enabling constant propagation |
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | fix a few compatibility bindings issues |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | wrong answer benchmarks |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | wrong result benchmark |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog