Age | Commit message (Expand) | Author |
2010-11-16 | Added Theory::presolve(). | Tim King |
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-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | 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 | With "-d extra-checking", rewrites are now checked (after | 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-15 | I made a documentation change to get() to make explicit the contract requirem... | Tim King |
2010-06-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |
2010-04-04 | * Node::isAtomic() now looks at an "atomic" attribute of arguments | Morgan Deters |
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-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-02-28 | TheoryUFWhite is passing. I fixed 2 errors. Unfortunately, I also changed a ... | Tim King |
2010-02-26 | * test/unit/context/context_black.h: Test CDList<>. In particular, | Morgan Deters |
2010-02-26 | TheoryUFWhite tests are added. There are also accompanying bug fixes. These c... | Tim King |
2010-02-25 | * src/expr/node.h: add a copy constructor. Apparently GCC doesn't | Morgan Deters |
2010-02-24 | Committing small changes to attribute, and theory to avoid future merge probl... | Tim King |
2010-02-22 | * configure.ac: Remove doc/ from search path for Makefile.ams | Morgan Deters |
2010-02-22 | Re-committing revision 232 properly: | Morgan Deters |
2010-02-22 | undoing improperly-committed revision 232; will re-commit to get "svn blame" ... | Morgan Deters |
2010-02-22 | * Add virtual destructors to CnfStream, Theory, OutputChannel, and | Cesare Tinelli |
2010-02-17 | Initial draft of TheoryUF. Should compile without problems. A decent amount o... | Tim King |
2010-02-10 | note on setup(); for discussion at 2010.02.11 meeting | 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 |
2010-01-29 | fixed CNF conversion, and more modular; CNF conversion command line option; v... | Morgan Deters |
2010-01-19 | minor changes to Theory | Morgan Deters |
2009-12-17 | update-copyright.pl now retrieves and incorporates author information from re... | Morgan Deters |
2009-12-10 | killing expr into node... | Dejan Jovanović |
2009-11-24 | configure option adjustments as per 11/24 meeting; various fixes and improvem... | Morgan Deters |
2009-11-23 | fixups, file comments | Morgan Deters |
2009-11-19 | testing framework, configure fixes, incorporations from meeting, continued work | Morgan Deters |
2009-11-17 | from meeting | Morgan Deters |