diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-11-17 09:44:13 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-17 09:44:13 -0800 |
commit | 40b04572d72ed5c46b85ec3cd06e5654efaa6d33 (patch) | |
tree | ab2220a5fe9935778c510ce56a0bfdad2d96afe6 /src/decision | |
parent | 6c6f4e23aea405a812b1c6a3dd4d80696eb34741 (diff) |
Add random number generator. (#1370)
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index d0d2b39c9..a60f2c365 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -24,6 +24,7 @@ #include "theory/rewriter.h" #include "smt/term_formula_removal.h" #include "smt/smt_statistics_registry.h" +#include "util/random.h" namespace CVC4 { @@ -298,33 +299,35 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity DecisionWeight JustificationHeuristic::getWeight(TNode n) { if(!n.hasAttribute(DecisionWeightAttr()) ) { - DecisionWeightInternal combiningFn = - options::decisionWeightInternal(); + DecisionWeightInternal combiningFn = options::decisionWeightInternal(); - if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) { - - if(options::decisionRandomWeight() != 0) { - n.setAttribute(DecisionWeightAttr(), rand() % options::decisionRandomWeight()); + if (combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) + { + if (options::decisionRandomWeight() != 0) + { + n.setAttribute(DecisionWeightAttr(), + Random::getRandom().pick(0, options::decisionRandomWeight()-1)); } - - } else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) { - + } + else if (combiningFn == DECISION_WEIGHT_INTERNAL_MAX) + { DecisionWeight dW = 0; - for(TNode::iterator i=n.begin(); i != n.end(); ++i) + 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 == DECISION_WEIGHT_INTERNAL_SUM + || combiningFn == DECISION_WEIGHT_INTERNAL_USR1) + { DecisionWeight dW = 0; - for(TNode::iterator i=n.begin(); i != n.end(); ++i) + for (TNode::iterator i = n.begin(); i != n.end(); ++i) dW = max(dW, getWeight(*i)); n.setAttribute(DecisionWeightAttr(), dW); - - } else { + } + else + { Unreachable(); } - } return n.getAttribute(DecisionWeightAttr()); } |