| Age | Commit message (Expand) | Author |
|---|
| 2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
| 2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
| 2011-07-06 | Fixing two bugs: | 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 | Removing dead code that came in on commit r1740. | Tim King |
| 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-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-16 | - Turns on the excluded middle assertions during the miplibTrick. If it is kn... | Tim King |
| 2011-03-16 | - Turns on the miplibTrick. This detects during the static learning phase a ... | 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 | - Creates a queue for lemmas discovered during the simplex procedure. Lemmas ... | Tim King |
| 2011-03-03 | Merged the tableau-copy branch into trunk. This adds a copy constructor and o... | Tim King |
| 2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
| 2011-02-21 | - Adds the statistic d_avgNumRowsNotContainingOnPivot. | Tim King |
| 2011-02-19 | Changes: | Tim King |
| 2011-02-18 | Changes: | Tim King |
| 2011-02-17 | This commit is the promised clean up after removing row ejection. | Tim King |
| 2011-02-17 | Removed ActivityMonitor from arithmetic. This was only used for row ejection,... | Tim King |
| 2011-02-17 | Row ejection is now completely disabled. Another commit cleaning this one up ... | 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-15 | This commit merges the arith-prop-opt branch into the main trunk. This was do... | Tim King |
| 2010-11-12 | Some bug fixes in the SAT for lemmas, and an experiment with a more complete ... | Dejan Jovanović |
| 2010-11-09 | Lemmas on demand work, push-pop, some cleanup. | Dejan Jovanović |
| 2010-11-03 | Adds statistics for the number of Uservariables and Slack variables used by a... | Tim King |
| 2010-10-29 | Factors out the QF_LRA decision procedure from TheoryArith and puts this into... | Tim King |
| 2010-10-28 | The Row implementation has no been replaced by RowVector and ReducedRowVector... | 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-22 | Fixes to getValue for TheoryArith. | Tim King |
| 2010-10-14 | Fixed computation of infinitesimals for arithmetic model generation. | Tim King |
| 2010-10-12 | IDENTITY has been removed. | Tim King |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
| 2010-10-07 | Small tableau optimization. | Tim King |
| 2010-10-04 | Fix to bug 211. ArithVar is now typedefed to uint32_t. | Tim King |
| 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-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters |
| 2010-07-09 | the tableaux optimization | Dejan Jovanović |
