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).
#include "theory/rewriter.h"
#include "smt/term_formula_removal.h"
#include "smt/smt_statistics_registry.h"
+#include "util/random.h"
namespace CVC4 {
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());
}
common-option - --copyright void :handler copyright
show CVC4 copyright information
+common-option seed -s --seed uint64_t :default 0
+ seed for random number generator
+
option - --show-debug-tags void :handler showDebugTags
show all available tags for debugging
option - --show-trace-tags void :handler showTraceTags
#include "theory/theory_traits.h"
#include "util/hash.h"
#include "util/proof.h"
+#include "util/random.h"
#include "util/resource_manager.h"
using namespace std;
}
void SmtEngine::setDefaults() {
+ Random::getRandom().setSeed(options::seed());
// Language-based defaults
if (!options::bitvectorDivByZeroConst.wasSetByUser())
{
#include "theory/valuation.h"
#include "util/dense_map.h"
#include "util/integer.h"
+#include "util/random.h"
#include "util/rational.h"
#include "util/result.h"
#include "util/statistics_registry.h"
namespace arith {
static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
-static double fRand(double fMin, double fMax);
static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
d_div_skolem(u),
d_int_div_skolem(u)
{
- srand(79);
-
if( options::nlExt() ){
d_nonlinearExtension = new NonlinearExtension(
containing, d_congruenceManager.getEqualityEngine());
if(!options::trySolveIntStandardEffort()){ return false; }
- if (d_lastContextIntegerAttempted <= (level >> 2)){
-
- double d = (double)(d_solveIntMaybeHelp + 1) / (d_solveIntAttempts + 1 + level*level);
- double t = fRand(0.0, 1.0);
- if(t < d){
+ if (d_lastContextIntegerAttempted <= (level >> 2))
+ {
+ double d = (double)(d_solveIntMaybeHelp + 1)
+ / (d_solveIntAttempts + 1 + level * level);
+ if (Random::getRandom().pickWithProb(d))
+ {
return getSolveIntegerResource();
}
}
return false;
}
-double fRand(double fMin, double fMax)
-{
- double f = (double)rand() / RAND_MAX;
- return fMin + f * (fMax - fMin);
-}
-
bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
uint32_t rowLength = d_tableau.getRowLength(ridx);
Debug("arith::prop")
<< "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl;
- if(rowLength >= options::arithPropagateMaxLength()){
- if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
- return false;
- }
+ if (rowLength >= options::arithPropagateMaxLength()
+ && Random::getRandom().pickWithProb(
+ 1.0 - double(options::arithPropagateMaxLength()) / rowLength))
+ {
+ return false;
}
if(hasCount.lowerBoundCount() == rowLength){
#include "theory/quantifiers/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "util/random.h"
using namespace CVC4;
using namespace CVC4::kind;
Node CegConjecturePbe::constructBestConditional( std::vector< Node >& conds, UnifContext& x ) {
Assert( !conds.empty() );
// TODO
- double r = (double)(rand())/((double)(RAND_MAX));
+ double r = Random::getRandom().pickDouble(0.0, 1.0);
unsigned cindex = r*conds.size();
if( cindex>conds.size() ){
cindex = conds.size() - 1;
UnifContext& x ) {
Assert( !strs.empty() );
// TODO
- double r = (double)(rand())/((double)(RAND_MAX));
+ double r = Random::getRandom().pickDouble(0.0, 1.0);
unsigned cindex = r*strs.size();
if( cindex>strs.size() ){
cindex = strs.size() - 1;
#include "theory/arith/theory_arith_private.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/bitvector.h"
+#include "util/random.h"
#include <algorithm>
#include <stack>
if( iti!=d_var_to_inst_id.end() ){
Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
// if interleaving, do not do inversion half the time
- if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) {
+ if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5))
+ {
bool firstVar = sf.empty();
// get inst id list
if (Trace.isOn("cegqi-bv"))
resource_manager.cpp \
resource_manager.h \
result.cpp \
+ random.h \
+ random.cpp \
result.h \
safe_print.cpp \
safe_print.h \
--- /dev/null
+/********************* */
+/*! \file random.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A Random Number Generator.
+ **
+ ** A random number generator, 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).
+ **/
+
+#include "util/random.h"
+
+#include <cfloat>
+#include "base/cvc4_assert.h"
+
+namespace CVC4 {
+
+uint64_t Random::rand()
+{
+ /* 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). */
+ d_state ^= d_state >> 12;
+ d_state ^= d_state << 25;
+ d_state ^= d_state >> 27;
+ d_state *= uint64_t{2685821657736338717};
+ return d_state;
+}
+
+uint64_t Random::pick(uint64_t from, uint64_t to)
+{
+ Assert(from <= to);
+ Assert(to < UINT64_MAX);
+ return (Random::rand() % (to - from + 1)) + from;
+}
+
+double Random::pickDouble(double from, double to)
+{
+ Assert(from <= to);
+ Assert(to <= DBL_MAX);
+ return Random::rand() * (to - from) + from;
+}
+
+bool Random::pickWithProb(double probability)
+{
+ Assert(probability <= 1);
+ uint64_t p = (uint64_t) (probability * 1000);
+ uint64_t r = pick(0, 999);
+ return r < p;
+}
+
+}
--- /dev/null
+/********************* */
+/*! \file random.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A Random Number Generator.
+ **
+ ** A random number generator, 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).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL__RANDOM_H
+#define __CVC4__UTIL__RANDOM_H
+
+#include "base/tls.h"
+
+namespace CVC4 {
+
+class Random
+{
+ public:
+ Random(uint64_t seed) : d_seed(seed), d_state(seed) {}
+
+ /* Get current RNG (singleton). */
+ static Random& getRandom()
+ {
+ static CVC4_THREAD_LOCAL Random s_current(0);
+ return s_current;
+ }
+
+ /* Set seed of Random. */
+ void setSeed(uint64_t seed)
+ {
+ d_seed = seed;
+ d_state = seed;
+ }
+
+ /* Next random uint64_t number. */
+ uint64_t rand();
+ /* Pick random uint64_t number between from and to (inclusive). */
+ uint64_t pick(uint64_t from, uint64_t to);
+ /* Pick random double number between from and to (inclusive). */
+ double pickDouble(double from, double to);
+ /* Pick with given probability (yes / no). */
+ bool pickWithProb(double probability);
+
+ private:
+ /* The seed of the RNG. */
+ uint64_t d_seed;
+ /* The current state of the RNG. */
+ uint64_t d_state;
+};
+
+} // namespace CVC4
+#endif
projects / cvc5.git / commitdiff