diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/decision | |
parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff) |
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.cpp | 5 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 17 |
2 files changed, 12 insertions, 10 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 679dd6cc6..dc798626e 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -18,7 +18,6 @@ #include "decision/decision_attributes.h" #include "decision/justification_heuristic.h" #include "expr/node.h" -#include "options/decision_mode.h" #include "options/decision_options.h" #include "options/smt_options.h" @@ -53,8 +52,8 @@ void DecisionEngine::init() Trace("decision-init") << " * options->decisionStopOnly: " << options::decisionStopOnly() << std::endl; - if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { } - if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) { + if (options::decisionMode() == options::DecisionMode::JUSTIFICATION) + { ITEDecisionStrategy* ds = new decision::JustificationHeuristic(this, d_userContext, d_satContext); enableStrategy(ds); diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index f7e5b84fc..a6b6cbd8f 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -248,7 +248,9 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satV DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity) { - if(options::decisionWeightInternal() != DECISION_WEIGHT_INTERNAL_USR1) { + if (options::decisionWeightInternal() + != options::DecisionWeightInternal::USR1) + { return getWeight(n); } @@ -297,10 +299,11 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity DecisionWeight JustificationHeuristic::getWeight(TNode n) { if(!n.hasAttribute(DecisionWeightAttr()) ) { + options::DecisionWeightInternal combiningFn = + options::decisionWeightInternal(); - DecisionWeightInternal combiningFn = options::decisionWeightInternal(); - - if (combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) + if (combiningFn == options::DecisionWeightInternal::OFF + || n.getNumChildren() == 0) { if (options::decisionRandomWeight() != 0) { @@ -308,15 +311,15 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { Random::getRandom().pick(0, options::decisionRandomWeight()-1)); } } - else if (combiningFn == DECISION_WEIGHT_INTERNAL_MAX) + else if (combiningFn == options::DecisionWeightInternal::MAX) { DecisionWeight dW = 0; for (TNode::iterator i = n.begin(); i != n.end(); ++i) dW = max(dW, getWeight(*i)); n.setAttribute(DecisionWeightAttr(), dW); } - else if (combiningFn == DECISION_WEIGHT_INTERNAL_SUM - || combiningFn == DECISION_WEIGHT_INTERNAL_USR1) + else if (combiningFn == options::DecisionWeightInternal::SUM + || combiningFn == options::DecisionWeightInternal::USR1) { DecisionWeight dW = 0; for (TNode::iterator i = n.begin(); i != n.end(); ++i) |