| Age | Commit message (Expand) | Author |
|---|
| 2012-09-29 | This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ... | Tim King |
| 2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
| 2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
| 2012-09-10 | Fixed an error in the rewriter Pascal pointed out. This was in effectively de... | Tim King |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
| 2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
| 2012-08-14 | Implements TheoryArith::collectModelInfo(). The current implementation is qu... | Tim King |
| 2012-08-14 | Adds substituteDelta() to DeltaRational which given a value for delta returns... | Tim King |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 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ć |
