diff options
Diffstat (limited to 'src/decision/relevancy.cpp')
-rw-r--r-- | src/decision/relevancy.cpp | 376 |
1 files changed, 376 insertions, 0 deletions
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp new file mode 100644 index 000000000..c5e1f7fbc --- /dev/null +++ b/src/decision/relevancy.cpp @@ -0,0 +1,376 @@ +/********************* */ +/*! \file relevancy.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Justification heuristic for decision making + ** + ** A ATGP-inspired justification-based decision heuristic. See + ** [insert reference] for more details. This code is, or not, based + ** on the CVC3 implementation of the same heuristic -- note below. + ** + ** It needs access to the simplified but non-clausal formula. + **/ +/*****************************************************************************/ + +#include "relevancy.h" + +#include "expr/node_manager.h" +#include "expr/kind.h" +#include "theory/rewriter.h" +#include "util/ite_removal.h" + +// Relevancy stuff + +void Relevancy::setJustified(TNode n) +{ + Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; + d_justified.insert(n); + if(d_opt.computeRelevancy) { + d_relevancy[n] = d_maxRelevancy[n]; + updateRelevancy(n); + } +} + +bool Relevancy::checkJustified(TNode n) +{ + return d_justified.find(n) != d_justified.end(); +} + +SatValue Relevancy::tryGetSatValue(Node n) +{ + 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 Relevancy::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); + } +} + +const IteList& Relevancy::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 Relevancy::findSplitterRec(TNode node, + SatValue desiredVal) +{ + Trace("decision") + << "findSplitterRec([" << node.getId() << "]" << node << ", " + << desiredVal << ", .. )" << std::endl; + + ++d_expense; + + /* Handle NOT as a special case */ + while (node.getKind() == kind::NOT) { + desiredVal = invertValue(desiredVal); + node = node[0]; + } + + /* Avoid infinite loops */ + if(d_visited.find(node) != d_visited.end()) { + Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl; + Assert(false); + Assert(node.getKind() == kind::ITE); + return false; + } + + /* Base case */ + if(checkJustified(node)) { + return false; + } + + /** + * If we have already explored the subtree for some desiredVal, we + * skip this and continue exploring the rest + */ + if(d_polarityCache.find(node) == d_polarityCache.end()) { + d_polarityCache[node] = desiredVal; + } else { + Assert(d_multipleBacktrace || d_opt.computeRelevancy); + return true; + } + + d_visited.insert(node); + +#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; + } + } + //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"); + + /* Good luck, hope you can get what you want */ + Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, + "invariant voilated"); + + /* What type of node is this */ + Kind k = node.getKind(); + theory::TheoryId tId = theory::kindToTheoryId(k); + + /* Some debugging stuff */ + 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. + */ + if(tId != theory::THEORY_BOOL + // && !(k == kind::EQUAL && node[0].getType().isBoolean()) + ) { + + // 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; + 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(d_visited.find(node) != d_visited.end() ) continue; + if(findSplitterRec(l[i], SAT_VALUE_TRUE)) { + d_visited.erase(node); + return true; + } + } + Debug("jh-ite") << " ite done " << l.size() << std::endl; + + if(litVal != SAT_VALUE_UNKNOWN) { + d_visited.erase(node); + 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(); + *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); + Trace("decision") << "decision " << *d_curDecision << std::endl; + Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; + d_visited.erase(node); + return true; + } + } + + bool ret = false; + SatValue flipCaseVal = 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); + break; + + case kind::AND: + if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE); + else ret = handleOrFalse(node, SAT_VALUE_TRUE); + break; + + case kind::OR: + if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE); + else ret = handleOrTrue(node, SAT_VALUE_TRUE); + break; + + case kind::IMPLIES: + Assert(node.getNumChildren() == 2, "Expected 2 fanins"); + if (desiredVal == SAT_VALUE_FALSE) { + ret = findSplitterRec(node[0], SAT_VALUE_TRUE); + if(ret) break; + ret = findSplitterRec(node[1], SAT_VALUE_FALSE); + break; + } + else { + if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) { + ret = findSplitterRec(node[0], SAT_VALUE_FALSE); + //if(!ret || !d_multipleBacktrace) + break; + } + if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) { + ret = findSplitterRec(node[1], SAT_VALUE_TRUE); + break; + } + Assert(d_multipleBacktrace, "No controlling input found (3)"); + } + break; + + case kind::XOR: + flipCaseVal = SAT_VALUE_TRUE; + case kind::IFF: { + SatValue val = tryGetSatValue(node[0]); + if (val != SAT_VALUE_UNKNOWN) { + ret = findSplitterRec(node[0], val); + if (ret) break; + if (desiredVal == flipCaseVal) val = invertValue(val); + ret = findSplitterRec(node[1], val); + } + else { + val = tryGetSatValue(node[1]); + if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE; + if (desiredVal == flipCaseVal) val = invertValue(val); + ret = findSplitterRec(node[0], val); + if(ret) break; + Assert(false, "Unable to find controlling input (4)"); + } + break; + } + + case kind::ITE: + ret = handleITE(node, desiredVal); + break; + + default: + Assert(false, "Unexpected Boolean operator"); + break; + }//end of switch(k) + + d_visited.erase(node); + if(ret == false) { + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); + setJustified(node); + } + return ret; + + Unreachable(); +}/* findRecSplit method */ + +bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) { + Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", " + << desiredVal << std::endl; + + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or + (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); + + int n = node.getNumChildren(); + bool ret = false; + for(int i = 0; i < n; ++i) { + if (findSplitterRec(node[i], desiredVal)) { + if(!d_opt.computeRelevancy) + return true; + else + ret = true; + } + } + return ret; +} + +bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) { + Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", " + << desiredVal << std::endl; + + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or + (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); + + int n = node.getNumChildren(); + SatValue desiredValInverted = invertValue(desiredVal); + for(int i = 0; i < n; ++i) { + if ( tryGetSatValue(node[i]) != desiredValInverted ) { + // PRE RELEVANCY return findSplitterRec(node[i], desiredVal); + bool ret = findSplitterRec(node[i], desiredVal); + if(ret) { + // Splitter could be found... so can't justify this node + if(!d_multipleBacktrace) + return true; + } + else { + // Splitter couldn't be found... should be justified + return false; + } + } + } + // Multiple backtrace is on, so must have reached here because + // everything had splitter + if(d_multipleBacktrace) return true; + + 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"); + return false; +} + +bool Relevancy::handleITE(TNode node, SatValue desiredVal) +{ + Debug("jh-findSplitterRec") << " handleITE (" << node << ", " + << desiredVal << std::endl; + + //[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)) return true; + + Assert(false, "No controlling input found (6)"); + } else { + + // Try to justify 'if' + if(findSplitterRec(node[0], ifVal)) 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) ) { + return true; + } + }// else (...ifVal...) + return false; +}//handleITE |