| Age | Commit message (Expand) | Author |
|---|
| 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-27 | Removing Theory::registerTerm() as discussed in the meeting. Now pre-register... | Dejan Jovanović |
| 2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
| 2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović |
| 2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters |
| 2011-07-11 | fix some confusing debug output (bogus counter) | Morgan Deters |
| 2011-07-11 | if running in QF_AX, equalities over terms of uninterpreted sort go to arrays... | Morgan Deters |
| 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-23 | Merge from arrays2 branch. | Morgan Deters |
| 2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
| 2011-04-25 | Weekend work. The main points: | Morgan Deters |
| 2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
| 2011-04-18 | This commit merges the branch arithmetic/propagation-again into trunk. | Tim King |
| 2011-04-18 | Partial merge from datatypes-merge branch: | Morgan Deters |
| 2011-04-05 | Minor adjustments to the Registrar commit in 1644, documentation. | Morgan Deters |
| 2011-04-04 | Merging the satliteral-before-prereg branch into trunk. Theory preregistratio... | Tim King |
| 2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
| 2011-03-30 | Add Valuation::getSatValue() so that theories can access the current | Morgan Deters |
| 2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
| 2011-03-17 | Adds debugging output to EngineOutputChannel::lemma. | Tim King |
| 2011-03-08 | Clean up Theory base class as per code review bug #60; also fixes to CodeTime... | Morgan Deters |
| 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-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
| 2010-11-19 | Merge from ufprop branch, including: | Morgan Deters |
| 2010-11-16 | Added Theory::presolve(). | Tim King |
| 2010-11-15 | Changes to Solver and PropEngine to support lemmasOnDemand during solve but n... | 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-11-08 | command-line flag to disable theory registration, also SMT-LIBv2 compliance (... | Morgan Deters |
| 2010-10-22 | Merging main/getopt.cpp, main/usage.h, and smt/options.h in | Christopher L. Conway |
| 2010-10-21 | * Option --no-type-checking now disables type checks in SmtEngine | Christopher L. Conway |
| 2010-10-12 | hooked up "we are incomplete" flag after conversation with Tim (a theory noti... | Morgan Deters |
| 2010-10-12 | Merge from cc-memout branch. Here are the main points | Morgan Deters |
| 2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp... | Morgan Deters |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
| 2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
| 2010-09-24 | basic union find for bitvectors | Dejan Jovanović |
| 2010-08-17 | Merge from "cc" branch: | Morgan Deters |
| 2010-08-17 | Change TheoryEngine to use pointers to theories instead of | Morgan Deters |
| 2010-07-22 | incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool);... | Morgan Deters |
| 2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett |
| 2010-07-06 | Moved registration to theory engine | Clark Barrett |
| 2010-07-06 | Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some mino... | Morgan Deters |
| 2010-07-04 | enable arrays | Morgan Deters |
| 2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
| 2010-07-02 | re-generated comment headers of source files | Morgan Deters |
| 2010-07-02 | * Added white-box TheoryEngine test that tests the rewriter | Morgan Deters |
