From: Aina Niemetz Date: Fri, 17 Nov 2017 17:44:13 +0000 (-0800) Subject: Add random number generator. (#1370) X-Git-Tag: cvc5-1.0.0~5467 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40b04572d72ed5c46b85ec3cd06e5654efaa6d33;p=cvc5.git 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). --- 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()); } diff --git a/src/options/main_options b/src/options/main_options index e47f55746..1793cae2d 100644 --- a/src/options/main_options +++ b/src/options/main_options @@ -18,6 +18,9 @@ common-option - --show-config void :handler showConfiguration 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e82a337c..d703e8e83 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -102,6 +102,7 @@ #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; @@ -1289,6 +1290,7 @@ void SmtEngine::setLogicInternal() throw() { } void SmtEngine::setDefaults() { + Random::getRandom().setSeed(options::seed()); // Language-based defaults if (!options::bitvectorDivByZeroConst.wasSetByUser()) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a3e2d8ee4..c9a220566 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -70,6 +70,7 @@ #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" @@ -82,7 +83,6 @@ namespace theory { namespace arith { static Node toSumNode(const ArithVariables& vars, const DenseMap& sum); -static double fRand(double fMin, double fMax); static bool complexityBelow(const DenseMap& row, uint32_t cap); @@ -147,8 +147,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_div_skolem(u), d_int_div_skolem(u) { - srand(79); - if( options::nlExt() ){ d_nonlinearExtension = new NonlinearExtension( containing, d_congruenceManager.getEqualityEngine()); @@ -2203,11 +2201,12 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em 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(); } } @@ -4804,12 +4803,6 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C 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); @@ -4821,10 +4814,11 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex 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){ diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index 687f05f47..97cded35c 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -19,6 +19,7 @@ #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; @@ -1385,7 +1386,7 @@ Node CegConjecturePbe::constructBestSolvedConditional( std::vector< Node >& solv 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; @@ -1399,7 +1400,7 @@ Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs, 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; diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 7502d42f1..d58fa2f1e 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -26,6 +26,7 @@ #include "theory/arith/theory_arith_private.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" +#include "util/random.h" #include #include @@ -1114,7 +1115,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, 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")) diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 027abce64..33218dbe9 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -44,6 +44,8 @@ libutil_la_SOURCES = \ resource_manager.cpp \ resource_manager.h \ result.cpp \ + random.h \ + random.cpp \ result.h \ safe_print.cpp \ safe_print.h \ diff --git a/src/util/random.cpp b/src/util/random.cpp new file mode 100644 index 000000000..aca7756ae --- /dev/null +++ b/src/util/random.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \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 +#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; +} + +} diff --git a/src/util/random.h b/src/util/random.h new file mode 100644 index 000000000..9083c63e4 --- /dev/null +++ b/src/util/random.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \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