| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2010-06-30 | * theory "tree" rewriting implemented and works | Morgan Deters |
| 2010-06-29 | Merging the unate-propagator branch into the trunk. This is a big update so ... | Tim King |
| 2010-06-24 | Added post_mortem.py a statistics collector for user with the smt_curnch clus... | 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-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |
| 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-05-25 | Some initial changes to allow for lemmas on demand. | Dejan Jovanović |
| 2010-05-20 | Added the division symbol to the parser, and minimal support for it in Theory... | Tim King |
| 2010-05-19 | Significant revision to theory/arith. The new draft has a lot of small bug f... | Tim King |
| 2010-04-14 | Marging from types 404:415, changes: Massive | Dejan Jovanović |
| 2010-04-13 | Doxygen fixes | Christopher L. Conway |
| 2010-04-01 | reran update-copyright.pl to get new contributors and add new header comments... | Morgan Deters |
| 2010-04-01 | PARSER STUFF: | Morgan Deters |
| 2010-03-30 | Highlights of this commit are: | Morgan Deters |
| 2010-03-15 | This checkin resolves bug #57. | Morgan Deters |
| 2010-03-12 | Fixing unnecessary construction of NOT nodes when generating conflict clause... | Dejan Jovanović |
| 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-03-11 | Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t... | Dejan Jovanović |
| 2010-03-08 | adding simple-uf to the regressions, and the code that apparently solves it | Dejan Jovanović |
| 2010-03-08 | some more sat stuff for tim: assertions now go to theory_uf | Dejan Jovanović |
| 2010-02-26 | * test/unit/context/context_black.h: Test CDList<>. In particular, | Morgan Deters |
| 2010-02-25 | * src/expr/node.h: add a copy constructor. Apparently GCC doesn't | Morgan Deters |
| 2010-02-04 | minor interface changes to TheoryEngine/Theory after meeting and conversation... | 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-08 | work on propositional layer, expression builder support for large expressions... | Morgan Deters |
| 2009-11-19 | testing framework, configure fixes, incorporations from meeting, continued work | Morgan Deters |
| 2009-11-17 | from meeting | Morgan Deters |
