| Age | Commit message (Expand) | Author |
|---|
| 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-17 | The "UF engineering issues" release, after much profiling. | Morgan Deters |
| 2010-11-16 | Added Theory::presolve(). | Tim King |
| 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-28 | fix pre-registration of operator, previously committed; clean up theory engin... | Morgan Deters |
| 2010-09-28 | comment fix as per this morning's meeting; also, don't theory-rewrite operato... | Morgan Deters |
| 2010-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters |
| 2010-07-27 | Moving EQ->IFF handling from TheoryEngine to parser/type checker | Christopher L. Conway |
| 2010-07-22 | incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool);... | Morgan Deters |
| 2010-07-07 | Shared term manager tested and working | Clark Barrett |
| 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-04 | Considerably simplified the way output streams are used. This commit | Morgan Deters |
| 2010-07-04 | fix to production build | Morgan Deters |
| 2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
| 2010-07-02 | roll back a small change that made arith fail some asserts | Morgan Deters |
| 2010-07-02 | * Added white-box TheoryEngine test that tests the rewriter | Morgan Deters |
| 2010-06-30 | * theory "tree" rewriting implemented and works | Morgan Deters |
| 2010-06-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |
| 2010-06-03 | Fixes a bug where registration occurs before preregistration. | Tim King |
| 2010-06-01 | This commit is a fix for a bug in removeITEs(). The check that the then bran... | Tim King |
| 2010-05-29 | After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. ... | Tim King |
| 2010-05-28 | A few changes to the organization of TheoryEngine rewriting. A few bug fixes ... | Tim King |
| 2010-05-28 | Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ... | Tim King |
| 2010-05-27 | Preregistration has been turned on. Highly experimental eager splitting suppo... | Tim King |
| 2010-04-01 | PARSER STUFF: | Morgan Deters |
| 2010-03-30 | Highlights of this commit are: | Morgan Deters |
| 2010-03-12 | * Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine, | Morgan Deters |
| 2010-03-11 | naive rewriting to fix minisat invariant; rewrite x == x ==> TRUE | Morgan Deters |
| 2010-02-04 | remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing... | Morgan Deters |
| 2010-02-04 | Added theory output channel interfaces and "Interrupted" exception. | Morgan Deters |
| 2009-12-17 | update-copyright.pl now retrieves and incorporates author information from re... | Morgan Deters |
| 2009-12-10 | cleanups, assert work, add a stubbed uf theory, fix driver | Morgan Deters |
