Fix RNG for seed = 0. (#1459)

The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0.

diff --git a/src/util/random.cpp b/src/util/random.cpp
index aca7756ae9d6b99517caeda59dd1b8b8670734b9..d10fb2eec66f9a69f5c1d703764b83dcdb36eb23 100644 (file)
--- a/src/util/random.cpp
+++ b/src/util/random.cpp
@@ -31,8 +31,7 @@ uint64_t Random::rand()
   d_state ^= d_state >> 12;
   d_state ^= d_state << 25;
   d_state ^= d_state >> 27;
-  d_state *= uint64_t{2685821657736338717};
-  return d_state;
+  return d_state * uint64_t{2685821657736338717};
 }
 
 uint64_t Random::pick(uint64_t from, uint64_t to)

diff --git a/src/util/random.h b/src/util/random.h
index 9083c63e416384020bdddcbacec1a8e96a5bb02e..1e837642e5040ab6764d43c907bf698a4378ac8b 100644 (file)
--- a/src/util/random.h
+++ b/src/util/random.h
@@ -28,7 +28,7 @@ namespace CVC4 {
 class Random
 {
  public:
-  Random(uint64_t seed) : d_seed(seed), d_state(seed) {}
+  Random(uint64_t seed) { setSeed(seed); }
 
   /* Get current RNG (singleton).  */
   static Random& getRandom()
@@ -40,8 +40,8 @@ class Random
   /* Set seed of Random.  */
   void setSeed(uint64_t seed)
   {
-    d_seed = seed;
-    d_state = seed;
+    d_seed = seed == 0 ? ~seed : seed;
+    d_state = d_seed;
   }
 
   /* Next random uint64_t number. */