diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.h | 1 | ||||
-rw-r--r-- | src/decision/decision_mode.h | 9 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 346 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 58 | ||||
-rw-r--r-- | src/decision/options | 12 | ||||
-rw-r--r-- | src/decision/options_handlers.h | 13 |
6 files changed, 367 insertions, 72 deletions
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, "<<threshold<<")" << std::endl; TimerStat::CodeTimer codeTimer(d_timestat); d_visited.clear(); + d_curThreshold = threshold; if(Trace.isOn("justified")) { for(JustifiedSet::key_iterator i = d_justified.key_begin(); @@ -71,7 +92,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { } } - for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { + for(unsigned i = getPrvsIndex(); i < d_assertions.size(); ++i) { Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl; // Sanity check: if it was false, aren't we inconsistent? @@ -83,7 +104,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { litDecision = findSplitter(d_assertions[i], desiredVal); if(litDecision != undefSatLiteral) { - d_prvsIndex = i; + setPrvsIndex(i); return litDecision; } } @@ -104,12 +125,13 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { << d_assertions[i] << std::endl; } } - Assert(alljustified); + Assert(alljustified || d_curThreshold != 0); #endif // SAT solver can stop... stopSearch = true; - d_decisionEngine->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<DecisionWeight>::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<DecisionWeight>::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<DecisionWeight>::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<TNode> 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<pair<TNode,TNode> > IteList; typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache; + typedef std::vector<TNode> ChildList; + typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache; typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; + typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache; // being 'justified' is monotonic with respect to decisions typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet; JustifiedSet d_justified; + typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold; + ExploredThreshold d_exploredThreshold; context::CDO<unsigned> d_prvsIndex; + context::CDO<unsigned> 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 */ |