Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andres Noetzli, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Sampler class that generates random values of different sorts
14 : : *
15 : : * The Sampler class can be used to generate random values of different sorts
16 : : * with biased and unbiased distributions.
17 : : */
18 : :
19 : : #include "util/sampler.h"
20 : :
21 : : #include <sstream>
22 : :
23 : : #include "base/check.h"
24 : : #include "util/bitvector.h"
25 : : #include "util/random.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : 272690 : BitVector Sampler::pickBvUniform(unsigned sz)
30 : : {
31 : 272690 : Random& rnd = Random::getRandom();
32 : :
33 : 272690 : std::stringstream ss;
34 [ + + ]: 5431340 : for (unsigned i = 0; i < sz; i++)
35 : : {
36 [ + + ]: 5158650 : ss << (rnd.pickWithProb(0.5) ? "1" : "0");
37 : : }
38 : :
39 : 818070 : return BitVector(ss.str(), 2);
40 : : }
41 : :
42 : 0 : FloatingPoint Sampler::pickFpUniform(unsigned e, unsigned s)
43 : : {
44 : 0 : return FloatingPoint(e, s, pickBvUniform(e + s));
45 : : }
46 : :
47 : 19994 : FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
48 : : {
49 : : // The biased generation of random FP values is inspired by
50 : : // PyMPF [0].
51 : : //
52 : : // [0] https://github.com/florianschanda/PyMPF
53 : :
54 : 19994 : Random& rnd = Random::getRandom();
55 : :
56 : 39988 : BitVector zero(1);
57 : 39988 : BitVector one(1, static_cast<unsigned int>(1));
58 : :
59 : 39988 : BitVector sign(1);
60 : 39988 : BitVector exp(e);
61 : 39988 : BitVector sig(s - 1);
62 : :
63 [ + + ]: 19994 : if (rnd.pickWithProb(probSpecial))
64 : : {
65 : : // Generate special values
66 : :
67 : 4032 : uint64_t type = rnd.pick(0, 12);
68 [ + + ][ + + ]: 4032 : switch (type)
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ]
69 : : {
70 : : // NaN
71 : : // sign = 1, exp = 11...11, sig = 11...11
72 : 330 : case 0:
73 : 330 : sign = one;
74 : 330 : exp = BitVector::mkOnes(e);
75 : 330 : sig = BitVector::mkOnes(s - 1);
76 : 330 : break;
77 : :
78 : : // +/- inf
79 : : // sign = x, exp = 11...11, sig = 00...00
80 : 282 : case 1: sign = one; CVC5_FALLTHROUGH;
81 : 600 : case 2: exp = BitVector::mkOnes(e); break;
82 : :
83 : : // +/- zero
84 : : // sign = x, exp = 00...00, sig = 00...00
85 : 344 : case 3: sign = one; CVC5_FALLTHROUGH;
86 : 652 : case 4: break;
87 : :
88 : : // +/- max subnormal
89 : : // sign = x, exp = 00...00, sig = 11...11
90 : 338 : case 5: sign = one; CVC5_FALLTHROUGH;
91 : 596 : case 6: sig = BitVector::mkOnes(s - 1); break;
92 : :
93 : : // +/- min subnormal
94 : : // sign = x, exp = 00...00, sig = 00...01
95 : 308 : case 7: sign = one; CVC5_FALLTHROUGH;
96 : 670 : case 8: sig = BitVector(s - 1, static_cast<unsigned int>(1)); break;
97 : :
98 : : // +/- max normal
99 : : // sign = x, exp = 11...10, sig = 11...11
100 : 304 : case 9: sign = one; CVC5_FALLTHROUGH;
101 : 650 : case 10:
102 : 650 : exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1));
103 : 650 : sig = BitVector::mkOnes(s - 1);
104 : 650 : break;
105 : :
106 : : // +/- min normal
107 : : // sign = x, exp = 00...01, sig = 00...00
108 : 240 : case 11: sign = one; CVC5_FALLTHROUGH;
109 : 534 : case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break;
110 : :
111 : 0 : default: Unreachable();
112 : : }
113 : : }
114 : : else
115 : : {
116 : : // Generate normal and subnormal values
117 : :
118 : : // 50% chance of positive/negative sign
119 [ + + ]: 15962 : if (rnd.pickWithProb(0.5))
120 : : {
121 : 7958 : sign = one;
122 : : }
123 : :
124 : 15962 : uint64_t pattern = rnd.pick(0, 5);
125 [ + + ][ + + ]: 15962 : switch (pattern)
[ + + ][ - ]
126 : : {
127 : 2784 : case 0:
128 : : // sign = x, exp = xx...x0, sig = 11...11
129 : 2784 : exp = pickBvUniform(e - 1).concat(zero);
130 : 2784 : sig = BitVector::mkOnes(s - 1);
131 : 2784 : break;
132 : :
133 : 2662 : case 1:
134 : : // sign = x, exp = xx...x0, sig = 00...00
135 : 2662 : exp = pickBvUniform(e - 1).concat(zero);
136 : 2662 : break;
137 : :
138 : 2644 : case 2:
139 : : // sign = x, exp = 0x...x1, sig = 11...11
140 : 2644 : exp = zero.concat(pickBvUniform(e - 2).concat(one));
141 : 2644 : sig = BitVector::mkOnes(s - 1);
142 : 2644 : break;
143 : :
144 : 2552 : case 3:
145 : : // sign = x, exp = xx...x0, sig = xx...xx
146 : 2552 : exp = pickBvUniform(e - 1).concat(zero);
147 : 2552 : sig = pickBvUniform(s - 1);
148 : 2552 : break;
149 : :
150 : 2598 : case 4:
151 : : // sign = x, exp = 0x...x1, sig = xx...xx
152 : 2598 : exp = zero.concat(pickBvUniform(e - 2).concat(one));
153 : 2598 : sig = pickBvUniform(s - 1);
154 : 2598 : break;
155 : :
156 : 2722 : case 5:
157 : : {
158 : : // sign = x, exp = xx...xx0xx...xx, sig = xx...xx
159 : 2722 : uint64_t lsbSize = rnd.pick(1, e - 2);
160 : 2722 : uint64_t msbSize = e - lsbSize - 1;
161 : 5444 : BitVector lsb = pickBvUniform(lsbSize);
162 : 5444 : BitVector msb = pickBvUniform(msbSize);
163 : 2722 : exp = msb.concat(zero.concat(lsb));
164 : 2722 : sig = pickBvUniform(s - 1);
165 : 2722 : break;
166 : : }
167 : :
168 : 0 : default: Unreachable();
169 : : }
170 : : }
171 : :
172 : 39988 : BitVector bv = sign.concat(exp.concat(sig));
173 : 39988 : return FloatingPoint(e, s, bv);
174 : : }
175 : :
176 : : } // namespace cvc5::internal
|
