diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-11-17 09:44:13 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-17 09:44:13 -0800 |
commit | 40b04572d72ed5c46b85ec3cd06e5654efaa6d33 (patch) | |
tree | ab2220a5fe9935778c510ce56a0bfdad2d96afe6 /src/util | |
parent | 6c6f4e23aea405a812b1c6a3dd4d80696eb34741 (diff) |
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).
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/random.cpp | 60 | ||||
-rw-r--r-- | src/util/random.h | 64 |
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 |