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 : : * Sampler class that generates random values of different sorts
11 : : *
12 : : * The Sampler class can be used to generate random values of different sorts
13 : : * with biased and unbiased distributions.
14 : : */
15 : :
16 : : #include "util/sampler.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "base/check.h"
21 : : #include "util/bitvector.h"
22 : : #include "util/random.h"
23 : :
24 : : namespace cvc5::internal {
25 : :
26 : 129512 : BitVector Sampler::pickBvUniform(unsigned sz)
27 : : {
28 : 129512 : Random& rnd = Random::getRandom();
29 : :
30 : 129512 : std::stringstream ss;
31 [ + + ]: 4556039 : for (unsigned i = 0; i < sz; i++)
32 : : {
33 [ + + ]: 4426527 : ss << (rnd.pickWithProb(0.5) ? "1" : "0");
34 : : }
35 : :
36 : 388536 : return BitVector(ss.str(), 2);
37 : 129512 : }
38 : :
39 : 0 : FloatingPoint Sampler::pickFpUniform(unsigned e, unsigned s)
40 : : {
41 : 0 : return FloatingPoint(e, s, pickBvUniform(e + s));
42 : : }
43 : :
44 : 4636 : FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
45 : : {
46 : : // The biased generation of random FP values is inspired by
47 : : // PyMPF [0].
48 : : //
49 : : // [0] https://github.com/florianschanda/PyMPF
50 : :
51 : 4636 : Random& rnd = Random::getRandom();
52 : :
53 : 4636 : BitVector zero(1);
54 : 4636 : BitVector one(1, static_cast<unsigned int>(1));
55 : :
56 : 4636 : BitVector sign(1);
57 : 4636 : BitVector exp(e);
58 : 4636 : BitVector sig(s - 1);
59 : :
60 [ + + ]: 4636 : if (rnd.pickWithProb(probSpecial))
61 : : {
62 : : // Generate special values
63 : :
64 : 936 : uint64_t type = rnd.pick<uint64_t>(0, 12);
65 [ + + ][ + + ]: 936 : switch (type)
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ]
66 : : {
67 : : // NaN
68 : : // sign = 1, exp = 11...11, sig = 11...11
69 : 54 : case 0:
70 : 54 : sign = one;
71 : 54 : exp = BitVector::mkOnes(e);
72 : 54 : sig = BitVector::mkOnes(s - 1);
73 : 54 : break;
74 : :
75 : : // +/- inf
76 : : // sign = x, exp = 11...11, sig = 00...00
77 : 68 : case 1: sign = one; CVC5_FALLTHROUGH;
78 : 152 : case 2: exp = BitVector::mkOnes(e); break;
79 : :
80 : : // +/- zero
81 : : // sign = x, exp = 00...00, sig = 00...00
82 : 114 : case 3: sign = one; CVC5_FALLTHROUGH;
83 : 184 : case 4: break;
84 : :
85 : : // +/- max subnormal
86 : : // sign = x, exp = 00...00, sig = 11...11
87 : 54 : case 5: sign = one; CVC5_FALLTHROUGH;
88 : 122 : case 6: sig = BitVector::mkOnes(s - 1); break;
89 : :
90 : : // +/- min subnormal
91 : : // sign = x, exp = 00...00, sig = 00...01
92 : 80 : case 7: sign = one; CVC5_FALLTHROUGH;
93 : 160 : case 8: sig = BitVector(s - 1, static_cast<unsigned int>(1)); break;
94 : :
95 : : // +/- max normal
96 : : // sign = x, exp = 11...10, sig = 11...11
97 : 42 : case 9: sign = one; CVC5_FALLTHROUGH;
98 : 110 : case 10:
99 : 110 : exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1));
100 : 110 : sig = BitVector::mkOnes(s - 1);
101 : 110 : break;
102 : :
103 : : // +/- min normal
104 : : // sign = x, exp = 00...01, sig = 00...00
105 : 72 : case 11: sign = one; CVC5_FALLTHROUGH;
106 : 154 : case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break;
107 : :
108 : 0 : default: Unreachable();
109 : : }
110 : : }
111 : : else
112 : : {
113 : : // Generate normal and subnormal values
114 : :
115 : : // 50% chance of positive/negative sign
116 [ + + ]: 3700 : if (rnd.pickWithProb(0.5))
117 : : {
118 : 1782 : sign = one;
119 : : }
120 : :
121 : 3700 : uint64_t pattern = rnd.pick<uint64_t>(0, 5);
122 [ + + ][ + + ]: 3700 : switch (pattern)
[ + + ][ - ]
123 : : {
124 : 602 : case 0:
125 : : // sign = x, exp = xx...x0, sig = 11...11
126 : 602 : exp = pickBvUniform(e - 1).concat(zero);
127 : 602 : sig = BitVector::mkOnes(s - 1);
128 : 602 : break;
129 : :
130 : 596 : case 1:
131 : : // sign = x, exp = xx...x0, sig = 00...00
132 : 596 : exp = pickBvUniform(e - 1).concat(zero);
133 : 596 : break;
134 : :
135 : 504 : case 2:
136 : : // sign = x, exp = 0x...x1, sig = 11...11
137 : 504 : exp = zero.concat(pickBvUniform(e - 2).concat(one));
138 : 504 : sig = BitVector::mkOnes(s - 1);
139 : 504 : break;
140 : :
141 : 682 : case 3:
142 : : // sign = x, exp = xx...x0, sig = xx...xx
143 : 682 : exp = pickBvUniform(e - 1).concat(zero);
144 : 682 : sig = pickBvUniform(s - 1);
145 : 682 : break;
146 : :
147 : 682 : case 4:
148 : : // sign = x, exp = 0x...x1, sig = xx...xx
149 : 682 : exp = zero.concat(pickBvUniform(e - 2).concat(one));
150 : 682 : sig = pickBvUniform(s - 1);
151 : 682 : break;
152 : :
153 : 634 : case 5:
154 : : {
155 : : // sign = x, exp = xx...xx0xx...xx, sig = xx...xx
156 [ - + ][ - + ]: 634 : Assert(e > 2);
[ - - ]
157 : 634 : uint64_t lsbSize = rnd.pick<uint64_t>(1, e - 2);
158 : 634 : uint64_t msbSize = e - lsbSize - 1;
159 : 634 : BitVector lsb = pickBvUniform(lsbSize);
160 : 634 : BitVector msb = pickBvUniform(msbSize);
161 : 634 : exp = msb.concat(zero.concat(lsb));
162 : 634 : sig = pickBvUniform(s - 1);
163 : 634 : break;
164 : 634 : }
165 : :
166 : 0 : default: Unreachable();
167 : : }
168 : : }
169 : :
170 : 9272 : BitVector bv = sign.concat(exp.concat(sig));
171 : 9272 : return FloatingPoint(e, s, bv);
172 : 4636 : }
173 : :
174 : : } // namespace cvc5::internal
|
