| 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 |
| 2012-06-06 |
Morgan Deters | Fixing numerous issues with tests and "make dist": |
commit | commitdiff | tree |
| 2012-06-06 |
Dejan Jovanović | disabling a super-expensive assertions to speed up... |
commit | commitdiff | tree |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
commit | commitdiff | tree |
| 2012-06-06 |
Clark Barrett | Fixed problem causing crash at destruction time |
commit | commitdiff | tree |
| 2012-06-05 |
Clark Barrett | More clean-up |
commit | commitdiff | tree |
| 2012-06-05 |
Clark Barrett | Fixed a performance issue with unconstrained simplifier |
commit | commitdiff | tree |
| 2012-06-05 |
Clark Barrett | Adding missing files... |
commit | commitdiff | tree |
| 2012-06-04 |
Clark Barrett | Added preprocessing pass that propagates unconstrained... |
commit | commitdiff | tree |
| 2012-06-01 |
Morgan Deters | add a global user-context push/pop in smt engine, just... |
commit | commitdiff | tree |
| 2012-05-31 |
Clark Barrett | Fixed bug in bv: one more case where non-shared equalit... |
commit | commitdiff | tree |
| 2012-05-31 |
Morgan Deters | svn:ignore a parallel-tests driver file that automake... |
commit | commitdiff | tree |
| 2012-05-31 |
Morgan Deters | pass JAVA_CPPFLAGS properly |
commit | commitdiff | tree |
| 2012-05-30 |
Clark Barrett | Added BitwiseEq bitvector rewrite |
commit | commitdiff | tree |
| 2012-05-30 |
Clark Barrett | Fixed problem with array queue growing too large |
commit | commitdiff | tree |
| 2012-05-30 |
Morgan Deters | remove unused/broken check build target |
commit | commitdiff | tree |
| 2012-05-29 |
Morgan Deters | removing now-unused TheoryEngine::setLogic() interface... |
commit | commitdiff | tree |
| 2012-05-29 |
Clark Barrett | Enabled SolveEq bv rewrite |
commit | commitdiff | tree |
| 2012-05-28 |
Clark Barrett | Added some BV rewrites, fixed bugs in array theory... |
commit | commitdiff | tree |
| 2012-05-27 |
Dejan Jovanović | some reordering to keep invariants |
commit | commitdiff | tree |
| 2012-05-27 |
Dejan Jovanović | Committing the work on equality engine, I need to see... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog