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.

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 72e7d7e689e0dfd57c25f40da7367ab83e3fb4ec..272914c25231cd76210830f9b5bf1c1726535b63 100644 (file)
--- 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 0dc704219515cfd947cf409f973ce1acf8685a8b..1d2f9a322f882134cd6cdd6ff4a6224ad2616b73 100644 (file)
--- 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<rt_types.size(); i++ ){
 
@@ -1812,11 +1813,17 @@ void TermGenEnv::collectSignatureInformation() {
     }
   }
   //shuffle functions
-  for( std::map< TypeNode, std::vector< TNode > >::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<TypeNode, std::vector<TNode> >::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; i<it->second.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 cfcfcc5a5859b45e567de3ebd7d11b4321087c96..6784fb8e3a2ad67cfcea61f7fed068bc80d894c3 100644 (file)
--- 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 d1217d01df0ca5178d5644f4b4bff2e0eda9c9cd..c262c77e521784f4cff3a14195d169e788e23c18 100644 (file)
--- 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<Node> 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 4fe3cfbed0a938797aa8de2e3f12c5fa04eb4fb5..bd9274f918634b29e5b474544daf214d3cfe60df 100644 (file)
--- 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 86c569a4a4a65a28e126ce51a6d867245b3b70ad..7c6abd33e5889531143bca006092590a913b389e 100644 (file)
--- 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 480271c03ec906916d8b15a95be9ee6fb6c86081..e746666fc43a260f8e708af48decdf22167d0570 100644 (file)
--- 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: