Age | Commit message (Expand) | Author |
2011-09-16 | fix numerous documentation issues; doxygen complains much less, now | 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-09 | surprize surprize | Dejan Jovanović |
2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
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-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-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-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-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-04-01 | PARSER STUFF: | Morgan Deters |
2010-03-12 | * Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine, | Morgan Deters |
2010-03-08 | some more sat stuff for tim: assertions now go to theory_uf | Dejan Jovanović |
2010-03-03 | Some SAT stuff, not doing anything special yet, just to keep it in sync. | 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-22 | * configure.ac: Remove doc/ from search path for Makefile.ams | Morgan Deters |
2010-02-09 | Changes to the CNF conversion and the SAT solver. All regression pass now, an... | Dejan Jovanović |
2010-02-04 | beautification of the prop engine | Dejan Jovanović |
2010-02-04 | remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing... | Morgan Deters |
2010-02-04 | Changed mapping from atoms to literals in the prop engine to be atoms to vars. | Tim King |
2010-02-04 | minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re... | Morgan Deters |
2010-02-03 | Addressed many of the concerns of bug 10 (build system code review). | Morgan Deters |
2010-02-03 | I hacked in a temporary way to restart minisat for multiple queries. | Tim King |
2010-02-02 | Switched cnf conversion to go through CnfStream. | Tim King |
2010-01-30 | cnf conversion (variable-introducing), cleanups, fixes to minisat calling for... | 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-12-08 | work on propositional layer, expression builder support for large expressions... | Morgan Deters |
2009-11-24 | various fixes and updates to use and support parser | 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 |