summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2012-02-24Theory interface changes:Dejan Jovanović
2012-02-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-20Added Theory::postsolve() infrastructure as Clark requested.Morgan Deters
2012-02-20By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1Morgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g...Morgan Deters
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-20Merge from "swig" branch: language binding for Java is compiling and linking....Morgan Deters
2011-09-16dump define-funs correctly with "--dump declarations", whether the function i...Morgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-08-24Simplification of the preregister and register throught a NodeVisitor class. ...Dejan Jovanović
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-05-02fix a performance issue from last commitMorgan Deters
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ...Morgan Deters
2011-04-25Monday tasks:Morgan Deters
2011-04-22fix to last commitMorgan Deters
2011-04-22Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for fin...Morgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-04-13cache the LET rewriting (and defined-function expansion too)---it wasn't befo...Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory preregistratio...Tim King
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan Deters
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-08command-line flag to disable theory registration, also SMT-LIBv2 compliance (...Morgan Deters
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-27"make dist" fixes; a distribution tarball can now build and pass tests. "make...Morgan Deters
2010-10-22removing unused functionality from util; related to bug #222Morgan Deters
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-22comment out the "interactive" check in SmtEngine::getValue() for now (resolve...Morgan Deters
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-12hooked up "we are incomplete" flag after conversation with Tim (a theory noti...Morgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-12check last result in (get-assignment); some context cleanupMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback