Add more sophisticated floating-point sampler (#2155)

This commit adds a floating-point sampler inspired by PyMPF [0]. It also
creates a new Sampler class that can be used for creating random values
of different sorts (currently BV and FP values).

[0] https://github.com/florianschanda/PyMPF

3 files changed, 247 insertions, 3 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 9117b9d6b..297d96208 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -19,8 +19,8 @@ libutil_la_SOURCES = \
 	abstract_value.cpp \
 	abstract_value.h \
 	bin_heap.h \
-	bitvector.h \
 	bitvector.cpp \
+	bitvector.h \
 	bool.h \
 	cardinality.cpp \
 	cardinality.h \
@@ -40,16 +40,18 @@ libutil_la_SOURCES = \
 	ostream_util.cpp \
 	ostream_util.h \
 	proof.h \
+	random.cpp \
+	random.h \
 	regexp.cpp \
 	regexp.h \
 	resource_manager.cpp \
 	resource_manager.h \
 	result.cpp \
-	random.h \
-	random.cpp \
 	result.h \
 	safe_print.cpp \
 	safe_print.h \
+	sampler.cpp \
+	sampler.h \
 	sexpr.cpp \
 	sexpr.h \
 	smt2_quote_string.cpp \
diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
new file mode 100644
index 000000000..e64ab56df
--- /dev/null
+++ b/src/util/sampler.cpp
@@ -0,0 +1,184 @@
+/*********************                                                        */
+/*! \file sampler.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Sampler class that generates random values of different sorts
+ **
+ ** The Sampler class can be used to generate random values of different sorts
+ ** with biased and unbiased distributions.
+ **/
+
+#include "util/sampler.h"
+
+#include "base/cvc4_assert.h"
+#include "util/bitvector.h"
+
+namespace CVC4 {
+
+BitVector Sampler::pickBvUniform(unsigned sz)
+{
+  Random& rnd = Random::getRandom();
+
+  std::stringstream ss;
+  for (unsigned i = 0; i < sz; i++)
+  {
+    ss << (rnd.pickWithProb(0.5) ? "1" : "0");
+  }
+
+  return BitVector(ss.str(), 2);
+}
+
+FloatingPoint Sampler::pickFpUniform(unsigned e, unsigned s)
+{
+  return FloatingPoint(e, s, pickBvUniform(e + s));
+}
+
+FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
+{
+  // The biased generation of random FP values is inspired by
+  // PyMPF [0].
+  //
+  // [0] https://github.com/florianschanda/PyMPF
+
+  Random& rnd = Random::getRandom();
+
+  BitVector zero(1);
+  BitVector one(1, static_cast<unsigned int>(1));
+
+  BitVector sign(1);
+  BitVector exp(e);
+  BitVector sig(s - 1);
+
+  if (rnd.pickWithProb(probSpecial))
+  {
+    // Generate special values
+
+    uint64_t type = rnd.pick(0, 12);
+    switch (type)
+    {
+      // NaN
+      // sign = 1, exp = 11...11, sig = 11...11
+      case 0:
+        sign = one;
+        exp = BitVector::mkOnes(e);
+        sig = BitVector::mkOnes(s - 1);
+        break;
+
+      // +/- inf
+      // sign = x, exp = 11...11, sig = 00...00
+      case 1:
+        sign = one;
+        // Intentional fall-through
+      case 2: exp = BitVector::mkOnes(e); break;
+
+      // +/- zero
+      // sign = x, exp = 00...00, sig = 00...00
+      case 3:
+        sign = one;
+        // Intentional fall-through
+      case 4: break;
+
+      // +/- max subnormal
+      // sign = x, exp = 00...00, sig = 11...11
+      case 5:
+        sign = one;
+        // Intentional fall-through
+      case 6: sig = BitVector::mkOnes(s - 1); break;
+
+      // +/- min subnormal
+      // sign = x, exp = 00...00, sig = 00...01
+      case 7:
+        sign = one;
+        // Intentional fall-through
+      case 8: sig = BitVector(s - 1, static_cast<unsigned int>(1)); break;
+
+      // +/- max normal
+      // sign = x, exp = 11...10, sig = 11...11
+      case 9:
+        sign = one;
+        // Intentional fall-through
+      case 10:
+        exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1));
+        sig = BitVector::mkOnes(s - 1);
+        break;
+
+      // +/- min normal
+      // sign = x, exp = 00...01, sig = 00...00
+      case 11:
+        sign = one;
+        // Intentional fall-through
+      case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break;
+
+      default: Unreachable();
+    }
+  }
+  else
+  {
+    // Generate normal and subnormal values
+
+    // 50% chance of positive/negative sign
+    if (rnd.pickWithProb(0.5))
+    {
+      sign = one;
+    }
+
+    uint64_t pattern = rnd.pick(0, 5);
+    switch (pattern)
+    {
+      case 0:
+        // sign = x, exp = xx...x0, sig = 11...11
+        exp = pickBvUniform(e - 1).concat(zero);
+        sig = BitVector::mkOnes(s - 1);
+        break;
+
+      case 1:
+        // sign = x, exp = xx...x0, sig = 00...00
+        exp = pickBvUniform(e - 1).concat(zero);
+        break;
+
+      case 2:
+        // sign = x, exp = 0x...x1, sig = 11...11
+        exp = zero.concat(pickBvUniform(e - 2).concat(one));
+        sig = BitVector::mkOnes(s - 1);
+        break;
+
+      case 3:
+        // sign = x, exp = xx...x0, sig = xx...xx
+        exp = pickBvUniform(e - 1).concat(zero);
+        sig = pickBvUniform(s - 1);
+        break;
+
+      case 4:
+        // sign = x, exp = 0x...x1, sig = xx...xx
+        exp = zero.concat(pickBvUniform(e - 2).concat(one));
+        sig = pickBvUniform(s - 1);
+        break;
+
+      case 5:
+      {
+        // sign = x, exp = xx...xx0xx...xx, sig = xx...xx
+        uint64_t lsbSize = rnd.pick(1, e - 2);
+        uint64_t msbSize = e - lsbSize - 1;
+        BitVector lsb = pickBvUniform(lsbSize);
+        BitVector msb = pickBvUniform(msbSize);
+        exp = msb.concat(zero.concat(lsb));
+        sig = pickBvUniform(s - 1);
+        break;
+      }
+
+      default: Unreachable();
+    }
+  }
+
+  BitVector bv = sign.concat(exp.concat(sig));
+  return FloatingPoint(e, s, bv);
+}
+
+}  // namespace CVC4
diff --git a/src/util/sampler.h b/src/util/sampler.h
new file mode 100644
index 000000000..f8f11dff2
--- /dev/null
+++ b/src/util/sampler.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file sampler.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Sampler class that generates random values of different sorts
+ **
+ ** The Sampler class can be used to generate random values of different sorts
+ ** with biased and unbiased distributions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#define __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+
+#include "util/floatingpoint.h"
+#include "util/random.h"
+
+namespace CVC4 {
+
+class Sampler
+{
+ public:
+  /**
+   * Generates a random, uniform bit-vector value.
+   */
+  static BitVector pickBvUniform(unsigned sz);
+
+  /**
+   * Generates a random, uniform floating-point value.
+   */
+  static FloatingPoint pickFpUniform(unsigned e, unsigned s);
+
+  /**
+   * Generates a random floating-point value biased towards special values
+   * (e.g.  +/- inf) and interesting bit-patterns (e.g. values with a zero
+   * significand).
+   */
+  static FloatingPoint pickFpBiased(unsigned e, unsigned s);
+
+ private:
+  /**
+   * Probablility with which special floating-point values are picked when
+   * picking a biased floating-point value
+   */
+  static constexpr double probSpecial = 0.2;
+};
+
+}  // namespace CVC4
+
+#endif /* __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */