| Age | Commit message (Expand) | Author |
|---|
| 2012-09-06 | Remove SmtEngine::getStackLevel(), which exposed implementation details and w... | Morgan Deters |
| 2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
| 2012-08-28 | Improved compatibility layer, now supports quantifiers. Also incorporates | Morgan Deters |
| 2012-08-08 | Public interface review items: | Morgan Deters |
| 2012-08-06 | Support setting :regular-output-channel and :diagnostic-output-channel. | Morgan Deters |
| 2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
| 2012-08-01 | a couple fixes to SmtEngine::setOption(). thanks Andy for the report! | Morgan Deters |
| 2012-08-01 | fix for the SmtEngine::beforeSearch() option predicate | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-17 | SMT-LIBv2 compliance updates: | Morgan Deters |
| 2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-06-14 | This commit: | Kshitij Bansal |
| 2012-06-12 | Moved some things around in the preprocessor. Now theory preprocessing gets | Clark Barrett |
| 2012-06-12 | cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we we... | Kshitij Bansal |
| 2012-06-12 | Adding constant propagation code - needs more testing - off by default | Clark Barrett |
| 2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
| 2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
| 2012-05-11 | Added some ITE rewrites, | Clark Barrett |
| 2012-04-28 | New LogicInfo functionality. | Morgan Deters |
| 2012-04-23 | Merge from decision branch -- partially working justification heuristic | Kshitij Bansal |
| 2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
| 2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
| 2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
| 2012-02-23 | Added ability to set a "cvc4-specific logic" in standards-compliant | Morgan Deters |
| 2012-02-20 | portfolio merge | Morgan Deters |
| 2012-02-20 | Added Theory::postsolve() infrastructure as Clark requested. | Morgan Deters |
| 2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |
| 2011-10-28 | merged the proofgen3 branch into trunk: | Liana Hadarean |
| 2011-10-13 | Interruption, time-out, and deterministic time-out ("resource-out") features. | Morgan Deters |
| 2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in preparation... | Morgan Deters |
| 2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
| 2011-09-20 | Merge from "swig" branch: language binding for Java is compiling and linking.... | Morgan Deters |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
| 2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
| 2011-05-02 | Minor fixes to various parts of CVC4, including the removal of the uintptr_t ... | Morgan Deters |
| 2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
| 2010-11-19 | Merge from ufprop branch, including: | Morgan Deters |
| 2010-11-16 | SmtEngine now fails with a ModalException if --incremental is not enabled | Morgan Deters |
| 2010-11-09 | Lemmas on demand work, push-pop, some cleanup. | Dejan Jovanović |
| 2010-11-08 | cleanup, documentation, SMT-LIBv2 compliance | Morgan Deters |
| 2010-10-22 | removing unused functionality from util; related to bug #222 | 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 | 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 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ... | Morgan Deters |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
| 2010-10-08 | * (define-fun...) now has proper type checking in non-debug builds | Morgan Deters |
