| 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 |
| 2012-06-10 |
Clark Barrett | Fixed one more bug in rewriter |
commit | commitdiff | tree |
| 2012-06-10 |
Clark Barrett | Added a very fruitful assertion to the rewriter: checks... |
commit | commitdiff | tree |
| 2012-06-10 |
Dejan Jovanović | adding an assertion to trigger the problem of bug349... |
commit | commitdiff | tree |
| 2012-06-10 |
Dejan Jovanović | fixes for bug347 |
commit | commitdiff | tree |
| 2012-06-09 |
Clark Barrett | Turning on unconstrained simp for QF_AUFBV |
commit | commitdiff | tree |
| 2012-06-09 |
Morgan Deters | Cleanup and comments for the dag-ifier. Also some... |
commit | commitdiff | tree |
| 2012-06-09 |
Morgan Deters | Dagification of output expressions. |
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | The option --arith-presolve-lemmas had previously been... |
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | Extend Printer infrastructure also to the "Result"... |
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | minor fixes, for Mac OS |
commit | commitdiff | tree |
| 2012-06-08 |
Dejan Jovanović | very small fast example for the bv fail |
commit | commitdiff | tree |
| 2012-06-08 |
Morgan Deters | Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri... |
commit | commitdiff | tree |
| 2012-06-08 |
Kshitij Bansal | handle BitVectorSignExtend in pickler |
commit | commitdiff | tree |
| 2012-06-08 |
Kshitij Bansal | threadlocal |
commit | commitdiff | tree |
| 2012-06-08 |
Kshitij Bansal | Merge from decision branch (till r3663) |
commit | commitdiff | tree |
| 2012-06-08 |
Dejan Jovanović | small fuzz examples where bv fails |
commit | commitdiff | tree |
| 2012-06-07 |
Dejan Jovanović | fixing the wrong results. arrays equality adaptor had... |
commit | commitdiff | tree |
| 2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization... |
commit | commitdiff | tree |
| 2012-06-07 |
Clark Barrett | Fixed performance issue with ite_simplifier on some... |
commit | commitdiff | tree |
| 2012-06-07 |
Morgan Deters | Adding EchoCommand and associated printer and parser... |
commit | commitdiff | tree |
| 2012-06-07 |
Dejan Jovanović | cleaning up the expample for the future |
commit | commitdiff | tree |
| 2012-06-07 |
Clark Barrett | Added small test case for diseq propagation |
commit | commitdiff | tree |
| 2012-06-07 |
Dejan Jovanović | fixing some bugs in propagation of disequalities |
commit | commitdiff | tree |
| 2012-06-06 |
Clark Barrett | Don't ever call nonclausalSimplify if simplificationMod... |
commit | commitdiff | tree |
| 2012-06-06 |
Clark Barrett | Fixed assertion failures |
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | removing std::cout from trunk |
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | also remove now-incorrect comment from makefile |
commit | commitdiff | tree |
| 2012-06-06 |
Clark Barrett | Fixed broken test case, removed one that is a mistake |
commit | commitdiff | tree |
| 2012-06-06 |
Morgan Deters | unconstrained regressions are now run with "make check... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog