| Age | Commit message (Expand) | Author |
|---|
| 2012-06-14 | This commit: | Kshitij Bansal |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal |
| 2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
| 2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal |
| 2012-04-30 | Added map from skolem variables to new ite formulas in ite removal. | Clark Barrett |
| 2012-04-25 | fix for de+lemmas | Kshitij Bansal |
| 2012-04-23 | Merge from decision branch -- partially working justification heuristic | Kshitij Bansal |
| 2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
| 2012-04-11 | merge from arrays-clark branch | Morgan Deters |
| 2012-03-26 | More cleaning up. | Dejan Jovanović |
| 2012-03-25 | sat_module.h,cpp -> sat_solver.h,cpp (as intended) | Dejan Jovanović |
| 2012-03-25 | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) | Dejan Jovanović |
| 2012-03-09 | Some work on the dump infrastructure to support portfolio work. | Morgan Deters |
| 2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
| 2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
| 2012-02-20 | fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my... | Morgan Deters |
| 2011-11-29 | Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic no... | Tim King |
| 2011-11-15 | Bindings work (ocaml bindings are now sort of working); also minor cleanup | Morgan Deters |
| 2011-10-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
| 2011-10-05 | ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t... | Morgan Deters |
| 2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in preparation... | Morgan Deters |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović |
| 2011-07-11 | Clark's work on array theory - can now solve all QF_AX problems | Clark Barrett |
| 2011-07-11 | merge from symmetry branch | Morgan Deters |
| 2011-07-09 | surprize surprize | Dejan Jovanović |
| 2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
| 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-31 | Fixes to Valuation. | Tim King |
| 2011-03-30 | Add Valuation::getSatValue() so that theories can access the current | 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-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-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-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-07-04 | Considerably simplified the way output streams are used. This commit | Morgan Deters |
| 2010-06-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |
| 2010-06-01 | In order for splitting on demand to be able to retract clauses every translat... | Dejan Jovanović |
| 2010-05-25 | Some initial changes to allow for lemmas on demand. | Dejan Jovanović |
| 2010-05-14 | Adding debugging code in PropEngine/CnfStream | Christopher L. Conway |
| 2010-05-13 | Minor refactorings to PropEngine, SatSolver | Christopher L. Conway |
| 2010-03-09 | (no commit message) | Dejan Jovanović |
