1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "utils/btorrng.h"
10 #include "btoropt.h"
11
12 #include <assert.h>
13 #include <limits.h>
14 #ifndef NDEBUG
15 #include <float.h>
16 #endif
17
18 #ifdef BTOR_USE_GMP
19 #include <gmp.h>
20 #endif
21
22 void
btor_rng_init(BtorRNG * rng,uint32_t seed)23 btor_rng_init (BtorRNG* rng, uint32_t seed)
24 {
25 assert (rng);
26
27 rng->w = seed;
28 rng->z = ~rng->w;
29 rng->w <<= 1;
30 rng->z <<= 1;
31 rng->w += 1;
32 rng->z += 1;
33 rng->w *= 2019164533u;
34 rng->z *= 1000632769u;
35
36 #ifdef BTOR_USE_GMP
37 if (rng->is_init)
38 {
39 assert (rng->gmp_state);
40 gmp_randclear (*((gmp_randstate_t*) rng->gmp_state));
41 }
42 else
43 {
44 rng->mm = btor_mem_mgr_new ();
45 rng->gmp_state = btor_mem_malloc (rng->mm, sizeof (gmp_randstate_t));
46 }
47 rng->is_init = true;
48 gmp_randinit_mt (*((gmp_randstate_t*) rng->gmp_state));
49 gmp_randseed_ui (*((gmp_randstate_t*) rng->gmp_state), btor_rng_rand (rng));
50 #endif
51 }
52
53 void
btor_rng_clone(BtorRNG * rng,BtorRNG * clone)54 btor_rng_clone (BtorRNG* rng, BtorRNG* clone)
55 {
56 (void) rng;
57 (void) clone;
58 #ifdef BTOR_USE_GMP
59 assert (rng->gmp_state);
60 clone->mm = btor_mem_mgr_new ();
61 clone->gmp_state = btor_mem_malloc (clone->mm, sizeof (gmp_randstate_t));
62 gmp_randinit_set (*((gmp_randstate_t*) clone->gmp_state),
63 *((gmp_randstate_t*) rng->gmp_state));
64 #endif
65 }
66
67 void
btor_rng_delete(BtorRNG * rng)68 btor_rng_delete (BtorRNG* rng)
69 {
70 (void) rng;
71 #ifdef BTOR_USE_GMP
72 assert (rng->gmp_state);
73 gmp_randclear (*((gmp_randstate_t*) rng->gmp_state));
74 btor_mem_free (rng->mm, rng->gmp_state, sizeof (gmp_randstate_t));
75 btor_mem_mgr_delete (rng->mm);
76 rng->gmp_state = 0;
77 rng->is_init = false;
78 #endif
79 }
80
81 uint32_t
btor_rng_rand(BtorRNG * rng)82 btor_rng_rand (BtorRNG* rng)
83 {
84 assert (rng);
85 rng->z = 36969 * (rng->z & 65535) + (rng->z >> 16);
86 rng->w = 18000 * (rng->w & 65535) + (rng->w >> 16);
87 return (rng->z << 16) + rng->w; /* 32-bit result */
88 }
89
90 uint32_t
btor_rng_pick_rand(BtorRNG * rng,uint32_t from,uint32_t to)91 btor_rng_pick_rand (BtorRNG* rng, uint32_t from, uint32_t to)
92 {
93 assert (rng);
94 assert (from <= to);
95
96 uint32_t res;
97
98 from = from == UINT32_MAX ? UINT32_MAX - 1 : from;
99 to = to == UINT32_MAX ? UINT32_MAX - 1 : to;
100 res = btor_rng_rand (rng);
101 res %= to - from + 1;
102 res += from;
103 return res;
104 }
105
106 double
btor_rng_pick_rand_dbl(BtorRNG * rng,double from,double to)107 btor_rng_pick_rand_dbl (BtorRNG* rng, double from, double to)
108 {
109 assert (rng);
110 assert (from <= to && to < DBL_MAX);
111
112 double res;
113
114 res = (double) btor_rng_rand (rng) / UINT32_MAX;
115 res = from + res * (to - from);
116 return res;
117 }
118
119 bool
btor_rng_pick_with_prob(BtorRNG * rng,uint32_t prob)120 btor_rng_pick_with_prob (BtorRNG* rng, uint32_t prob)
121 {
122 assert (rng);
123 assert (prob <= BTOR_PROB_MAX);
124
125 uint32_t r;
126
127 r = btor_rng_pick_rand (rng, 0, BTOR_PROB_MAX - 1);
128 return r < prob;
129 }
130