From: Kshitij Bansal Date: Fri, 26 Apr 2013 22:02:02 +0000 (-0400) Subject: Merge experimental decisionweight branch X-Git-Tag: cvc5-1.0.0~7309^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d090726fcd1cf86422da4a747ad1b97852b7e6bc;p=cvc5.git Merge experimental decisionweight branch None of these are enabled by default, so any performance impact counts as a bug Options added are: --decision-threshold=N :default 0 + ignore all nodes greater than threshold in first attempt to pick decision --decision-use-weight bool :default false + use the weight nodes (locally, by looking at children) to direct recursive search --decision-random-weight=N int :default 0 + assign random weights to nodes between 0 and N-1 (0: disable) --decision-weight-internal=HOW + computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) Squashed commit of the following: commit 0dbae066c19abde37092517b50f23255398539db Author: Kshitij Bansal Date: Fri Apr 26 16:42:36 2013 -0400 contentless cleanup commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e Author: Kshitij Bansal Date: Tue Apr 16 21:43:55 2013 -0400 bugfixes in usr1 auto weight computation commit 9f039cba805bfd722466734920e758d48ae3b23e Author: Kshitij Bansal Date: Fri Mar 29 15:01:33 2013 -0400 DECISION_WEIGHT_INTERNAL_USR1 commit 744e16d514594e5f1c69b36473b03cf501d9b9d1 Author: Kshitij Bansal Date: Wed Mar 27 11:05:43 2013 -0400 split theory and decision requests commit f379d8a821df31c74b42a7722e891abc5c944f16 Author: Kshitij Bansal Date: Wed Mar 27 09:51:58 2013 -0400 fix potential bug with threshold commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12 Author: Kshitij Bansal Date: Wed Feb 27 20:29:38 2013 -0500 stat bv::weightComputationTimer commit 2ab97d063e221357d2bb017af4589105777fd5a3 Author: Kshitij Bansal Date: Sat Feb 23 17:02:43 2013 -0500 decision: option to auto compute weight of boolean structure commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8 Author: Kshitij Bansal Date: Sat Feb 23 14:53:50 2013 -0500 decision: fix design to do partial explorations * make findSplitterRec and all related helper functions' return type trivalued, to be able to distinguish between "partial exploration" vs "done exploration but found nothing" * keep additional data structure to remember to what extent the partial exploration has been completed so not to repeat it. we can use this to make multiple passes on formula with arbritrary order of thresholds for exploration commit 0815991fc1b0f1d63f0e8124d4672d782e89d671 Author: lianah Date: Fri Feb 22 17:55:40 2013 -0500 added simple node weight computation for bv. commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3 Author: Kshitij Bansal Date: Wed Feb 20 02:35:21 2013 -0500 --decision-use-weight, --decision-random-weight=N commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2 Author: Kshitij Bansal Date: Tue Feb 19 23:36:49 2013 -0500 decisionThreshold option commit ac3579a52e452e3118ce116ff1823d6c6885544b Author: Kshitij Bansal Date: Tue Feb 19 20:22:51 2013 -0500 DecisionWeightAttr --- diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 5d7c5ea74..bc071f7f6 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 "theory/decision_attributes.h" #include "util/ite_removal.h" #include "util/output.h" diff --git a/src/decision/decision_mode.h b/src/decision/decision_mode.h index 335e6279e..20743cba1 100644 --- a/src/decision/decision_mode.h +++ b/src/decision/decision_mode.h @@ -46,6 +46,15 @@ enum DecisionMode { };/* enum DecisionMode */ + +/** Enumeration of combining functions for computing internal weights */ +enum DecisionWeightInternal { + DECISION_WEIGHT_INTERNAL_OFF, + DECISION_WEIGHT_INTERNAL_MAX, + DECISION_WEIGHT_INTERNAL_SUM, + DECISION_WEIGHT_INTERNAL_USR1 +};/* enum DecisionInternalWeight */ + }/* CVC4::decision namespace */ std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC; diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 28d26adb1..de49f6e0a 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -22,6 +22,7 @@ #include "expr/node_manager.h" #include "expr/kind.h" #include "theory/rewriter.h" +#include "decision/options.h" #include "util/ite_removal.h" @@ -32,7 +33,9 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c): ITEDecisionStrategy(de, c), d_justified(c), + d_exploredThreshold(c), d_prvsIndex(c, 0), + d_threshPrvsIndex(c, 0), d_helfulness("decision::jh::helpfulness", 0), d_giveup("decision::jh::giveup", 0), d_timestat("decision::jh::time"), @@ -41,7 +44,10 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_iteCache(uc), d_visited(), d_visitedComputeITE(), - d_curDecision() { + d_curDecision(), + d_curThreshold(0), + d_childCache(uc), + d_weightCache(uc) { StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_giveup); StatisticsRegistry::registerStat(&d_timestat); @@ -54,11 +60,26 @@ JustificationHeuristic::~JustificationHeuristic() { StatisticsRegistry::unregisterStat(&d_timestat); } -CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { - Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; +CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) +{ + if(options::decisionThreshold() > 0) { + bool stopSearchTmp = false; + SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold()); + if(lit != undefSatLiteral) { + Assert(stopSearchTmp == false); + return lit; + } + Assert(stopSearchTmp == true); + } + return getNextThresh(stopSearch, 0); +} + +CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, DecisionWeight threshold) { + Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<setResult(SAT_VALUE_TRUE); + if(d_curThreshold == 0) + d_decisionEngine->setResult(SAT_VALUE_TRUE); return prop::undefSatLiteral; } @@ -164,6 +186,8 @@ void JustificationHeuristic::addAssertions d_iteAssertions[i->first] = assertions[i->second]; } + + // Automatic weight computation } SatLiteral JustificationHeuristic::findSplitter(TNode node, @@ -187,6 +211,139 @@ bool JustificationHeuristic::checkJustified(TNode n) return d_justified.find(n) != d_justified.end(); } +DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n) +{ + return + d_exploredThreshold.find(n) == d_exploredThreshold.end() ? + numeric_limits::max() : d_exploredThreshold[n]; +} + +void JustificationHeuristic::setExploredThreshold(TNode n) +{ + d_exploredThreshold[n] = d_curThreshold; +} + +int JustificationHeuristic::getPrvsIndex() +{ + if(d_curThreshold == 0) + return d_prvsIndex; + else + return d_threshPrvsIndex; +} + +void JustificationHeuristic::setPrvsIndex(int prvsIndex) +{ + if(d_curThreshold == 0) + d_prvsIndex = prvsIndex; + else + d_threshPrvsIndex = prvsIndex; +} + +DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satValue) +{ + Assert(satValue == SAT_VALUE_TRUE || satValue == SAT_VALUE_FALSE); + return getWeightPolarized(n, satValue == SAT_VALUE_TRUE); +} + +DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity) +{ + if(options::decisionWeightInternal() != DECISION_WEIGHT_INTERNAL_USR1) { + return getWeight(n); + } + + if(d_weightCache.find(n) == d_weightCache.end()) { + Kind k = n.getKind(); + theory::TheoryId tId = theory::kindToTheoryId(k); + DecisionWeight dW1, dW2; + if(tId != theory::THEORY_BOOL) { + dW1 = dW2 = getWeight(n); + } else { + + if(k == kind::OR) { + dW1 = numeric_limits::max(), dW2 = 0; + for(TNode::iterator i=n.begin(); i != n.end(); ++i) { + dW1 = min(dW1, getWeightPolarized(*i, true)); + dW2 = max(dW2, getWeightPolarized(*i, false)); + } + } else if(k == kind::AND) { + dW1 = 0, dW2 = numeric_limits::max(); + for(TNode::iterator i=n.begin(); i != n.end(); ++i) { + dW1 = max(dW1, getWeightPolarized(*i, true)); + dW2 = min(dW2, getWeightPolarized(*i, false)); + } + } else if(k == kind::IMPLIES) { + dW1 = min(getWeightPolarized(n[0], false), + getWeightPolarized(n[1], true)); + dW2 = max(getWeightPolarized(n[0], true), + getWeightPolarized(n[1], false)); + } else if(k == kind::NOT) { + dW1 = getWeightPolarized(n[0], false); + dW2 = getWeightPolarized(n[0], true); + } else { + dW1 = 0; + for(TNode::iterator i=n.begin(); i != n.end(); ++i) { + dW1 = max(dW1, getWeightPolarized(*i, true)); + dW1 = max(dW1, getWeightPolarized(*i, false)); + } + dW2 = dW1; + } + + } + d_weightCache[n] = make_pair(dW1, dW2); + } + return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second; +} + +DecisionWeight JustificationHeuristic::getWeight(TNode n) { + if(!n.hasAttribute(theory::DecisionWeightAttr()) ) { + + DecisionWeightInternal combiningFn = + options::decisionWeightInternal(); + + if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) { + + if(options::decisionRandomWeight() != 0) { + n.setAttribute(theory::DecisionWeightAttr(), rand() % options::decisionRandomWeight()); + } + + } else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) { + + DecisionWeight dW = 0; + for(TNode::iterator i=n.begin(); i != n.end(); ++i) + dW = max(dW, getWeight(*i)); + n.setAttribute(theory::DecisionWeightAttr(), dW); + + } else if(combiningFn == DECISION_WEIGHT_INTERNAL_SUM || + combiningFn == DECISION_WEIGHT_INTERNAL_USR1) { + DecisionWeight dW = 0; + for(TNode::iterator i=n.begin(); i != n.end(); ++i) + dW = max(dW, getWeight(*i)); + n.setAttribute(theory::DecisionWeightAttr(), dW); + + } else { + Unreachable(); + } + + } + return n.getAttribute(theory::DecisionWeightAttr()); +} + +typedef vector ChildList; +TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { + if(options::decisionUseWeight()) { + // TODO: Optimize storing & access + if(d_childCache.find(n) == d_childCache.end()) { + ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end()); + std::sort(list0.begin(), list0.end(), JustificationHeuristic::myCompareClass(this,false)); + std::sort(list1.begin(), list1.end(), JustificationHeuristic::myCompareClass(this,true)); + d_childCache[n] = make_pair(list0, list1); + } + return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i]; + } else { + return n[i]; + } +} + SatValue JustificationHeuristic::tryGetSatValue(Node n) { Debug("decision") << " " << n << " has sat value " << " "; @@ -233,8 +390,8 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l) } } -bool JustificationHeuristic::findSplitterRec(TNode node, - SatValue desiredVal) +JustificationHeuristic::SearchResult +JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) { /** * Main idea @@ -258,7 +415,12 @@ bool JustificationHeuristic::findSplitterRec(TNode node, /* Base case */ if (checkJustified(node)) { Debug("decision::jh") << " justified, returning" << std::endl; - return false; + return NO_SPLITTER; + } + if (getExploredThreshold(node) < d_curThreshold) { + Debug("decision::jh") << " explored, returning" << std::endl; + Assert(d_curThreshold != 0); + return DONT_KNOW; } #if defined CVC4_ASSERTIONS || defined CVC4_DEBUG @@ -298,23 +460,25 @@ bool JustificationHeuristic::findSplitterRec(TNode node, if(tId != theory::THEORY_BOOL) { // if node has embedded ites, resolve that first - if(handleEmbeddedITEs(node)) - return true; + if(handleEmbeddedITEs(node) == FOUND_SPLITTER) + return FOUND_SPLITTER; if(litVal != SAT_VALUE_UNKNOWN) { setJustified(node); - return false; + return NO_SPLITTER; } else { Assert(d_decisionEngine->hasSatLiteral(node)); - SatVariable v = + if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold) + return DONT_KNOW; + SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - return true; + return FOUND_SPLITTER; } } - bool ret = false; + SearchResult ret = NO_SPLITTER; switch (k) { case kind::CONST_BOOLEAN: @@ -365,65 +529,108 @@ bool JustificationHeuristic::findSplitterRec(TNode node, break; }//end of switch(k) - if(ret == false) { - Assert(litPresent == false || litVal == desiredVal, + if(ret == DONT_KNOW) { + setExploredThreshold(node); + } + + if(ret == NO_SPLITTER) { + Assert( litPresent == false || litVal == desiredVal, "Output should be justified"); setJustified(node); } return ret; }/* findRecSplit method */ -bool JustificationHeuristic::handleAndOrEasy(TNode node, - SatValue desiredVal) +JustificationHeuristic::SearchResult +JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) { Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); int numChildren = node.getNumChildren(); SatValue desiredValInverted = invertValue(desiredVal); - for(int i = 0; i < numChildren; ++i) - if ( tryGetSatValue(node[i]) != desiredValInverted ) - return findSplitterRec(node[i], desiredVal); - Assert(false, "handleAndOrEasy: No controlling input found"); - return false; + for(int i = 0; i < numChildren; ++i) { + TNode curNode = getChildByWeight(node, i, desiredVal); + if ( tryGetSatValue(curNode) != desiredValInverted ) { + SearchResult ret = findSplitterRec(curNode, desiredVal); + if(ret != DONT_KNOW) + return ret; + } + } + Assert(d_curThreshold != 0, "handleAndOrEasy: No controlling input found"); + return DONT_KNOW; } -bool JustificationHeuristic::handleAndOrHard(TNode node, +JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); int numChildren = node.getNumChildren(); - for(int i = 0; i < numChildren; ++i) - if (findSplitterRec(node[i], desiredVal)) - return true; - return false; + bool noSplitter = true; + for(int i = 0; i < numChildren; ++i) { + TNode curNode = getChildByWeight(node, i, desiredVal); + SearchResult ret = findSplitterRec(curNode, desiredVal); + if (ret == FOUND_SPLITTER) + return FOUND_SPLITTER; + noSplitter = noSplitter && (ret == NO_SPLITTER); + } + return noSplitter ? NO_SPLITTER : DONT_KNOW; } -bool JustificationHeuristic::handleBinaryEasy(TNode node1, +JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2) { - if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) - return findSplitterRec(node1, desiredVal1); - if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) - return findSplitterRec(node2, desiredVal2); - Assert(false, "handleBinaryEasy: No controlling input found"); - return false; + if(options::decisionUseWeight() && + getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { + swap(node1, node2); + swap(desiredVal1, desiredVal2); + } + + if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) { + SearchResult ret = findSplitterRec(node1, desiredVal1); + if(ret != DONT_KNOW) + return ret; + } + if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) { + SearchResult ret = findSplitterRec(node2, desiredVal2); + if(ret != DONT_KNOW) + return ret; + } + Assert(d_curThreshold != 0, "handleBinaryEasy: No controlling input found"); + return DONT_KNOW; } -bool JustificationHeuristic::handleBinaryHard(TNode node1, +JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2) { - if( findSplitterRec(node1, desiredVal1) ) - return true; - return findSplitterRec(node2, desiredVal2); + if(options::decisionUseWeight() && + getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { + swap(node1, node2); + swap(desiredVal1, desiredVal2); + } + + bool noSplitter = true; + SearchResult ret; + + ret = findSplitterRec(node1, desiredVal1); + if (ret == FOUND_SPLITTER) + return FOUND_SPLITTER; + noSplitter &= (ret == NO_SPLITTER); + + ret = findSplitterRec(node2, desiredVal2); + if (ret == FOUND_SPLITTER) + return FOUND_SPLITTER; + noSplitter &= (ret == NO_SPLITTER); + + return noSplitter ? NO_SPLITTER : DONT_KNOW; } -bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) +JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) { Debug("decision::jh") << " handleITE (" << node << ", " << desiredVal << std::endl; @@ -431,48 +638,59 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) //[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 [CHOICE] - SatValue ifDesiredVal = - (tryGetSatValue(node[2]) == desiredVal || - tryGetSatValue(node[1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(node[0], ifDesiredVal)) return true; + SatValue trueChildVal = tryGetSatValue(node[1]); + SatValue falseChildVal = tryGetSatValue(node[2]); + SatValue ifDesiredVal; + + if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) { + ifDesiredVal = SAT_VALUE_TRUE; + } else if(trueChildVal == invertValue(desiredVal) || + falseChildVal == desiredVal || + (options::decisionUseWeight() && + getWeightPolarized(node[1], true) > getWeightPolarized(node[2], false)) + ) { + ifDesiredVal = SAT_VALUE_FALSE; + } else { + ifDesiredVal = SAT_VALUE_TRUE; + } + + if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER) + return FOUND_SPLITTER; - Assert(false, "No controlling input found (6)"); + Assert(d_curThreshold != 0, "No controlling input found (6)"); + return DONT_KNOW; } else { // Try to justify 'if' - if(findSplitterRec(node[0], ifVal)) return true; + if(findSplitterRec(node[0], ifVal) == FOUND_SPLITTER) + return FOUND_SPLITTER; // If that was successful, we need to go into only one of 'then' // or 'else' int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; - // STALE code: remove after tests or mar 2013, whichever earlier - // int chVal = tryGetSatValue(node[ch]); - // Assert(chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal); - // end STALE code: remove - - if( findSplitterRec(node[ch], desiredVal) ) { - return true; + if( findSplitterRec(node[ch], desiredVal) == FOUND_SPLITTER ) { + return FOUND_SPLITTER; } + + return NO_SPLITTER; }// else (...ifVal...) - return false; } -bool JustificationHeuristic::handleEmbeddedITEs(TNode node) +JustificationHeuristic::SearchResult JustificationHeuristic::handleEmbeddedITEs(TNode node) { const IteList l = getITEs(node); Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl; + bool noSplitter = true; for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { if(d_visited.find((*i).first) == d_visited.end()) { d_visited.insert((*i).first); - if(findSplitterRec((*i).second, SAT_VALUE_TRUE)) - return true; + SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE); + if (ret == FOUND_SPLITTER) + return FOUND_SPLITTER; + noSplitter = noSplitter && (ret == NO_SPLITTER); d_visited.erase((*i).first); } } - return false; + return noSplitter ? NO_SPLITTER : DONT_KNOW; } diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 503f6c2af..01458d9ea 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -37,14 +37,23 @@ namespace CVC4 { namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { + // TRUE FALSE MEH + enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW}; + typedef std::vector > IteList; typedef context::CDHashMap IteCache; + typedef std::vector ChildList; + typedef context::CDHashMap,TNodeHashFunction> ChildCache; typedef context::CDHashMap SkolemMap; + typedef context::CDHashMap,TNodeHashFunction> WeightCache; // being 'justified' is monotonic with respect to decisions typedef context::CDHashSet JustifiedSet; JustifiedSet d_justified; + typedef context::CDHashMap ExploredThreshold; + ExploredThreshold d_exploredThreshold; context::CDO d_prvsIndex; + context::CDO d_threshPrvsIndex; IntStat d_helfulness; IntStat d_giveup; @@ -80,6 +89,26 @@ class JustificationHeuristic : public ITEDecisionStrategy { /** current decision for the recursive call */ SatLiteral d_curDecision; + /** current threshold for the recursive call */ + DecisionWeight d_curThreshold; + + /** child cache */ + ChildCache d_childCache; + + /** computed polarized weight cache */ + WeightCache d_weightCache; + + + class myCompareClass { + JustificationHeuristic* d_jh; + bool d_b; + public: + myCompareClass(JustificationHeuristic* jh, bool b):d_jh(jh),d_b(b) {}; + bool operator() (TNode n1, TNode n2) { + return d_jh->getWeightPolarized(n1, d_b) < d_jh->getWeightPolarized(n2, d_b); + } + }; + public: JustificationHeuristic(CVC4::DecisionEngine* de, context::UserContext *uc, @@ -94,17 +123,30 @@ public: IteSkolemMap iteSkolemMap); private: + /* getNext with an option to specify threshold */ + prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold); + SatLiteral findSplitter(TNode node, SatValue desiredVal); /** * Do all the hard work. */ - bool findSplitterRec(TNode node, SatValue value); + SearchResult findSplitterRec(TNode node, SatValue value); /* Helper functions */ void setJustified(TNode); bool checkJustified(TNode); - + DecisionWeight getExploredThreshold(TNode); + void setExploredThreshold(TNode); + void setPrvsIndex(int); + int getPrvsIndex(); + DecisionWeight getWeightPolarized(TNode n, bool polarity); + DecisionWeight getWeightPolarized(TNode n, SatValue); + static DecisionWeight getWeight(TNode); + bool compareByWeightFalse(TNode, TNode); + bool compareByWeightTrue(TNode, TNode); + TNode getChildByWeight(TNode n, int i, bool polarity); + /* If literal exists corresponding to the node return that. Otherwise an UNKNOWN */ SatValue tryGetSatValue(Node n); @@ -115,14 +157,14 @@ private: /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); - bool handleAndOrEasy(TNode node, SatValue desiredVal); - bool handleAndOrHard(TNode node, SatValue desiredVal); - bool handleBinaryEasy(TNode node1, SatValue desiredVal1, + SearchResult handleAndOrEasy(TNode node, SatValue desiredVal); + SearchResult handleAndOrHard(TNode node, SatValue desiredVal); + SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2); - bool handleBinaryHard(TNode node1, SatValue desiredVal1, + SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2); - bool handleITE(TNode node, SatValue desiredVal); - bool handleEmbeddedITEs(TNode node); + SearchResult handleITE(TNode node, SatValue desiredVal); + SearchResult handleEmbeddedITEs(TNode node); };/* class JustificationHeuristic */ }/* namespace decision */ diff --git a/src/decision/options b/src/decision/options index 7e457f125..b86577e7b 100644 --- a/src/decision/options +++ b/src/decision/options @@ -20,4 +20,16 @@ option decisionMustRelevancy bool # only use DE to determine when to stop, not to make decisions option decisionStopOnly bool +expert-option decisionThreshold --decision-threshold=N decision::DecisionWeight :default 0 :include "theory/decision_attributes.h" + ignore all nodes greater than threshold in first attempt to pick decision + +expert-option decisionUseWeight --decision-use-weight bool :default false + use the weight nodes (locally, by looking at children) to direct recursive search + +expert-option decisionRandomWeight --decision-random-weight=N int :default 0 + assign random weights to nodes between 0 and N-1 (0: disable) + +expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::decision::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "decision/options_handlers.h" + computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) + endmodule diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index 1d4321614..05d975ef1 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -107,6 +107,19 @@ inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEn } } +inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "off") + return DECISION_WEIGHT_INTERNAL_OFF; + else if(optarg == "max") + return DECISION_WEIGHT_INTERNAL_MAX; + else if(optarg == "sum") + return DECISION_WEIGHT_INTERNAL_SUM; + else if(optarg == "usr1") + return DECISION_WEIGHT_INTERNAL_USR1; + else + throw OptionException(std::string("--decision-weight-internal must be off, max or sum.")); +} + }/* CVC4::decision namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index c7f1780b6..6196ca357 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -458,9 +458,8 @@ Lit Solver::pickBranchLit() } #endif /* CVC4_REPLAY */ - // Theory/DE requests - bool stopSearch = false; - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch)); + // Theory requests + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; @@ -469,12 +468,21 @@ Lit Solver::pickBranchLit() } else { Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; } - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest(stopSearch)); + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); } + Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl; + + // DE requests + bool stopSearch = false; + nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch)); if(stopSearch) { return lit_Undef; } - Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl; + if(nextLit != lit_Undef) { + Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value"); + decisions++; + return nextLit; + } Var next = var_Undef; diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index a6908ff52..c9f19b42e 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -79,15 +79,12 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) { d_queue.push(literalNode); } -SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { +SatLiteral TheoryProxy::getNextTheoryDecisionRequest() { TNode n = d_theoryEngine->getNextDecisionRequest(); - if(not n.isNull()) { - return d_cnfStream->getLiteral(n); - } + return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n); +} - // If theory doesn't give us a deicsion ask the decision engine. It - // may return in undefSatLiteral in which case the sat solver uses - // whatever default heuristic it has. +SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) { Assert(d_decisionEngine != NULL); Assert(stopSearch != true); SatLiteral ret = d_decisionEngine->getNext(stopSearch); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 5f1ea0e23..7b0aa2058 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -93,7 +93,9 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); - SatLiteral getNextDecisionRequest(bool& stopSearch); + SatLiteral getNextTheoryDecisionRequest(); + + SatLiteral getNextDecisionEngineRequest(bool& stopSearch); bool theoryNeedCheck() const; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index ad62ade38..8579012ab 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -108,6 +108,13 @@ void Bitblaster::bbAtom(TNode node) { } } +uint64_t Bitblaster::computeAtomWeight(TNode node) { + node = node.getKind() == kind::NOT? node[0] : node; + + Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); + uint64_t size = utils::numNodes(atom_bb); + return size; +} void Bitblaster::bbTerm(TNode node, Bits& bits) { diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 2c52a2670..c122c407d 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -165,6 +165,7 @@ public: } bool isSharedTerm(TNode node); + uint64_t computeAtomWeight(TNode node); private: diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 997244c40..2308f36a3 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -19,6 +19,8 @@ #include "theory/bv/theory_bv_utils.h" #include "theory/bv/bitblaster.h" #include "theory/bv/options.h" +#include "theory/decision_attributes.h" +#include "decision/options.h" using namespace std; using namespace CVC4; @@ -58,7 +60,12 @@ void BitblastSolver::preRegister(TNode node) { if (options::bitvectorEagerBitblast()) { d_bitblaster->bbAtom(node); } else { + CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer); d_bitblastQueue.push_back(node); + if ((options::decisionUseWeight() || options::decisionThreshold() != 0) && + !node.hasAttribute(theory::DecisionWeightAttr())) { + node.setAttribute(theory::DecisionWeightAttr(), d_bitblaster->computeAtomWeight(node)); + } } } } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 433223308..c597cb083 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -78,13 +78,15 @@ TheoryBV::Statistics::Statistics(): d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), d_solveTimer("theory::bv::solveTimer"), d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0), - d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0) + d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0), + d_weightComputationTimer("theory::bv::weightComputationTimer") { StatisticsRegistry::registerStat(&d_avgConflictSize); StatisticsRegistry::registerStat(&d_solveSubstitutions); StatisticsRegistry::registerStat(&d_solveTimer); StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort); StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort); + StatisticsRegistry::registerStat(&d_weightComputationTimer); } TheoryBV::Statistics::~Statistics() { @@ -93,6 +95,7 @@ TheoryBV::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_solveTimer); StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort); StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort); + StatisticsRegistry::unregisterStat(&d_weightComputationTimer); } @@ -205,6 +208,7 @@ void TheoryBV::propagate(Effort e) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; // temporary fix for incremental bit-blasting if (d_valuation.isSatLiteral(literal)) { + Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n"; ok = d_out->propagate(literal); } } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8b184f972..481493e13 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -78,6 +78,7 @@ private: TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; IntStat d_numCallsToCheckStandardEffort; + TimerStat d_weightComputationTimer; Statistics(); ~Statistics(); }; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index dffdf10df..174df03ab 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -23,7 +23,7 @@ #include #include #include "expr/node_manager.h" - +#include "theory/decision_attributes.h" namespace CVC4 { @@ -493,6 +493,26 @@ inline T gcd(T a, T b) { } +typedef __gnu_cxx::hash_set TNodeSet; + +inline uint64_t numNodesAux(TNode node, TNodeSet& seen) { + if (seen.find(node) != seen.end()) + return 0; + + uint64_t size = 1; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + size += numNodesAux(node[i], seen); + } + seen.insert(node); + return size; +} + +inline uint64_t numNodes(TNode node) { + TNodeSet seen; + uint64_t size = numNodesAux(node, seen); + return size; +} + } } } diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h new file mode 100644 index 000000000..204362a2a --- /dev/null +++ b/src/theory/decision_attributes.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file decision_attributes.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Rewriter attributes + ** + ** Rewriter attributes. + **/ + +#ifndef __CVC4__THEORY__DECISION_ATRRIBUTES +#define __CVC4__THEORY__DECISION_ATRRIBUTES + +#include "expr/attribute.h" + +namespace CVC4 { +namespace decision { +typedef uint64_t DecisionWeight; +} +namespace theory { +namespace attr { + struct DecisionWeightTag {}; +}/* CVC4::theory::attr namespace */ + +typedef expr::Attribute DecisionWeightAttr; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__DECISION_ATRRIBUTES */ diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 5d3fe371e..dbd9547a9 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -20,6 +20,7 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ fuzz01.smt \ + fuzz02.delta01.smt \ fuzz02.smt \ fuzz03.smt \ fuzz04.smt \ diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2 new file mode 100644 index 000000000..1feb32c7f --- /dev/null +++ b/test/regress/regress0/bv/decision-weight00.smt2 @@ -0,0 +1,19 @@ +(set-option :produce-models true) +(set-logic QF_BV) +(set-info :source | + Patrice Godefroid, SAGE (systematic dynamic test generation) + For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unknown) +(declare-fun x () (_ BitVec 32)) +(declare-fun y () (_ BitVec 32)) +(declare-fun z () (_ BitVec 4)) +(assert (or + (= x (bvmul x y)) + (and (= x y) + (not (= ((_ extract 2 2) x) ((_ extract 2 2) z)))) + )) +(check-sat) +(exit) diff --git a/test/regress/regress0/bv/fuzz02.delta01.smt b/test/regress/regress0/bv/fuzz02.delta01.smt new file mode 100644 index 000000000..1ef924ef1 --- /dev/null +++ b/test/regress/regress0/bv/fuzz02.delta01.smt @@ -0,0 +1,18 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v2 BitVec[9])) +:status unsat +:formula +(let (?n1 bv0[2]) +(let (?n2 bv0[6]) +(flet ($n3 (bvult v2 v2)) +(let (?n4 bv1[1]) +(let (?n5 bv0[1]) +(let (?n6 (ite $n3 ?n4 ?n5)) +(let (?n7 (concat ?n2 ?n6)) +(let (?n8 bv0[7]) +(let (?n9 (bvcomp ?n7 ?n8)) +(let (?n10 (zero_extend[1] ?n9)) +(flet ($n11 (= ?n1 ?n10)) +$n11 +))))))))))))