summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2012-06-27Fixing a bug in proof production for the DioSolver.Tim King
2012-06-27This adds TheoryArith::safeToReset(). This fixes bug 363.Tim King
2012-06-27Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorit...Tim King
2012-06-27Improved debugging output.Tim King
2012-06-27Improved debugging output.Tim King
2012-06-27Adding reduce() to the ArithPriorityQueue. This reduces the queue from a supe...Tim King
2012-06-25Added a warning to arithmetic for a known dio solver bug. Somehow the fix nev...Tim King
2012-06-22TPTP: add parser for cnf and fofFrançois Bobot
2012-06-22parser: add some acces function and recover the original nextToken from antlr3François Bobot
2012-06-22fix : function AntlrInput::tokenTextSubstrFrançois Bobot
2012-06-22Parser: add the possibility to bind at level 0.François Bobot
2012-06-18Reverting buggy rewriter codeClark Barrett
2012-06-18Fixed bug in rewriterClark Barrett
2012-06-18Fix for slow array rewrite and minor bug fix in arrays that popped up as a re...Clark Barrett
2012-06-18small bug fix and performance fix in ite simplifierClark Barrett
2012-06-18fixed smt version 1 parser for quantifiersAndrew Reynolds
2012-06-18tracing code to make sure decision options are being set correctlyKshitij Bansal
2012-06-18bugfix, enable only QF_LRA, not other arithKshitij Bansal
2012-06-18QF_LRA, Quantifiers: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-18Fixing bug 360. The driver wasn't exiting when there was an error (it just p...Morgan Deters
2012-06-17QF_AUFLIA: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17fixing a problem due to lemmas produced while backtrackingDejan Jovanović
2012-06-17--decision=justification-stoponly : use decision engine only for stoppingKshitij Bansal
2012-06-17enabling theoryof=term for quantifiers with sharingDejan Jovanović
2012-06-17fixing wrong assertionDejan Jovanović
2012-06-17Removed assertion that can failClark Barrett
2012-06-17Fix array bug causing incorrect answersClark Barrett
2012-06-16small change to equality assertions so that one doesn't get x = y and y = xDejan Jovanović
2012-06-16This is an attempt to fix the bug in the justification heuristic. TheKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-16Fixing if condition for trivial equalities in arithmetic. Also some whitespac...Tim King
2012-06-15Bug fix in justification heuristic. Had to do with howKshitij Bansal
2012-06-15Reverting rewrite rule to working versionClark Barrett
2012-06-15Fixes some assertion failuresClark Barrett
2012-06-15Fix for incompleteness bug with decision engine: repeated simplificationClark Barrett
2012-06-15Fixing mac compilation issues.Tim King
2012-06-15one bug fixedKshitij Bansal
2012-06-14WIPKshitij Bansal
2012-06-14fixing the problems with the bvminisat. there was a case when things would ge...Dejan Jovanović
2012-06-14add failing regression, move error upKshitij Bansal
2012-06-14Fixing a case for explanation of non-normal form equalities.Tim King
2012-06-14bug fixes in justification heuristicKshitij Bansal
2012-06-14Fixing a bug related to explaining propagations with non-normalized witnesses.Tim King
2012-06-14fixes for the hasTerm issues in the shared database under the decision heuristicDejan Jovanović
2012-06-14New substitutions implementation - fixes performance issue seen in nonclausalClark Barrett
2012-06-14Fixed arithmetic consistency issue. The simplex conflict variable had to be ...Tim King
2012-06-14fix for clark's bugDejan Jovanović
2012-06-14fix quantifier non-bugKshitij Bansal
2012-06-14Removed an assertion, unneeded header fileClark Barrett
2012-06-14some changes to make CVC4 work nicely with trace executor for application tra...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback