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).

3 files changed, 126 insertions, 0 deletions

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 <cfloat>
+#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