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.

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<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 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<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 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: