diff options
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 389 |
1 files changed, 206 insertions, 183 deletions
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; i<n.getNumChildren(); ++i) { + SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); + if(it2 != d_iteAssertions.end()) + l.push_back(it2->second); + 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<TNode>(); + 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<bool>() == false || desiredVal == SAT_VALUE_TRUE); + Assert(node.getConst<bool>() == 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 */ |