| Age | Commit message (Expand) | Author |
|---|
| 2011-10-17 | Sharing work | Dejan Jovanović |
| 2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
| 2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
| 2011-09-02 | * Changing pre-registration to be context dependent -- it is called from the ... | Dejan Jovanović |
| 2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
| 2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
| 2011-06-30 | only use theory registration if (1) a theory requests it, or (2) if there's m... | Morgan Deters |
| 2011-05-31 | This commit contains the code for allowing arbitrary equalities in the theory... | Tim King |
| 2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
| 2011-04-18 | This commit merges the branch arithmetic/propagation-again into trunk. | Tim King |
| 2011-04-04 | Reverts previous commit r1636. | Tim King |
| 2011-04-02 | Delayed the addition of unate propagation lemmas until propagation is called.... | Tim King |
| 2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
| 2011-03-30 | Merged the branch sparse-tableau into trunk. | Tim King |
| 2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
| 2011-03-17 | SimplexDecisionProcedure no longer takes an OutputChannel as a parameter. | Tim King |
| 2011-03-17 | - Removes arith_constants.h | Tim King |
| 2011-03-15 | Merge from cudd branch. This mostly just adds support for linking | Morgan Deters |
| 2011-03-07 | Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now ... | Tim King |
| 2011-03-03 | Merged the tableau-copy branch into trunk. This adds a copy constructor and o... | Tim King |
| 2011-02-27 | - Adds a path for Theory to be passed a reference to Options. | Tim King |
| 2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
| 2011-02-19 | Changes: | Tim King |
| 2011-02-18 | Changes: | Tim King |
| 2011-02-17 | Removed ActivityMonitor from arithmetic. This was only used for row ejection,... | Tim King |
| 2011-02-16 | Overview of the changes: | Tim King |
| 2011-02-13 | 3 heuristics were added to arithmetic. A heuristic for detecting an encoding ... | Tim King |
| 2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
| 2010-11-16 | Added Theory::presolve(). | Tim King |
| 2010-11-15 | This commit merges the arith-prop-opt branch into the main trunk. This was do... | Tim King |
| 2010-11-09 | Lemmas on demand work, push-pop, some cleanup. | Dejan Jovanović |
| 2010-10-29 | Factors out the QF_LRA decision procedure from TheoryArith and puts this into... | Tim King |
| 2010-10-23 | Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more ... | Tim King |
| 2010-10-22 | Code cleanup for TheoryArith. | Tim King |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
| 2010-10-02 | branches/arith-indexed-variables merged into the main trunk. | Tim King |
| 2010-09-21 | part of review (bug #197): coding conventions, file-level documentation, re-r... | Morgan Deters |
| 2010-09-13 | * New normal form for arithmetic is in place. | Tim King |
| 2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett |
| 2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
| 2010-06-30 | * theory "tree" rewriting implemented and works | Morgan Deters |
| 2010-06-29 | This commit merges the decaying-rows branch into the main trunk. | Tim King |
| 2010-06-29 | Merging the unate-propagator branch into the trunk. This is a big update so ... | Tim King |
| 2010-06-18 | Merging the statistics branch into the main trunk. I'll go over how to use th... | Tim King |
| 2010-06-16 | Added the experimental. +bool TheoryArith::AssertEquality(TNode n, TNode orig... | Tim King |
| 2010-06-16 | More assorted changes to arithmetic in preparation for the code review. | Tim King |
| 2010-06-06 | Some assorted fixes and local optimizations for theory arith. | Tim King |
| 2010-06-04 | Changed how assignments are saved during check. These are now backed by an a... | Tim King |
