Age | Commit message (Expand) | Author |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
2012-08-01 | some fixes for Mac OS | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-27 | Fixing a bug in proof production for the DioSolver. | Tim King |
2012-06-27 | This adds TheoryArith::safeToReset(). This fixes bug 363. | Tim King |
2012-06-27 | Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorit... | Tim King |
2012-06-27 | Improved debugging output. | Tim King |
2012-06-27 | Improved debugging output. | Tim King |
2012-06-27 | Adding reduce() to the ArithPriorityQueue. This reduces the queue from a supe... | Tim King |
2012-06-25 | Added a warning to arithmetic for a known dio solver bug. Somehow the fix nev... | Tim King |
2012-06-16 | Fixing if condition for trivial equalities in arithmetic. Also some whitespac... | Tim King |
2012-06-14 | Fixing a case for explanation of non-normal form equalities. | Tim King |
2012-06-14 | Fixing a bug related to explaining propagations with non-normalized witnesses. | Tim King |
2012-06-14 | Fixed arithmetic consistency issue. The simplex conflict variable had to be ... | Tim King |
2012-06-14 | The "no-tears-in-competition-mode" commit. Change all (non-driver, non-SAT-s... | Morgan Deters |
2012-06-14 | fix cout, fix statname, rm deadcode | Kshitij Bansal |
2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović |
2012-06-13 | Added witnesses to Constraints. | Tim King |
2012-06-13 | - Added a loop to internally assert constraints that are marked as true. | Tim King |
2012-06-12 | Fix to yesterday's change in arithmetic. | Tim King |
2012-06-11 | Fix to term normalization of integer equalities. Adds a regression test that ... | Tim King |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-10 | fixes for bug347 | Dejan Jovanović |
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-19 | - The array type rules were fixed to use isSubtypeOf. | Tim King |
2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for arith... | Tim King |
2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King |
2012-05-17 | This fixes a fascinating segfault. This is the sequence of events: | Tim King |
2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
2012-05-14 | fixes for shared term registration. previously the type was not considered wh... | Dejan Jovanović |
2012-05-11 | Partially fixes something-like-a-problem with TheoryArith::getDeltaValue(). | Tim King |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
2012-05-07 | Fixing a bug with TheoryArith::ppAssert() and shared terms. | Tim King |
2012-05-07 | Fixes a sign bug in the DioSolver. | Tim King |
2012-05-04 | - This fixes a problem where simplex produced the same conflict in the single... | Tim King |
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
2012-04-27 | This merges in the branch cvc4/branches/arithmetic/matrix into trunk. | Tim King |
2012-04-24 | This commit merges in the branch branches/arithmetic/congruence into trunk. H... | Tim King |
2012-04-18 | cout -> warning. Happening in portfolio | Kshitij Bansal |
2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
2012-04-11 | merge from arrays-clark branch | Morgan Deters |