| 2012-07-14 |
Morgan Deters | fix a warning in unit test compilation |
commit | commitdiff | tree |
| 2012-07-14 |
Morgan Deters | svn ignore |
commit | commitdiff | tree |
| 2012-07-14 |
Dejan Jovanović | an example that uses bitvectors to simulate sha1 comput... |
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | removing readme from fmf-devel |
commit | commitdiff | tree |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
commit | commitdiff | tree |
| 2012-07-10 |
Morgan Deters | svn ingore |
commit | commitdiff | tree |
| 2012-07-10 |
Dejan Jovanović | * fixing the simple_vc_cxx.cpp compile issue (no more... |
commit | commitdiff | tree |
| 2012-07-10 |
Dejan Jovanović | going back to 1. being a non decimal |
commit | commitdiff | tree |
| 2012-07-10 |
Dejan Jovanović | small changes: |
commit | commitdiff | tree |
| 2012-07-09 |
Morgan Deters | minor fix-ups |
commit | commitdiff | tree |
| 2012-07-09 |
Morgan Deters | fix portfolio build |
commit | commitdiff | tree |
| 2012-07-09 |
Morgan Deters | fix eXecutable bit on a script |
commit | commitdiff | tree |
| 2012-07-08 |
Morgan Deters | minor SMT-LIBv2 compliance issues |
commit | commitdiff | tree |
| 2012-07-08 |
Morgan Deters | remove a debugging line from configure script that... |
commit | commitdiff | tree |
| 2012-07-08 |
Morgan Deters | another signed-ness warning fix for newer GCC |
commit | commitdiff | tree |
| 2012-07-08 |
Morgan Deters | Minor changes to avoid some warnings on GCC 4.7.1 ... |
commit | commitdiff | tree |
| 2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
commit | commitdiff | tree |
| 2012-07-07 |
Morgan Deters | Various fixes to documentation---typos, some incomplete... |
commit | commitdiff | tree |
| 2012-07-06 |
Tim King | Adding std namespace to a couple of make_pair instances. |
commit | commitdiff | tree |
| 2012-07-06 |
Tim King | Added include unistd to main/util.cpp |
commit | commitdiff | tree |
| 2012-07-06 |
Tim King | Added virtual destructor to PpRewrite. |
commit | commitdiff | tree |
| 2012-07-01 |
Morgan Deters | Some changes to configure.ac: |
commit | commitdiff | tree |
| 2012-06-28 |
Morgan Deters | svn:ignore |
commit | commitdiff | tree |
| 2012-06-28 |
Clark Barrett | Fixed bug in bv rewriter that caused wrong answer in... |
commit | commitdiff | tree |
| 2012-06-28 |
Morgan Deters | fix a link error on church, due to Antlr #defining... |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | Fixing a bug in proof production for the DioSolver. |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | This adds TheoryArith::safeToReset(). This fixes bug... |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | Adding access to simplex's ArithPriorityQueue to Theory... |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | Improved debugging output. |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | Improved debugging output. |
commit | commitdiff | tree |
| 2012-06-27 |
Tim King | Adding reduce() to the ArithPriorityQueue. This reduces... |
commit | commitdiff | tree |
| 2012-06-25 |
Tim King | Added a warning to arithmetic for a known dio solver... |
commit | commitdiff | tree |
| 2012-06-22 |
François Bobot | TPTP: add parser for cnf and fof |
commit | commitdiff | tree |
| 2012-06-22 |
François Bobot | parser: add some acces function and recover the origina... |
commit | commitdiff | tree |
| 2012-06-22 |
François Bobot | fix : function AntlrInput::tokenTextSubstr |
commit | commitdiff | tree |
| 2012-06-22 |
François Bobot | Parser: add the possibility to bind at level 0. |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | qf_lra strategy |
commit | commitdiff | tree |
| 2012-06-18 |
Clark Barrett | Reverting buggy rewriter code |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | another qf_lra strategy update |
commit | commitdiff | tree |
| 2012-06-18 |
Clark Barrett | Fixed bug in rewriter |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | unnecessary ^ in regular expression; warning produced... |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | QF_LRA strategy in run script, now final (?) for smt... |
commit | commitdiff | tree |
| 2012-06-18 |
Morgan Deters | final sources (?) for competition |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog