From: Kshitij Bansal Date: Wed, 9 May 2012 05:45:36 +0000 (+0000) Subject: Merge from decision branch (ITE support) X-Git-Tag: cvc5-1.0.0~8196 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6243fba11e0189891acf21de3c6daa072b038e13;p=cvc5.git Merge from decision branch (ITE support) Major changes from last merge * ITEs supported * Don't share theory lemmas to DE, only assertions Should probably be noted that 'make regress' doesn't quite pass with --decision=justification. Throws off search in couple of arith benchmarks. No serious performance changes expected. Keep an eye. --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 7c8718370..1d4f2fd42 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -26,13 +26,15 @@ using namespace std; namespace CVC4 { -DecisionEngine::DecisionEngine(context::Context *c) : + DecisionEngine::DecisionEngine(context::Context *sc, + context::Context *uc) : d_enabledStrategies(), - d_needSimplifiedPreITEAssertions(), + d_needIteSkolemMap(), d_assertions(), d_cnfStream(NULL), d_satSolver(NULL), - d_satContext(c), + d_satContext(sc), + d_userContext(uc), d_result(SAT_VALUE_UNKNOWN) { const Options* options = Options::current(); @@ -42,37 +44,56 @@ DecisionEngine::DecisionEngine(context::Context *c) : if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { - DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext); + ITEDecisionStrategy* ds = + new decision::JustificationHeuristic(this, d_satContext); enableStrategy(ds); + d_needIteSkolemMap.push_back(ds); } } void DecisionEngine::enableStrategy(DecisionStrategy* ds) { d_enabledStrategies.push_back(ds); - if( ds->needSimplifiedPreITEAssertions() ) - d_needSimplifiedPreITEAssertions.push_back(ds); } -void DecisionEngine::informSimplifiedPreITEAssertions(const vector &assertions) + +void DecisionEngine::addAssertions(const vector &assertions) +{ + Assert(false); // doing this so that we revisit what to do + // here. Currently not being used. + + // d_result = SAT_VALUE_UNKNOWN; + // d_assertions.reserve(assertions.size()); + // for(unsigned i = 0; i < assertions.size(); ++i) + // d_assertions.push_back(assertions[i]); +} + +void DecisionEngine::addAssertions + (const vector &assertions, + int assertionsEnd, + IteSkolemMap iteSkolemMap) { + // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; + d_assertions.reserve(assertions.size()); for(unsigned i = 0; i < assertions.size(); ++i) d_assertions.push_back(assertions[i]); - for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) - d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); + + for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) + d_needIteSkolemMap[i]-> + addAssertions(assertions, assertionsEnd, iteSkolemMap); } -void DecisionEngine::addAssertion(Node n) -{ - d_result = SAT_VALUE_UNKNOWN; - if(needSimplifiedPreITEAssertions()) { - d_assertions.push_back(n); - } - for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) - d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); -} +// void DecisionEngine::addAssertion(Node n) +// { +// d_result = SAT_VALUE_UNKNOWN; +// if(needIteSkolemMap()) { +// d_assertions.push_back(n); +// } +// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) +// d_needIteSkolemMap[i]->notifyAssertionsAvailable(); +// } }/* CVC4 namespace */ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 3ec6aaf2a..ea516aa54 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -27,6 +27,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" +#include "util/ite_removal.h" #include "util/output.h" using namespace std; @@ -38,7 +39,7 @@ namespace CVC4 { class DecisionEngine { vector d_enabledStrategies; - vector d_needSimplifiedPreITEAssertions; + vector d_needIteSkolemMap; vector d_assertions; @@ -47,13 +48,16 @@ class DecisionEngine { DPLLSatSolverInterface* d_satSolver; context::Context* d_satContext; + context::Context* d_userContext; SatValue d_result; + // Disable creating decision engine without required parameters + DecisionEngine() {} public: // Necessary functions /** Constructor, enables decision stragies based on options */ - DecisionEngine(context::Context *c); + DecisionEngine(context::Context *sc, context::Context *uc); /** Destructor, currently does nothing */ ~DecisionEngine() { @@ -88,6 +92,11 @@ public: /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool &stopSearch) { + Assert(d_cnfStream != NULL, + "Forgot to set cnfStream for decision engine?"); + Assert(d_satSolver != NULL, + "Forgot to set satSolver for decision engine?"); + SatLiteral ret = undefSatLiteral; for(unsigned i = 0; i < d_enabledStrategies.size() @@ -113,7 +122,7 @@ public: case SAT_VALUE_TRUE: return Result(Result::SAT); case SAT_VALUE_FALSE: return Result(Result::UNSAT); case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - default: Assert(false); + default: Assert(false, "d_result is garbage"); } return Result(); } @@ -137,11 +146,24 @@ public: // External World helping us help the Strategies /** If one of the enabled strategies needs them */ - bool needSimplifiedPreITEAssertions() { - return d_needSimplifiedPreITEAssertions.size() > 0; - } - void informSimplifiedPreITEAssertions(const vector &assertions); + /* bool needIteSkolemMap() { */ + /* return d_needIteSkolemMap.size() > 0; */ + /* } */ + /* add a set of assertions */ + void addAssertions(const vector &assertions); + + /** + * add a set of assertions, while providing a mapping between skolem + * variables and corresponding assertions. It is assumed that all + * assertions after assertionEnd were generated by ite + * removal. Hence, iteSkolemMap maps into only these. + */ + void addAssertions(const vector &assertions, + int assertionsEnd, + IteSkolemMap iteSkolemMap); + + /* add a single assertion */ void addAssertion(Node n); // Interface for Strategies to use stuff stored in Decision Engine @@ -157,15 +179,18 @@ public: // Interface for Strategies to get information about External World - bool hasSatLiteral(Node n) { + bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } - SatLiteral getSatLiteral(Node n) { + SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } + SatValue getSatValue(TNode n) { + return getSatValue(getSatLiteral(n)); + } Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 6746b13cc..6ee583ec2 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -20,6 +20,7 @@ #define __CVC4__DECISION__DECISION_STRATEGY_H #include "prop/sat_solver_types.h" +#include "util/ite_removal.h" namespace CVC4 { @@ -43,11 +44,25 @@ public: virtual prop::SatLiteral getNext(bool&) = 0; - virtual bool needSimplifiedPreITEAssertions() { return false; } + virtual bool needIteSkolemMap() { return false; } virtual void notifyAssertionsAvailable() { return; } }; +class ITEDecisionStrategy : public DecisionStrategy { +public: + ITEDecisionStrategy(DecisionEngine* de, context::Context *c) : + DecisionStrategy(de, c) { + } + + + bool needIteSkolemMap() { return true; } + + virtual void addAssertions(const std::vector &assertions, + unsigned assertionsEnd, + IteSkolemMap iteSkolemMap) = 0; +}; + }/* decision namespace */ }/* CVC4 namespace */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 62bd71f6a..c859e5d07 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -41,13 +41,18 @@ #include "justification_heuristic.h" +#include "expr/node_manager.h" #include "expr/kind.h" +#include "theory/rewriter.h" +#include "util/ite_removal.h" /*** +Here's the main idea -Summary of the algorithm: - - + Given a boolean formula "node", the goal is to try to make it +evaluate to "desiredVal" (true/false). for instance if "node" is a AND +formula we want to make it evaluate to true, we'd like one of the +children to be true. this is done recursively. ***/ @@ -60,6 +65,19 @@ CVC3 code <----> this code ***/ + +// Local helper functions for just this file + +SatValue invertValue(SatValue v) +{ + if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; + else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; + else return SAT_VALUE_TRUE; +} + + +// JustificationHeuristic stuff + void JustificationHeuristic::setJustified(TNode n) { d_justified.insert(n); @@ -70,49 +88,75 @@ bool JustificationHeuristic::checkJustified(TNode n) return d_justified.find(n) != d_justified.end(); } -SatValue invertValue(SatValue v) +SatValue JustificationHeuristic::tryGetSatValue(Node n) { - if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; - else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; - else return SAT_VALUE_TRUE; + Debug("decision") << " " << n << " has sat value " << " "; + if(d_decisionEngine->hasSatLiteral(n) ) { + Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl; + return d_decisionEngine->getSatValue(n); + } else { + Debug("decision") << "NO SAT LITERAL" << std::endl; + return SAT_VALUE_UNKNOWN; + }//end of else +} + +void JustificationHeuristic::computeITEs(TNode n, IteList &l) +{ + Debug("jh-ite") << " computeITEs( " << n << ", &l)\n"; + for(unsigned i=0; isecond); + computeITEs(n[i], l); + } } -bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, SatLiteral* litDecision) -//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision) +const IteList& JustificationHeuristic::getITEs(TNode n) +{ + IteCache::iterator it = d_iteCache.find(n); + if(it != d_iteCache.end()) { + return it->second; + } else { + // Compute the list of ITEs + // TODO: optimize by avoiding multiple lookup for d_iteCache[n] + d_iteCache[n] = vector(); + computeITEs(n, d_iteCache[n]); + return d_iteCache[n]; + } +} + +bool JustificationHeuristic::findSplitterRec(TNode node, + SatValue desiredVal, + SatLiteral* litDecision) { Trace("decision") - << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; + << "findSplitterRec(" << node << ", " + << desiredVal << ", .. )" << std::endl; /* Handle NOT as a special case */ - if (node.getKind() == kind::NOT) { + while (node.getKind() == kind::NOT) { desiredVal = invertValue(desiredVal); node = node[0]; } - if (checkJustified(node)) return false; - - SatValue litVal = tryGetSatValue(node); - -#ifdef CVC4_ASSERTIONS - bool litPresent = false; -#endif - - if(d_decisionEngine->hasSatLiteral(node) ) { - SatLiteral lit = d_decisionEngine->getSatLiteral(node); - -#ifdef CVC4_ASSERTIONS - litPresent = true; -#endif - - SatVariable v = lit.getSatVariable(); - // if (lit.isFalse() || lit.isTrue()) return false; - if (v == 0) { - setJustified(node); - return false; + /* Base case */ + if (checkJustified(node) || d_visited.find(node) != d_visited.end()) + return false; + +#if defined CVC4_ASSERTIONS || defined CVC4_TRACING + // We don't always have a sat literal, so remember that. Will need + // it for some assertions we make. + bool litPresent = d_decisionEngine->hasSatLiteral(node); + if(Trace.isOn("decision")) { + if(!litPresent) { + Trace("decision") << "no sat literal for this node" << std::endl; } - } else { - Trace("decision") << "no sat literal for this node" << std::endl; } + //Assert(litPresent); -- fails +#endif + + // Get value of sat literal for the node, if there is one + SatValue litVal = tryGetSatValue(node); /* You'd better know what you want */ Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); @@ -122,123 +166,104 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat "invariant voilated"); /* What type of node is this */ - Kind k = node.getKind(); + Kind k = node.getKind(); theory::TheoryId tId = theory::kindToTheoryId(k); /* Some debugging stuff */ - Trace("findSpitterRec") << "kind = " << k << std::endl; - Trace("findSplitterRec") << "theoryId = " << tId << std::endl; - Trace("findSplitterRec") << "node = " << node << std::endl; - Trace("findSplitterRec") << "litVal = " << litVal << std::endl; - - /* - if (d_cnfManager->numFanins(v) == 0) { - if (getValue(v) != Var::UNKNOWN) { - setJustified(v); - return false; - } - else { - *litDecision = Lit(v, value == Var::TRUE_VAL); - return true; - } - } - */ - + Trace("jh-findSplitterRec") << "kind = " << k << std::endl; + Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl; + Trace("jh-findSplitterRec") << "node = " << node << std::endl; + Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl; /** * If not in theory of booleans, and not a "boolean" EQUAL (IFF), - * then check if this is something to split-on? + * then check if this is something to split-on. */ if(tId != theory::THEORY_BOOL // && !(k == kind::EQUAL && node[0].getType().isBoolean()) ) { - if(litVal != SAT_VALUE_UNKNOWN) { - setJustified(node); - return false; - } else { - if(not d_decisionEngine->hasSatLiteral(node)) - throw GiveUpException(); - Assert(d_decisionEngine->hasSatLiteral(node)); - SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - Trace("decision") << "decision " << *litDecision << std::endl; - Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; - return true; - } - } + // if node has embedded ites -- which currently happens iff it got + // replaced during ite removal -- then try to resolve that first + const IteList& l = getITEs(node); + Debug("jh-ite") << " ite size = " << l.size() << std::endl; + d_visited.insert(node); + for(unsigned i = 0; i < l.size(); ++i) { + Assert(l[i].getKind() == kind::ITE, "Expected ITE"); + Debug("jh-ite") << " i = " << i + << " l[i] = " << l[i] << std::endl; + if (checkJustified(l[i])) continue; + + SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable +#ifdef CVC4_ASSERTIONS + bool litPresent = d_decisionEngine->hasSatLiteral(l[i]); +#endif - /*** TODO: Term ITEs ***/ - /* - else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) { - // This node represents a predicate with embedded ITE's - // We handle this case specially in order to catch the - // corner case when a variable is in its own fanin. - n = d_cnfManager->numFanins(v); - for (i=0; i < n; ++i) { - litTmp = d_cnfManager->getFanin(v, i); - varTmp = litTmp.getVar(); - DebugAssert(!litTmp.isInverted(),"Expected positive fanin"); - if (checkJustified(varTmp)) continue; - DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE, - "Expected ITE"); - DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE"); - Lit cIf = d_cnfManager->getFanin(varTmp,0); - Lit cThen = d_cnfManager->getFanin(varTmp,1); - Lit cElse = d_cnfManager->getFanin(varTmp,2); - if (getValue(cIf) == Var::UNKNOWN) { - if (getValue(cElse) == Var::TRUE_VAL || - getValue(cThen) == Var::FALSE_VAL) { - ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); - } - else { - ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); - } - if (!ret) { - cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; - DebugAssert(false,"No controlling input found (1)"); - } - return true; - } - else if (getValue(cIf) == Var::TRUE_VAL) { - if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { - return true; - } - if (cThen.getVar() != v && - (getValue(cThen) == Var::UNKNOWN || - getValue(cThen) == Var::TRUE_VAL) && - findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) { + // Handle the ITE to catch the case when a variable is its own + // fanin + SatValue ifVal = tryGetSatValue(l[i][0]); + if (ifVal == SAT_VALUE_UNKNOWN) { + // are we better off trying false? if not, try true + SatValue ifDesiredVal = + (tryGetSatValue(l[i][2]) == desiredVal || + tryGetSatValue(l[i][1]) == invertValue(desiredVal)) + ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; + + if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) { return true; } - } - else { - if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { + Assert(false, "No controlling input found (1)"); + } else { + + // Try to justify 'if' + if (findSplitterRec(l[i][0], ifVal, litDecision)) { return true; } - if (cElse.getVar() != v && - (getValue(cElse) == Var::UNKNOWN || - getValue(cElse) == Var::TRUE_VAL) && - findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) { + + // If that was successful, we need to go into only one of 'then' + // or 'else' + int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; + int chVal = tryGetSatValue(l[i][ch]); + if( d_visited.find(l[i]) == d_visited.end() + && (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) + && findSplitterRec(l[i][ch], desiredVal, litDecision) ) { return true; } } - setJustified(varTmp); + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); + setJustified(l[i]); } - if (getValue(v) != Var::UNKNOWN) { - setJustified(v); + d_visited.erase(node); + + if(litVal != SAT_VALUE_UNKNOWN) { + setJustified(node); return false; - } - else { - *litDecision = Lit(v, value == Var::TRUE_VAL); + } else { + Assert(d_decisionEngine->hasSatLiteral(node)); + /* if(not d_decisionEngine->hasSatLiteral(node)) + throw GiveUpException(); */ + Assert(d_decisionEngine->hasSatLiteral(node)); + SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); + *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); + Trace("decision") << "decision " << *litDecision << std::endl; + Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; return true; } } - */ SatValue valHard = SAT_VALUE_FALSE; switch (k) { + + case kind::CONST_BOOLEAN: + Assert(node.getConst() == false || desiredVal == SAT_VALUE_TRUE); + Assert(node.getConst() == true || desiredVal == SAT_VALUE_FALSE); + setJustified(node); + return false; + case kind::AND: valHard = SAT_VALUE_TRUE; + case kind::OR: if (desiredVal == valHard) { int n = node.getNumChildren(); @@ -247,7 +272,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat return true; } } - Assert(litPresent == false || litVal == valHard, "Output should be justified"); + Assert(litPresent == false || litVal == valHard, + "Output should be justified"); setJustified(node); return false; } @@ -255,9 +281,10 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat SatValue valEasy = invertValue(valHard); int n = node.getNumChildren(); for(int i = 0; i < n; ++i) { - Trace("findSplitterRec") << " node[i] = " << node[i] << " " << tryGetSatValue(node[i]) << std::endl; + Debug("jh-findSplitterRec") << " node[i] = " << node[i] << " " + << tryGetSatValue(node[i]) << std::endl; if ( tryGetSatValue(node[i]) != valHard) { - Trace("findSplitterRec") << "hi"<< std::endl; + Debug("jh-findSplitterRec") << "hi"<< std::endl; if (findSplitterRec(node[i], valEasy, litDecision)) { return true; } @@ -266,11 +293,16 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat return false; } } - Trace("findSplitterRec") << " * ** " << std::endl; - Trace("findSplitterRec") << node.getKind() << " " << node << std::endl; - for(unsigned i = 0; i < node.getNumChildren(); ++i) - Trace("findSplitterRec") << "child: " << tryGetSatValue(node[i]) << std::endl; - Trace("findSplitterRec") << "node: " << tryGetSatValue(node) << std::endl; + if(Debug.isOn("jh-findSplitterRec")) { + Debug("jh-findSplitterRec") << " * ** " << std::endl; + Debug("jh-findSplitterRec") << node.getKind() << " " + << node << std::endl; + for(unsigned i = 0; i < node.getNumChildren(); ++i) + Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i]) + << std::endl; + Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node) + << std::endl; + } Assert(false, "No controlling input found (2)"); } break; @@ -285,7 +317,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) { return true; } - Assert(litPresent == false || litVal == SAT_VALUE_FALSE, "Output should be justified"); + Assert(litPresent == false || litVal == SAT_VALUE_FALSE, + "Output should be justified"); setJustified(node); return false; } @@ -294,7 +327,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) { return true; } - Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified"); + Assert(litPresent == false || litVal == SAT_VALUE_TRUE, + "Output should be justified"); setJustified(node); return false; } @@ -302,13 +336,15 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) { return true; } - Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified"); + Assert(litPresent == false || litVal == SAT_VALUE_TRUE, + "Output should be justified"); setJustified(node); return false; } Assert(false, "No controlling input found (3)"); } break; + case kind::IFF: //throw GiveUpException(); { @@ -322,7 +358,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat if (findSplitterRec(node[1], val, litDecision)) { return true; } - Assert(litPresent == false || litVal == desiredVal, "Output should be justified"); + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); setJustified(node); return false; } @@ -351,7 +388,8 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat if (findSplitterRec(node[1], val, litDecision)) { return true; } - Assert(litPresent == false || litVal == desiredVal, "Output should be justified"); + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); setJustified(node); return false; } @@ -367,62 +405,47 @@ bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, Sat break; } - case kind::ITE: - throw GiveUpException(); - /* - case ITE: { - Lit cIf = d_cnfManager->getFanin(v, 0); - Lit cThen = d_cnfManager->getFanin(v, 1); - Lit cElse = d_cnfManager->getFanin(v, 2); - if (getValue(cIf) == Var::UNKNOWN) { - if (getValue(cElse) == value || - getValue(cThen) == Var::invertValue(value)) { - ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); - } - else { - ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); - } - if (!ret) { - cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; - DebugAssert(false,"No controlling input found (6)"); - } - return true; + case kind::ITE: { + //[0]: if, [1]: then, [2]: else + SatValue ifVal = tryGetSatValue(node[0]); + if (ifVal == SAT_VALUE_UNKNOWN) { + + // are we better off trying false? if not, try true + SatValue ifDesiredVal = + (tryGetSatValue(node[2]) == desiredVal || + tryGetSatValue(node[1]) == invertValue(desiredVal)) + ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; + + if(findSplitterRec(node[0], ifDesiredVal, litDecision)) { + return true; } - else if (getValue(cIf) == Var::TRUE_VAL) { - if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { - return true; - } - if (cThen.isVar() && cThen.getVar() != v && - (getValue(cThen) == Var::UNKNOWN || - getValue(cThen) == value) && - findSplitterRec(cThen, value, litDecision)) { - return true; - } + Assert(false, "No controlling input found (6)"); + } else { + + // Try to justify 'if' + if (findSplitterRec(node[0], ifVal, litDecision)) { + return true; } - else { - if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { - return true; - } - if (cElse.isVar() && cElse.getVar() != v && - (getValue(cElse) == Var::UNKNOWN || - getValue(cElse) == value) && - findSplitterRec(cElse, value, litDecision)) { - return true; - } + + // If that was successful, we need to go into only one of 'then' + // or 'else' + int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; + int chVal = tryGetSatValue(node[ch]); + if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) + && findSplitterRec(node[ch], desiredVal, litDecision) ) { + return true; } - DebugAssert(getValue(v) == value, "Output should be justified"); - setJustified(v); - return false; } - */ + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); + setJustified(node); + return false; + } + default: Assert(false, "Unexpected Boolean operator"); break; - } + }//end of switch(k) - /* Swap order of these two once we handle all cases */ - return false; Unreachable(); - - }/* findRecSplit method */ diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 0457e6d3c..acf2b3cfa 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -34,6 +34,8 @@ namespace CVC4 { namespace decision { +typedef std::vector IteList; + class GiveUpException : public Exception { public: GiveUpException() : @@ -41,15 +43,42 @@ public: } };/* class GiveUpException */ -class JustificationHeuristic : public DecisionStrategy { +class JustificationHeuristic : public ITEDecisionStrategy { + typedef hash_map IteCache; + typedef hash_map SkolemMap; + + // being 'justified' is monotonic with respect to decisions context::CDHashSet d_justified; context::CDO d_prvsIndex; + IntStat d_helfulness; IntStat d_giveup; TimerStat d_timestat; + + /** + * A copy of the assertions that need to be justified + * directly. Doesn't have ones introduced during during ITE-removal. + */ + std::vector d_assertions; + //TNode is fine since decisionEngine has them too + + /** map from ite-rewrite skolem to a boolean-ite assertion */ + SkolemMap d_iteAssertions; + // 'key' being TNode is fine since if a skolem didn't exist anywhere, + // we won't look it up. as for 'value', same reason as d_assertions + + /** Cache for ITE skolems present in a atomic formula */ + IteCache d_iteCache; + + /** + * This is used to prevent infinite loop when trying to find a + * splitter. Can happen when exploring assertion corresponding to a + * term-ITE. + */ + hash_set d_visited; public: JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c): - DecisionStrategy(de, c), + ITEDecisionStrategy(de, c), d_justified(c), d_prvsIndex(c, 0), d_helfulness("decision::jh::helpfulness", 0), @@ -66,74 +95,100 @@ public: } prop::SatLiteral getNext(bool &stopSearch) { Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; - TimerStat::CodeTimer codeTimer(d_timestat); - const vector& assertions = d_decisionEngine->getAssertions(); - - for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) { - SatLiteral litDecision; - - Trace("decision") << assertions[i] << std::endl; + d_visited.clear(); - SatValue desiredVal = SAT_VALUE_UNKNOWN; + for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { + Trace("decision") << d_assertions[i] << std::endl; - if(d_decisionEngine->hasSatLiteral(assertions[i]) ) { - //desiredVal = d_decisionEngine->getSatValue( d_decisionEngine->getSatLiteral(assertions[i]) ); - Trace("decision") << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl; - // continue; - // Assert(not lit.isNull()); - } + // Sanity check: if it was false, aren't we inconsistent? + Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); - if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE; + SatValue desiredVal = SAT_VALUE_TRUE; + SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal); - bool ret; - try { - ret = findSplitterRec(assertions[i], desiredVal, &litDecision); - }catch(GiveUpException &e) { - return prop::undefSatLiteral; - } - if(ret == true) { - Trace("decision") << "Yippee!!" << std::endl; - //d_prvsIndex = i; - ++d_helfulness; + if(litDecision != undefSatLiteral) return litDecision; - } } - Trace("decision") << "Nothing to split on " << std::endl; + Trace("decision") << "jh: Nothing to split on " << std::endl; +#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG bool alljustified = true; - for(unsigned i = 0 ; i < assertions.size() && alljustified ; ++i) { - alljustified &= assertions[i].getKind() == kind::NOT ? - checkJustified(assertions[i][0]) : checkJustified(assertions[i]); + for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { + TNode curass = d_assertions[i]; + while(curass.getKind() == kind::NOT) + curass = curass[0]; + alljustified &= checkJustified(curass); + if(Debug.isOn("decision")) { - bool x = assertions[i].getKind() == kind::NOT ? - checkJustified(assertions[i][0]) : checkJustified(assertions[i]); - if(x==false) - Debug("decision") << "****** Not justified [i="<setResult(SAT_VALUE_TRUE); - return prop::undefSatLiteral; - } - bool needSimplifiedPreITEAssertions() { return true; } - void notifyAssertionsAvailable() { - Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()" - << " size = " << d_decisionEngine->getAssertions().size() - << std::endl; - /* clear the justifcation labels -- reconsider if/when to do - this */ - //d_justified.clear(); - //d_prvsIndex = 0; + } + + void addAssertions(const std::vector &assertions, + unsigned assertionsEnd, + IteSkolemMap iteSkolemMap) { + Trace("decision") + << "JustificationHeuristic::addAssertions()" + << " size = " << assertions.size() + << " assertionsEnd = " << assertionsEnd + << std::endl; + + // Save the 'real' assertions locally + for(unsigned i = 0; i < assertionsEnd; ++i) + d_assertions.push_back(assertions[i]); + + // Save mapping between ite skolems and ite assertions + for(IteSkolemMap::iterator i = iteSkolemMap.begin(); + i != iteSkolemMap.end(); ++i) { + Assert(i->second >= assertionsEnd && i->second < assertions.size()); + Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to " + << assertions[(i->second)] << std::endl; + d_iteAssertions[i->first] = assertions[i->second]; + } + } + + /* Compute justified */ + bool computeJustified() { + } private: - /* Do all the hardwork. */ - bool findSplitterRec(Node node, SatValue value, SatLiteral* litDecision); + SatLiteral findSplitter(TNode node, SatValue desiredVal) + { + bool ret; + SatLiteral litDecision; + try { + ret = findSplitterRec(node, desiredVal, &litDecision); + }catch(GiveUpException &e) { + return prop::undefSatLiteral; + } + if(ret == true) { + Trace("decision") << "Yippee!!" << std::endl; + //d_prvsIndex = i; + ++d_helfulness; + return litDecision; + } else { + return undefSatLiteral; + } + } + + /** + * Do all the hardwork. + * @param findFirst returns + */ + bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision); /* Helper functions */ void setJustified(TNode); @@ -141,18 +196,13 @@ private: /* If literal exists corresponding to the node return that. Otherwise an UNKNOWN */ - SatValue tryGetSatValue(Node n) - { - Debug("decision") << " " << n << " has sat value " << " "; - if(d_decisionEngine->hasSatLiteral(n) ) { - Debug("decision") << d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n)) << std::endl; - return d_decisionEngine->getSatValue(d_decisionEngine->getSatLiteral(n)); - } else { - Debug("decision") << "NO SAT LITERAL" << std::endl; - return SAT_VALUE_UNKNOWN; - } - } + SatValue tryGetSatValue(Node n); + + /* Get list of all term-ITEs for the atomic formula v */ + const IteList& getITEs(TNode n); + /* Compute all term-ITEs in a node recursively */ + void computeITEs(TNode n, IteList &l); };/* class JustificationHeuristic */ }/* namespace decision */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ea6cafdcd..5e1b032a3 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1099,6 +1099,8 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // We need to do a full theory check to confirm + Debug("minisat::search") << "Doing a full theoy check..." + << std::endl; check_type = CHECK_FINAL; continue; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 03746c9b2..5b71e5ec5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -109,13 +109,13 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { } /* Tell decision engine */ - if(negated) { - NodeBuilder<> nb(kind::NOT); - nb << node; - d_decisionEngine->addAssertion(nb.constructNode()); - } else { - d_decisionEngine->addAssertion(node); - } + // if(negated) { + // NodeBuilder<> nb(kind::NOT); + // nb << node; + // d_decisionEngine->addAssertion(nb.constructNode()); + // } else { + // d_decisionEngine->addAssertion(node); + // } //TODO This comment is now false // Assert as removable diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 81af14031..e636b9142 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -272,9 +272,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory::theory_class>(THEORY); CVC4_FOR_EACH_THEORY; - d_decisionEngine = new DecisionEngine(d_context); + d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + d_theoryEngine->setDecisionEngine(d_decisionEngine); // d_decisionEngine->setPropEngine(d_propEngine); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); @@ -1034,14 +1035,16 @@ void SmtEnginePrivate::processAssertions() { // Simplify the assertions simplifyAssertions(); - if(d_smt.d_decisionEngine->needSimplifiedPreITEAssertions()) { - d_smt.d_decisionEngine->informSimplifiedPreITEAssertions(d_assertionsToCheck); - } + // any assertions beyond realAssertionsEnd _must_ be introduced by + // removeITEs(). + int realAssertionsEnd = d_assertionsToCheck.size(); + + // Remove ITEs, updating d_iteSkolemMap + removeITEs(); - // Remove ITEs - removeITEs(); // This may need to be in a try-catch - // block. make regress is passing, so - // skipping for now --K + // begin: INVARIANT to maintain: no reordering of assertions or + // introducing new ones + int iteRewriteAssertionsEnd = d_assertionsToCheck.size(); Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; @@ -1061,7 +1064,13 @@ void SmtEnginePrivate::processAssertions() { d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); } - // TODO: send formulas and iteSkolemMap to decision engine + // Push the formula to decision engine + Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); + d_smt.d_decisionEngine->addAssertions + (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap); + + // end: INVARIANT to maintain: no reordering of assertions or + // introducing new ones // Push the formula to SAT for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0a0778ebc..5c73da1f6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -25,6 +25,7 @@ #include #include +#include "decision/decision_engine.h" #include "expr/node.h" #include "expr/command.h" #include "prop/prop_engine.h" @@ -77,6 +78,9 @@ class TheoryEngine { /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; + /** Access to decision engine */ + DecisionEngine* d_decisionEngine; + /** Our context */ context::Context* d_context; @@ -430,26 +434,42 @@ class TheoryEngine { Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr()); } - // Remove the ITEs and assert to prop engine + // Remove the ITEs std::vector additionalLemmas; IteSkolemMap iteSkolemMap; additionalLemmas.push_back(node); RemoveITE::run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + + // assert to prop engine d_propEngine->assertLemma(additionalLemmas[0], negated, removable); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); d_propEngine->assertLemma(additionalLemmas[i], false, removable); } + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + if(negated) { + // Can't we just get rid of passing around this 'negated' stuff? + // Is it that hard for the propEngine to figure that out itself? + // (I like the use of triple negation .) --K + additionalLemmas[0] = additionalLemmas[0].notNode(); + negated = false; + } + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. + + // assert to decision engine + if(!removable) + d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); + // Mark that we added some lemmas d_lemmasAdded = true; // Lemma analysis isn't online yet; this lemma may only live for this // user level. - Node finalForm = - negated ? additionalLemmas[0].notNode() : additionalLemmas[0]; - return theory::LemmaStatus(finalForm, d_userContext->getLevel()); + return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); } /** Time spent in theory combination */ @@ -485,6 +505,11 @@ public: d_propEngine = propEngine; } + inline void setDecisionEngine(DecisionEngine* decisionEngine) { + Assert(d_decisionEngine == NULL); + d_decisionEngine = decisionEngine; + } + /** * Get a pointer to the underlying propositional engine. */ diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 248ce4efa..7327d4a64 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -33,16 +33,20 @@ class RemoveITE { public: /** - * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions. - * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new - * Boolean ite created in conjunction with that skolem variable. + * Removes the ITE nodes by introducing skolem variables. All + * additional assertions are pushed into assertions. iteSkolemMap + * contains a map from introduced skolem variables to the index in + * assertions containing the new Boolean ite created in conjunction + * with that skolem variable. */ static void run(std::vector& assertions, IteSkolemMap& iteSkolemMap); /** - * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions. - * iteSkolemMap contains a map from introduced skolem variables to the index in assertions containing the new - * Boolean ite created in conjunction with that skolem variable. + * Removes the ITE from the node by introducing skolem + * variables. All additional assertions are pushed into + * assertions. iteSkolemMap contains a map from introduced skolem + * variables to the index in assertions containing the new Boolean + * ite created in conjunction with that skolem variable. */ static Node run(TNode node, std::vector& additionalAssertions, IteSkolemMap& iteSkolemMap);