| Age | Commit message (Expand) | Author |
|---|
| 2012-10-03 | adding ::getBooleanVariables to the PropEngine | Dejan Jovanović |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
| 2012-04-30 | Added map from skolem variables to new ite formulas in ite removal. | Clark Barrett |
| 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-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 |
| 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-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 |
