From: Gereon Kremer Date: Fri, 29 Oct 2021 00:28:29 +0000 (-0700) Subject: Remove static access to options in decision folder (#7527) X-Git-Tag: cvc5-1.0.0~934 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;ds=sidebyside;h=70b7384838d1e9c99bdbd26d40feab3463eb0ebd;p=cvc5.git Remove static access to options in decision folder (#7527) This PR replaces static accesses to options (options::foo()) by using the options object provided via the environment. --- diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp index 120fc730b..261d78fdf 100644 --- a/src/decision/decision_engine_old.cpp +++ b/src/decision/decision_engine_old.cpp @@ -30,7 +30,7 @@ DecisionEngineOld::DecisionEngineOld(Env& env) d_result(context(), SAT_VALUE_UNKNOWN), d_engineState(0), d_enabledITEStrategy(nullptr), - d_decisionStopOnly(options::decisionMode() + d_decisionStopOnly(options().decision.decisionMode == options::DecisionMode::STOPONLY_OLD) { Trace("decision") << "Creating decision engine" << std::endl; @@ -39,11 +39,11 @@ DecisionEngineOld::DecisionEngineOld(Env& env) Trace("decision-init") << "DecisionEngineOld::init()" << std::endl; Trace("decision-init") << " * options->decisionMode: " - << options::decisionMode() << std::endl; + << options().decision.decisionMode << std::endl; Trace("decision-init") << " * decisionStopOnly: " << d_decisionStopOnly << std::endl; - if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) + if (options().decision.decisionMode == options::DecisionMode::JUSTIFICATION) { d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this)); } diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index e04de9ce1..cadb107c3 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -62,10 +62,11 @@ JustificationHeuristic::~JustificationHeuristic() {} cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch) { - if(options::decisionThreshold() > 0) { + if (options().decision.decisionThreshold > 0) + { bool stopSearchTmp = false; prop::SatLiteral lit = - getNextThresh(stopSearchTmp, options::decisionThreshold()); + getNextThresh(stopSearchTmp, options().decision.decisionThreshold); if (lit != prop::undefSatLiteral) { Assert(stopSearchTmp == false); @@ -252,7 +253,7 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satV DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity) { - if (options::decisionWeightInternal() + if (options().decision.decisionWeightInternal != options::DecisionWeightInternal::USR1) { return getWeight(n); @@ -304,15 +305,16 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity DecisionWeight JustificationHeuristic::getWeight(TNode n) { if(!n.hasAttribute(DecisionWeightAttr()) ) { options::DecisionWeightInternal combiningFn = - options::decisionWeightInternal(); + options().decision.decisionWeightInternal; if (combiningFn == options::DecisionWeightInternal::OFF || n.getNumChildren() == 0) { - if (options::decisionRandomWeight() != 0) + if (options().decision.decisionRandomWeight != 0) { n.setAttribute(DecisionWeightAttr(), - Random::getRandom().pick(0, options::decisionRandomWeight()-1)); + Random::getRandom().pick( + 0, options().decision.decisionRandomWeight - 1)); } } else if (combiningFn == options::DecisionWeightInternal::MAX) @@ -340,7 +342,8 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { typedef std::vector ChildList; TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { - if(options::decisionUseWeight()) { + if (options().decision.decisionUseWeight) + { // TODO: Optimize storing & access if(d_childCache.find(n) == d_childCache.end()) { ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end()); @@ -349,7 +352,9 @@ TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { d_childCache[n] = make_pair(list0, list1); } return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i]; - } else { + } + else + { return n[i]; } } @@ -612,8 +617,10 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN TNode node2, SatValue desiredVal2) { - if(options::decisionUseWeight() && - getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { + if (options().decision.decisionUseWeight + && getWeightPolarized(node1, desiredVal1) + > getWeightPolarized(node2, desiredVal2)) + { std::swap(node1, node2); std::swap(desiredVal1, desiredVal2); } @@ -637,8 +644,10 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TN TNode node2, SatValue desiredVal2) { - if(options::decisionUseWeight() && - getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { + if (options().decision.decisionUseWeight + && getWeightPolarized(node1, desiredVal1) + > getWeightPolarized(node2, desiredVal2)) + { std::swap(node1, node2); std::swap(desiredVal1, desiredVal2); } @@ -673,13 +682,17 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod 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)) - ) { + } + else if (trueChildVal == invertValue(desiredVal) + || falseChildVal == desiredVal + || (options().decision.decisionUseWeight + && getWeightPolarized(node[1], true) + > getWeightPolarized(node[2], false))) + { ifDesiredVal = SAT_VALUE_FALSE; - } else { + } + else + { ifDesiredVal = SAT_VALUE_TRUE; } diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 303f1a63b..fbba2e33a 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -150,7 +150,7 @@ private: int getPrvsIndex(); DecisionWeight getWeightPolarized(TNode n, bool polarity); DecisionWeight getWeightPolarized(TNode n, prop::SatValue); - static DecisionWeight getWeight(TNode); + DecisionWeight getWeight(TNode); bool compareByWeightFalse(TNode, TNode); bool compareByWeightTrue(TNode, TNode); TNode getChildByWeight(TNode n, int i, bool polarity); diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index d65936964..bced3d662 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -28,18 +28,19 @@ JustificationStrategy::JustificationStrategy(Env& env) d_assertions( userContext(), context(), - options::jhRlvOrder()), // assertions are user-context dependent + options() + .decision.jhRlvOrder), // assertions are user-context dependent d_skolemAssertions( context(), context()), // skolem assertions are SAT-context dependent d_justified(context()), d_stack(context()), d_lastDecisionLit(context()), d_currStatusDec(false), - d_useRlvOrder(options::jhRlvOrder()), - d_decisionStopOnly(options::decisionMode() + d_useRlvOrder(options().decision.jhRlvOrder), + d_decisionStopOnly(options().decision.decisionMode == options::DecisionMode::STOPONLY), - d_jhSkMode(options::jhSkolemMode()), - d_jhSkRlvMode(options::jhSkolemRlvMode()) + d_jhSkMode(options().decision.jhSkolemMode), + d_jhSkRlvMode(options().decision.jhSkolemRlvMode) { }