diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-08 13:38:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-08 13:38:45 -0700 |
commit | 86d9ba4431108e1fd89639e23857631a7380a005 (patch) | |
tree | 81e57f2b4594f6e4f80533a00789ece362b93da3 /src/util/sampler.h | |
parent | ad454857a1f57386f7b132c01ad460750ca8d3aa (diff) |
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
Diffstat (limited to 'src/util/sampler.h')
-rw-r--r-- | src/util/sampler.h | 58 |
1 files changed, 58 insertions, 0 deletions
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 */ |