summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2012-05-15This commit removes the CONST_INTEGER kind from nodes. This code comes from t...Tim King
2012-05-14fixes for shared term registration. previously the type was not considered wh...Dejan Jovanović
2012-05-13fixing build warningsDejan Jovanović
2012-05-11Disabled arith-rewrite-equalities by default unless in a pure arithmetic theoryClark Barrett
2012-05-11Added some ITE rewrites,Clark Barrett
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-09Merge from decision branch (ITE support)Kshitij Bansal
2012-04-30Added map from skolem variables to new ite formulas in ite removal.Clark Barrett
2012-04-28New LogicInfo functionality.Morgan Deters
2012-04-23Merge from decision branch -- partially working justification heuristicKshitij Bansal
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06* Fix ITEs and functions in CVC language printer.Morgan Deters
2012-04-02fix for cvc4_logic dumpKshitij Bansal
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
2012-03-21Disable nonclausal simplification for QF_SAT benchmarks by default.Morgan Deters
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
2012-03-02CDMap -> CDHashMapDejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-28Replace the sequence of hardcoded addTheory() calls with a use of the theory ...Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback