From 90ffa8b4eb26af9060e57be7fe5d6008717d3ce6 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 9 Oct 2018 10:36:40 -0700 Subject: [PATCH] Random: support URNG interface (#2595) Use std::shuffle (with Random as the unified random generator) instead of std::random_shuffle for deterministic, reproducable random shuffling. --- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 2 +- .../quantifiers/conjecture_generator.cpp | 17 ++++++--- .../ematching/inst_strategy_e_matching.cpp | 14 +++++--- src/theory/quantifiers/sygus/sygus_unif.cpp | 2 +- .../quantifiers/sygus/sygus_unif_io.cpp | 3 +- src/util/random.cpp | 10 ++++++ src/util/random.h | 35 ++++++++++++------- 7 files changed, 59 insertions(+), 24 deletions(-) diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 72e7d7e68..272914c25 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -302,7 +302,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // this helps robustness, since picking the same literal every time may // lead to a stream of value instantiations, whereas with randomization // we may find an invertible literal that leads to a useful instantiation. - std::random_shuffle(iti->second.begin(), iti->second.end()); + std::shuffle(iti->second.begin(), iti->second.end(), Random::getRandom()); if (Trace.isOn("cegqi-bv")) { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 0dc704219..1d2f9a322 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" +#include "util/random.h" using namespace CVC4; using namespace CVC4::kind; @@ -773,7 +774,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) d_tge.d_var_id[ it->first ] = it->second; d_tge.d_var_limit[ it->first ] = it->second; } - std::random_shuffle( rt_types.begin(), rt_types.end() ); + std::shuffle(rt_types.begin(), rt_types.end(), Random::getRandom()); std::map< TypeNode, std::vector< Node > > conj_rhs; for( unsigned i=0; i >::iterator it = d_typ_tg_funcs.begin(); it != d_typ_tg_funcs.end(); ++it ){ - std::random_shuffle( it->second.begin(), it->second.end() ); - if( it->first.isNull() ){ + for (std::map >::iterator it = + d_typ_tg_funcs.begin(); + it != d_typ_tg_funcs.end(); + ++it) + { + std::shuffle(it->second.begin(), it->second.end(), Random::getRandom()); + if (it->first.isNull()) + { Trace("sg-gen-tg-debug") << "In this order : "; - for( unsigned i=0; isecond.size(); i++ ){ + for (unsigned i = 0; i < it->second.size(); i++) + { Trace("sg-gen-tg-debug") << it->second[i] << " "; } Trace("sg-gen-tg-debug") << std::endl; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index cfcfcc5a5..6784fb8e3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" +#include "util/random.h" using namespace std; @@ -453,10 +454,15 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ return; } } - //if we are re-generating triggers, shuffle based on some method - if( d_made_multi_trigger[f] ){ - std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly - }else{ + // if we are re-generating triggers, shuffle based on some method + if (d_made_multi_trigger[f]) + { + std::shuffle(patTerms.begin(), + patTerms.end(), + Random::getRandom()); // shuffle randomly + } + else + { d_made_multi_trigger[f] = true; } //will possibly want to get an old trigger diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index d1217d01d..c262c77e5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -79,7 +79,7 @@ Node SygusUnif::constructBestStringToConcat( { Assert(!strs.empty()); std::vector strs_tmp = strs; - std::random_shuffle(strs_tmp.begin(), strs_tmp.end()); + std::shuffle(strs_tmp.begin(), strs_tmp.end(), Random::getRandom()); // prefer one that has incremented by more than 0 for (const Node& ns : strs_tmp) { diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 4fe3cfbed..bd9274f91 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1143,7 +1143,8 @@ Node SygusUnifIo::constructSol( // try a random strategy if (snode.d_strats.size() > 1) { - std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); + std::shuffle( + snode.d_strats.begin(), snode.d_strats.end(), Random::getRandom()); } // ITE always first if we have not yet solved // the reasoning is that splitting on conditions only subdivides the problem diff --git a/src/util/random.cpp b/src/util/random.cpp index 86c569a4a..7c6abd33e 100644 --- a/src/util/random.cpp +++ b/src/util/random.cpp @@ -23,6 +23,16 @@ namespace CVC4 { +Random::Random(uint64_t seed) { setSeed(seed); } + +void Random::setSeed(uint64_t seed) +{ + d_seed = seed == 0 ? ~seed : seed; + d_state = d_seed; +} + +uint64_t Random::operator()() { return rand(); } + uint64_t Random::rand() { /* xorshift* generator (see S. Vigna, An experimental exploration of diff --git a/src/util/random.h b/src/util/random.h index 480271c03..e746666fc 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -26,29 +26,40 @@ namespace CVC4 { class Random { public: - Random(uint64_t seed) { setSeed(seed); } + using result_type = uint64_t; - /* Get current RNG (singleton). */ + /** Constructor. */ + Random(uint64_t seed); + + /** Get current RNG (singleton). */ static Random& getRandom() { static thread_local Random s_current(0); return s_current; } - /* Set seed of Random. */ - void setSeed(uint64_t seed) - { - d_seed = seed == 0 ? ~seed : seed; - d_state = d_seed; - } + /** Get the minimum number that can be picked. */ + static uint64_t min() { return 0u; } + + /** Get the maximum number that can be picked. */ + static uint64_t max() { return UINT64_MAX; } + + /** Set seed of Random. */ + void setSeed(uint64_t seed); - /* Next random uint64_t number. */ + /** Operator overload to pick random uin64_t number (see rand()). */ + uint64_t operator()(); + + /** Next random uint64_t number. */ uint64_t rand(); - /* Pick random uint64_t number between from and to (inclusive). */ + + /** 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). */ + + /** Pick random double number between from and to (inclusive). */ double pickDouble(double from, double to); - /* Pick with given probability (yes / no). */ + + /** Pick with given probability (yes / no). */ bool pickWithProb(double probability); private: -- 2.30.2