| 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 |
| 2012-06-12 |
Dejan Jovanović | tests for the |
commit | commitdiff | tree |
| 2012-06-12 |
Dejan Jovanović | test cases for the |
commit | commitdiff | tree |
| 2012-06-12 |
Clark Barrett | Adding constant propagation code - needs more testing... |
commit | commitdiff | tree |
| 2012-06-12 |
Tim King | Adding incorrect qf_lia result. |
commit | commitdiff | tree |
| 2012-06-12 |
Morgan Deters | fix ordering issue of --dump-to and --default-dag-thres... |
commit | commitdiff | tree |
| 2012-06-11 |
Tim King | Fix to term normalization of integer equalities. Adds... |
commit | commitdiff | tree |
| 2012-06-11 |
Tim King | Fixing type comparision assertion in getEqualityStatus(). |
commit | commitdiff | tree |
| 2012-06-11 |
Dejan Jovanović | another benchmark that used to fail |
commit | commitdiff | tree |
| 2012-06-11 |
Dejan Jovanović | fixing bitvector bugs |
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | mark a quantifiers global var as "static" so we can... |
commit | commitdiff | tree |
| 2012-06-11 |
Clark Barrett | OK, now the rewrite issues are fixed |
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | distribute an .expect file. fixes a "make check" failu... |
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
commit | commitdiff | tree |
| 2012-06-11 |
Clark Barrett | Fix for array bug with decision heuristic |
commit | commitdiff | tree |
| 2012-06-11 |
Morgan Deters | fix issue referred to in bug 352 regarding infinite... |
commit | commitdiff | tree |
| 2012-06-11 |
Dejan Jovanović | failing bv examples |
commit | commitdiff | tree |
| 2012-06-11 |
Clark Barrett | Fixed bug 352 |
commit | commitdiff | tree |
| 2012-06-11 |
Dejan Jovanović | some failing examples |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog