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

9 files changed, 169 insertions, 38 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index d0d2b39c9..a60f2c365 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -24,6 +24,7 @@
 #include "theory/rewriter.h"
 #include "smt/term_formula_removal.h"
 #include "smt/smt_statistics_registry.h"
+#include "util/random.h"
 
 namespace CVC4 {
 
@@ -298,33 +299,35 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
 DecisionWeight JustificationHeuristic::getWeight(TNode n) {
   if(!n.hasAttribute(DecisionWeightAttr()) ) {
 
-    DecisionWeightInternal combiningFn =
-      options::decisionWeightInternal();
+    DecisionWeightInternal combiningFn = options::decisionWeightInternal();
 
-    if(combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0) {
-
-      if(options::decisionRandomWeight() != 0) {
-        n.setAttribute(DecisionWeightAttr(), rand() % options::decisionRandomWeight());
+    if (combiningFn == DECISION_WEIGHT_INTERNAL_OFF || n.getNumChildren() == 0)
+    {
+      if (options::decisionRandomWeight() != 0)
+      {
+        n.setAttribute(DecisionWeightAttr(),
+            Random::getRandom().pick(0, options::decisionRandomWeight()-1));
       }
-
-    } else if(combiningFn == DECISION_WEIGHT_INTERNAL_MAX) {
-
+    }
+    else if (combiningFn == DECISION_WEIGHT_INTERNAL_MAX)
+    {
       DecisionWeight dW = 0;
-      for(TNode::iterator i=n.begin(); i != n.end(); ++i)
+      for (TNode::iterator i = n.begin(); i != n.end(); ++i)
         dW = max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
-
-    } else if(combiningFn == DECISION_WEIGHT_INTERNAL_SUM ||
-              combiningFn == DECISION_WEIGHT_INTERNAL_USR1) {
+    }
+    else if (combiningFn == DECISION_WEIGHT_INTERNAL_SUM
+             || combiningFn == DECISION_WEIGHT_INTERNAL_USR1)
+    {
       DecisionWeight dW = 0;
-      for(TNode::iterator i=n.begin(); i != n.end(); ++i)
+      for (TNode::iterator i = n.begin(); i != n.end(); ++i)
         dW = max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
-
-    } else {
+    }
+    else
+    {
       Unreachable();
     }
-
   }
   return n.getAttribute(DecisionWeightAttr());
 }
diff --git a/src/options/main_options b/src/options/main_options
index e47f55746..1793cae2d 100644
--- a/src/options/main_options
+++ b/src/options/main_options
@@ -18,6 +18,9 @@ common-option - --show-config void :handler showConfiguration
 common-option - --copyright void :handler copyright
  show CVC4 copyright information
 
+common-option seed -s --seed uint64_t :default 0
+ seed for random number generator
+
 option - --show-debug-tags void :handler showDebugTags
  show all available tags for debugging
 option - --show-trace-tags void :handler showTraceTags
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3e82a337c..d703e8e83 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -102,6 +102,7 @@
 #include "theory/theory_traits.h"
 #include "util/hash.h"
 #include "util/proof.h"
+#include "util/random.h"
 #include "util/resource_manager.h"
 
 using namespace std;
@@ -1289,6 +1290,7 @@ void SmtEngine::setLogicInternal() throw() {
 }
 
 void SmtEngine::setDefaults() {
+  Random::getRandom().setSeed(options::seed());
   // Language-based defaults
   if (!options::bitvectorDivByZeroConst.wasSetByUser())
   {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a3e2d8ee4..c9a220566 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -70,6 +70,7 @@
 #include "theory/valuation.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
+#include "util/random.h"
 #include "util/rational.h"
 #include "util/result.h"
 #include "util/statistics_registry.h"
@@ -82,7 +83,6 @@ namespace theory {
 namespace arith {
 
 static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
-static double fRand(double fMin, double fMax);
 static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
 
 
@@ -147,8 +147,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_div_skolem(u),
   d_int_div_skolem(u)
 {
-  srand(79);
-  
   if( options::nlExt() ){
     d_nonlinearExtension = new NonlinearExtension(
         containing, d_congruenceManager.getEqualityEngine());
@@ -2203,11 +2201,12 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em
 
   if(!options::trySolveIntStandardEffort()){ return false; }
 
-  if (d_lastContextIntegerAttempted <= (level >> 2)){
-
-    double d = (double)(d_solveIntMaybeHelp + 1) / (d_solveIntAttempts + 1 + level*level);
-    double t = fRand(0.0, 1.0);
-    if(t < d){
+  if (d_lastContextIntegerAttempted <= (level >> 2))
+  {
+    double d = (double)(d_solveIntMaybeHelp + 1)
+               / (d_solveIntAttempts + 1 + level * level);
+    if (Random::getRandom().pickWithProb(d))
+    {
       return getSolveIntegerResource();
     }
   }
@@ -4804,12 +4803,6 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
   return false;
 }
 
-double fRand(double fMin, double fMax)
-{
-  double f = (double)rand() / RAND_MAX;
-  return fMin + f * (fMax - fMin);
-}
-
 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
   uint32_t rowLength = d_tableau.getRowLength(ridx);
@@ -4821,10 +4814,11 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   Debug("arith::prop")
     << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
 
-  if(rowLength >= options::arithPropagateMaxLength()){
-    if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
-      return false;
-    }
+  if (rowLength >= options::arithPropagateMaxLength()
+      && Random::getRandom().pickWithProb(
+             1.0 - double(options::arithPropagateMaxLength()) / rowLength))
+  {
+    return false;
   }
 
   if(hasCount.lowerBoundCount() == rowLength){
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp
index 687f05f47..97cded35c 100644
--- a/src/theory/quantifiers/ce_guided_pbe.cpp
+++ b/src/theory/quantifiers/ce_guided_pbe.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "util/random.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -1385,7 +1386,7 @@ Node CegConjecturePbe::constructBestSolvedConditional( std::vector< Node >& solv
 Node CegConjecturePbe::constructBestConditional( std::vector< Node >& conds, UnifContext& x ) {
   Assert( !conds.empty() );
   // TODO
-  double r = (double)(rand())/((double)(RAND_MAX));
+  double r = Random::getRandom().pickDouble(0.0, 1.0);
   unsigned cindex = r*conds.size();
   if( cindex>conds.size() ){
     cindex = conds.size() - 1;
@@ -1399,7 +1400,7 @@ Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs,
                                                     UnifContext& x ) {
   Assert( !strs.empty() );
   // TODO
-  double r = (double)(rand())/((double)(RAND_MAX));
+  double r = Random::getRandom().pickDouble(0.0, 1.0);
   unsigned cindex = r*strs.size();
   if( cindex>strs.size() ){
     cindex = strs.size() - 1;
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 7502d42f1..d58fa2f1e 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -26,6 +26,7 @@
 #include "theory/arith/theory_arith_private.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
+#include "util/random.h"
 
 #include <algorithm>
 #include <stack>
@@ -1114,7 +1115,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
   if( iti!=d_var_to_inst_id.end() ){
     Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
     // if interleaving, do not do inversion half the time
-    if (!options::cbqiBvInterleaveValue() || rand() % 2 == 0) {
+    if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5))
+    {
       bool firstVar = sf.empty();
       // get inst id list
       if (Trace.isOn("cegqi-bv"))
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