Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A random number generator, based on the Mersenne-Twister engine.
      11                 :            :  */
      12                 :            : 
      13                 :            : #ifndef CVC5__UTIL__RANDOM_H
      14                 :            : #define CVC5__UTIL__RANDOM_H
      15                 :            : 
      16                 :            : #include <random>
      17                 :            : #include <type_traits>
      18                 :            : 
      19                 :            : #include "base/check.h"
      20                 :            : #include "cvc5_private.h"
      21                 :            : 
      22                 :            : #ifdef CVC5_GMP_IMP
      23                 :            : #include <gmpxx.h>
      24                 :            : #endif
      25                 :            : #ifdef CVC5_CLN_IMP
      26                 :            : #include <cln/random.h>
      27                 :            : #endif
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :            : class Random
      32                 :            : {
      33                 :            :  public:
      34                 :            :   using result_type = uint64_t;
      35                 :            : 
      36                 :            :   /** Constructor. */
      37                 :            :   Random(uint64_t seed);
      38                 :            :   /** Destructor. */
      39                 :            :   ~Random();
      40                 :            : 
      41                 :            :   Random(const Random& rng) = delete;
      42                 :            :   Random& operator=(const Random& rng) = delete;
      43                 :            : 
      44                 :            :   /** Get current RNG (singleton).  */
      45                 :    4900030 :   static Random& getRandom()
      46                 :            :   {
      47         [ +  + ]:    4900030 :     static thread_local Random s_current(0);
      48                 :    4900030 :     return s_current;
      49                 :            :   }
      50                 :            : 
      51                 :            :   /** Get the minimum number that can be picked. */
      52                 :            :   static constexpr uint64_t min() { return std::mt19937_64::min(); }
      53                 :            : 
      54                 :            :   /** Get the maximum number that can be picked. */
      55                 :            :   static constexpr uint64_t max() { return std::mt19937_64::max(); }
      56                 :            : 
      57                 :            :   /** Set seed of Random.  */
      58                 :            :   void setSeed(uint64_t seed);
      59                 :            : 
      60                 :            :   /** Operator overload to pick random uint64_t number. */
      61                 :            :   uint64_t operator()();
      62                 :            : 
      63                 :            :   /** Pick an integral number with type T. */
      64                 :            :   template <typename T,
      65                 :            :             typename std::enable_if<std::is_integral<T>::value, int>::type = 0>
      66                 :      11129 :   T pick()
      67                 :            :   {
      68                 :      11129 :     std::uniform_int_distribution<T> dist;
      69                 :      22258 :     return dist(d_rng);
      70                 :            :   }
      71                 :            : 
      72                 :            :   /**
      73                 :            :    * Pick an integral number with type T between 'from' and 'to' (inclusive).
      74                 :            :    */
      75                 :            :   template <typename T,
      76                 :            :             typename std::enable_if<std::is_integral<T>::value, int>::type = 0>
      77                 :    9082149 :   T pick(T from, T to)
      78                 :            :   {
      79 [ -  + ][ -  + ]:    9082149 :     Assert(from <= to);
                 [ -  - ]
      80                 :    9082149 :     std::uniform_int_distribution<T> dist(from, to);
      81                 :   18164298 :     return dist(d_rng);
      82                 :            :   }
      83                 :            : 
      84                 :            :   /** Pick a floating point number with type T. */
      85                 :            :   template <
      86                 :            :       typename T,
      87                 :            :       typename std::enable_if<std::is_floating_point<T>::value, int>::type = 0>
      88                 :            :   T pick()
      89                 :            :   {
      90                 :            :     std::uniform_real_distribution<T> dist;
      91                 :            :     return dist(d_rng);
      92                 :            :   }
      93                 :            : 
      94                 :            :   /** Pick a floating point number with type T between 'from' and 'to'
      95                 :            :    * ([from, to), upper bound exclusive). */
      96                 :            :   template <
      97                 :            :       typename T,
      98                 :            :       typename std::enable_if<std::is_floating_point<T>::value, int>::type = 0>
      99                 :        482 :   T pick(T from, T to)
     100                 :            :   {
     101 [ -  + ][ -  + ]:        482 :     Assert(from <= to);
                 [ -  - ]
     102                 :        482 :     std::uniform_real_distribution<T> dist(from, to);
     103                 :        964 :     return dist(d_rng);
     104                 :            :   }
     105                 :            : 
     106                 :            :   /** Pick with given probability (yes / no). */
     107                 :            :   bool pickWithProb(double probability);
     108                 :            : 
     109                 :            : #ifdef CVC5_GMP_IMP
     110                 :            :   gmp_randstate_t* getGMPRandstate() { return &d_gmp_randstate; }
     111                 :            : #endif
     112                 :            : #ifdef CVC5_CLN_IMP
     113                 :         27 :   cln::random_state* getCLNRandstate() { return &d_cln_randstate; }
     114                 :            : #endif
     115                 :            : 
     116                 :            :  private:
     117                 :            :   /* The seed of the RNG. */
     118                 :            :   uint64_t d_seed;
     119                 :            :   /** The underlying RNG Mersenne Twister engine. */
     120                 :            :   std::mt19937_64 d_rng;
     121                 :            : 
     122                 :            : #ifdef CVC5_GMP_IMP
     123                 :            :   gmp_randstate_t d_gmp_randstate;
     124                 :            : #endif
     125                 :            : #ifdef CVC5_CLN_IMP
     126                 :            :   cln::random_state d_cln_randstate;
     127                 :            : #endif
     128                 :            : };
     129                 :            : 
     130                 :            : }  // namespace cvc5::internal
     131                 :            : #endif