GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/sampler.cpp Lines: 7 74 9.5 %
Date: 2021-03-23 Branches: 12 203 5.9 %

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