1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andres Noetzli |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 { |
28 |
|
|
29 |
94598 |
BitVector Sampler::pickBvUniform(unsigned sz) |
30 |
|
{ |
31 |
94598 |
Random& rnd = Random::getRandom(); |
32 |
|
|
33 |
189196 |
std::stringstream ss; |
34 |
656110 |
for (unsigned i = 0; i < sz; i++) |
35 |
|
{ |
36 |
561512 |
ss << (rnd.pickWithProb(0.5) ? "1" : "0"); |
37 |
|
} |
38 |
|
|
39 |
189196 |
return BitVector(ss.str(), 2); |
40 |
|
} |
41 |
|
|
42 |
|
FloatingPoint Sampler::pickFpUniform(unsigned e, unsigned s) |
43 |
|
{ |
44 |
|
return FloatingPoint(e, s, pickBvUniform(e + s)); |
45 |
|
} |
46 |
|
|
47 |
|
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 |
|
Random& rnd = Random::getRandom(); |
55 |
|
|
56 |
|
BitVector zero(1); |
57 |
|
BitVector one(1, static_cast<unsigned int>(1)); |
58 |
|
|
59 |
|
BitVector sign(1); |
60 |
|
BitVector exp(e); |
61 |
|
BitVector sig(s - 1); |
62 |
|
|
63 |
|
if (rnd.pickWithProb(probSpecial)) |
64 |
|
{ |
65 |
|
// Generate special values |
66 |
|
|
67 |
|
uint64_t type = rnd.pick(0, 12); |
68 |
|
switch (type) |
69 |
|
{ |
70 |
|
// NaN |
71 |
|
// sign = 1, exp = 11...11, sig = 11...11 |
72 |
|
case 0: |
73 |
|
sign = one; |
74 |
|
exp = BitVector::mkOnes(e); |
75 |
|
sig = BitVector::mkOnes(s - 1); |
76 |
|
break; |
77 |
|
|
78 |
|
// +/- inf |
79 |
|
// sign = x, exp = 11...11, sig = 00...00 |
80 |
|
case 1: sign = one; CVC5_FALLTHROUGH; |
81 |
|
case 2: exp = BitVector::mkOnes(e); break; |
82 |
|
|
83 |
|
// +/- zero |
84 |
|
// sign = x, exp = 00...00, sig = 00...00 |
85 |
|
case 3: sign = one; CVC5_FALLTHROUGH; |
86 |
|
case 4: break; |
87 |
|
|
88 |
|
// +/- max subnormal |
89 |
|
// sign = x, exp = 00...00, sig = 11...11 |
90 |
|
case 5: sign = one; CVC5_FALLTHROUGH; |
91 |
|
case 6: sig = BitVector::mkOnes(s - 1); break; |
92 |
|
|
93 |
|
// +/- min subnormal |
94 |
|
// sign = x, exp = 00...00, sig = 00...01 |
95 |
|
case 7: sign = one; CVC5_FALLTHROUGH; |
96 |
|
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 |
|
case 9: sign = one; CVC5_FALLTHROUGH; |
101 |
|
case 10: |
102 |
|
exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1)); |
103 |
|
sig = BitVector::mkOnes(s - 1); |
104 |
|
break; |
105 |
|
|
106 |
|
// +/- min normal |
107 |
|
// sign = x, exp = 00...01, sig = 00...00 |
108 |
|
case 11: sign = one; CVC5_FALLTHROUGH; |
109 |
|
case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break; |
110 |
|
|
111 |
|
default: Unreachable(); |
112 |
|
} |
113 |
|
} |
114 |
|
else |
115 |
|
{ |
116 |
|
// Generate normal and subnormal values |
117 |
|
|
118 |
|
// 50% chance of positive/negative sign |
119 |
|
if (rnd.pickWithProb(0.5)) |
120 |
|
{ |
121 |
|
sign = one; |
122 |
|
} |
123 |
|
|
124 |
|
uint64_t pattern = rnd.pick(0, 5); |
125 |
|
switch (pattern) |
126 |
|
{ |
127 |
|
case 0: |
128 |
|
// sign = x, exp = xx...x0, sig = 11...11 |
129 |
|
exp = pickBvUniform(e - 1).concat(zero); |
130 |
|
sig = BitVector::mkOnes(s - 1); |
131 |
|
break; |
132 |
|
|
133 |
|
case 1: |
134 |
|
// sign = x, exp = xx...x0, sig = 00...00 |
135 |
|
exp = pickBvUniform(e - 1).concat(zero); |
136 |
|
break; |
137 |
|
|
138 |
|
case 2: |
139 |
|
// sign = x, exp = 0x...x1, sig = 11...11 |
140 |
|
exp = zero.concat(pickBvUniform(e - 2).concat(one)); |
141 |
|
sig = BitVector::mkOnes(s - 1); |
142 |
|
break; |
143 |
|
|
144 |
|
case 3: |
145 |
|
// sign = x, exp = xx...x0, sig = xx...xx |
146 |
|
exp = pickBvUniform(e - 1).concat(zero); |
147 |
|
sig = pickBvUniform(s - 1); |
148 |
|
break; |
149 |
|
|
150 |
|
case 4: |
151 |
|
// sign = x, exp = 0x...x1, sig = xx...xx |
152 |
|
exp = zero.concat(pickBvUniform(e - 2).concat(one)); |
153 |
|
sig = pickBvUniform(s - 1); |
154 |
|
break; |
155 |
|
|
156 |
|
case 5: |
157 |
|
{ |
158 |
|
// sign = x, exp = xx...xx0xx...xx, sig = xx...xx |
159 |
|
uint64_t lsbSize = rnd.pick(1, e - 2); |
160 |
|
uint64_t msbSize = e - lsbSize - 1; |
161 |
|
BitVector lsb = pickBvUniform(lsbSize); |
162 |
|
BitVector msb = pickBvUniform(msbSize); |
163 |
|
exp = msb.concat(zero.concat(lsb)); |
164 |
|
sig = pickBvUniform(s - 1); |
165 |
|
break; |
166 |
|
} |
167 |
|
|
168 |
|
default: Unreachable(); |
169 |
|
} |
170 |
|
} |
171 |
|
|
172 |
|
BitVector bv = sign.concat(exp.concat(sig)); |
173 |
|
return FloatingPoint(e, s, bv); |
174 |
|
} |
175 |
|
|
176 |
29574 |
} // namespace cvc5 |