| 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 |
| 2012-05-27 |
Clark Barrett | Another expensive function call in a Debug trace |
commit | commitdiff | tree |
| 2012-05-27 |
Clark Barrett | Another expensive function call in a Debug line |
commit | commitdiff | tree |
| 2012-05-25 |
Kshitij Bansal | init bug fix |
commit | commitdiff | tree |
| 2012-05-25 |
Clark Barrett | Checking in fix for bug 340 - somehow didn't get checke... |
commit | commitdiff | tree |
| 2012-05-24 |
Dejan Jovanović | Separating the subtheory implementations in the bitvect... |
commit | commitdiff | tree |
| 2012-05-24 |
Dejan Jovanović | Significant changes to the internals of the equality... |
commit | commitdiff | tree |
| 2012-05-22 |
Tim King | This commit merges in the branch arithmetic/cprop. |
commit | commitdiff | tree |
| 2012-05-21 |
Dejan Jovanović | Updating equality manager to handle tagged trigger... |
commit | commitdiff | tree |
| 2012-05-21 |
Morgan Deters | main() no longer catches non-CVC4 exceptions. This... |
commit | commitdiff | tree |
| 2012-05-19 |
Tim King | Adding regress test for bug 341. |
commit | commitdiff | tree |
| 2012-05-19 |
Tim King | - The array type rules were fixed to use isSubtypeOf. |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
commit | commitdiff | tree |
| 2012-05-18 |
Tim King | Removing long unsigned operator+ from CDList's const_it... |
commit | commitdiff | tree |
| 2012-05-18 |
Dejan Jovanović | removing failing regression |
commit | commitdiff | tree |
| 2012-05-17 |
Tim King | This fixes a fascinating segfault. This is the sequenc... |
commit | commitdiff | tree |
| 2012-05-17 |
Morgan Deters | Fixing an issue with LogicInfo::isPure() that turned... |
commit | commitdiff | tree |
| 2012-05-17 |
Liana Hadarean | Fixed bug 338: |
commit | commitdiff | tree |
| 2012-05-17 |
Tim King | Adding failing regression for ite type computation. |
commit | commitdiff | tree |
| 2012-05-17 |
Dejan Jovanović | Queueing up asserted literals in the proxy instead... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | adding simple-minded handling of (dis-)equalities where... |
commit | commitdiff | tree |
| 2012-05-16 |
Morgan Deters | Fixing C compatibility library (it still had a referenc... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | testcase for bug 337 |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | Changes to SAT solver: |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | equality status for bitvectors can now look into the... |
commit | commitdiff | tree |
| 2012-05-16 |
Dejan Jovanović | removing duplicate literals in explanations of propagations |
commit | commitdiff | tree |
| 2012-05-16 |
Liana Hadarean | refactored TheoryBV bitblaster and equality engine... |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | fixed QF_BV performance problem due to using CDList... |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2012-05-15 |
Dejan Jovanović | test cases |
commit | commitdiff | tree |
| 2012-05-15 |
Tim King | Fix to shared terms visitor. |
commit | commitdiff | tree |
| 2012-05-15 |
Morgan Deters | Implement TypeNode::isComparableTo() and add a unit... |
commit | commitdiff | tree |
| 2012-05-15 |
Clark Barrett | Fixed several bugs in shared terms database |
commit | commitdiff | tree |
| 2012-05-15 |
Tim King | This commit removes the CONST_INTEGER kind from nodes... |
commit | commitdiff | tree |
| 2012-05-15 |
Liana Hadarean | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaste... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog