summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
AgeCommit message (Expand)Author
2012-06-18bugfix, enable only QF_LRA, not other arithKshitij Bansal
2012-06-18QF_LRA, Quantifiers: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17QF_AUFLIA: enable use decision for (only for) stopping searchKshitij Bansal
2012-06-17enabling theoryof=term for quantifiers with sharingDejan Jovanović
2012-06-17Removed assertion that can failClark Barrett
2012-06-16This is an attempt to fix the bug in the justification heuristic. TheKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-16Fixing if condition for trivial equalities in arithmetic. Also some whitespac...Tim King
2012-06-15Fixes some assertion failuresClark Barrett
2012-06-15Fix for incompleteness bug with decision engine: repeated simplificationClark Barrett
2012-06-15one bug fixedKshitij Bansal
2012-06-14WIPKshitij Bansal
2012-06-14add failing regression, move error upKshitij Bansal
2012-06-14New substitutions implementation - fixes performance issue seen in nonclausalClark Barrett
2012-06-14Removed an assertion, unneeded header fileClark Barrett
2012-06-14some changes to make CVC4 work nicely with trace executor for application tra...Morgan Deters
2012-06-14making --simplification=none the default for quantified logics; this a reques...Morgan Deters
2012-06-14bug ifx, mvKshitij Bansal
2012-06-14restore destruction of stuff in driverKshitij Bansal
2012-06-14This commit:Kshitij Bansal
2012-06-14Brings the tuning branch into trunk. This includes the changes from restricte...Tim King
2012-06-12Moved some things around in the preprocessor. Now theory preprocessing getsClark Barrett
2012-06-12cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we we...Kshitij Bansal
2012-06-12Fixed compile errorClark Barrett
2012-06-12Enabling constant propagationClark Barrett
2012-06-12Adding constant propagation code - needs more testing - off by defaultClark Barrett
2012-06-09Turning on unconstrained simp for QF_AUFBVClark Barrett
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-06-07LogicInfo locking implemented, and some initialization-order issues in SmtEng...Morgan Deters
2012-06-06Don't ever call nonclausalSimplify if simplificationMode = NONE (even ifClark Barrett
2012-06-06removing std::cout from trunkMorgan Deters
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-06-01add a global user-context push/pop in smt engine, just like clark's addition ...Morgan Deters
2012-05-31Fixed bug in bv: one more case where non-shared equality was getting propagatedClark Barrett
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback