1# This file is part of Hypothesis, which may be found at
2# https://github.com/HypothesisWorks/hypothesis/
3#
4# Copyright the Hypothesis Authors.
5# Individual contributors are listed in AUTHORS.rst and the git log.
6#
7# This Source Code Form is subject to the terms of the Mozilla Public License,
8# v. 2.0. If a copy of the MPL was not distributed with this file, You can
9# obtain one at https://mozilla.org/MPL/2.0/.
10
11import math
12import sys
13
14from hypothesis.internal.conjecture.floats import float_to_lex
15from hypothesis.internal.conjecture.shrinking.common import Shrinker
16from hypothesis.internal.conjecture.shrinking.integer import Integer
17from hypothesis.internal.floats import MAX_PRECISE_INTEGER, float_to_int, int_to_float
18
19# Bit pattern of the boundary float, so we can compute float-grid indices
20# relative to it without recomputing the constant on every call.
21_BOUNDARY_BITS = float_to_int(float(MAX_PRECISE_INTEGER))
22
23
24def _float_to_position(f: float) -> int:
25 """Map a non-negative float to a linear integer position such that adjacent
26 representable floats correspond to adjacent integers.
27
28 For ``f <= MAX_PRECISE_INTEGER`` the position is just ``int(f)``. Above the
29 boundary, where the gap between adjacent floats exceeds 1, we extend by the
30 float's index in the bit-pattern sequence past ``MAX_PRECISE_INTEGER``, so
31 that decrementing the position by 1 corresponds to ``next_down(f)``.
32 """
33 if f <= MAX_PRECISE_INTEGER:
34 return int(f)
35 return MAX_PRECISE_INTEGER + (float_to_int(f) - _BOUNDARY_BITS)
36
37
38def _position_to_float(n: int) -> float:
39 """Inverse of :func:`_float_to_position` on the integer-valued range. Always
40 returns an integer-valued, non-negative float."""
41 if n <= MAX_PRECISE_INTEGER:
42 return float(n)
43 return int_to_float(_BOUNDARY_BITS + (n - MAX_PRECISE_INTEGER))
44
45
46class Float(Shrinker):
47 def setup(self):
48 self.debugging_enabled = True
49
50 def make_canonical(self, f):
51 if math.isnan(f):
52 # Distinguish different NaN bit patterns, while making each equal to itself.
53 # Wrap in tuple to avoid potential collision with (huge) finite floats.
54 return ("nan", float_to_int(f))
55 return f
56
57 def check_invariants(self, value):
58 # We only handle positive floats (including NaN) because we encode the sign
59 # separately anyway.
60 assert not (value < 0)
61
62 def left_is_better(self, left, right):
63 lex1 = float_to_lex(left)
64 lex2 = float_to_lex(right)
65 return lex1 < lex2
66
67 def short_circuit(self):
68 # We check for a bunch of standard "large" floats. If we're currently
69 # worse than them and the shrink downwards doesn't help, abort early
70 # because there's not much useful we can do here.
71
72 for g in [sys.float_info.max, math.inf, math.nan]:
73 self.consider(g)
74
75 # If we're stuck at a nasty float don't try to shrink it further.
76 if not math.isfinite(self.current):
77 return True
78
79 def run_step(self):
80 # Above MAX_PRECISE_INTEGER all floats are integers, but the gap between
81 # adjacent floats is > 1, so consecutive integers are not all
82 # representable. Integer.shrink would step by n - 1, which rounds straight
83 # back to n and stalls. We instead shrink on the float grid by delegating
84 # to Integer with a bijection that maps each representable float to an
85 # adjacent integer position, so n - 1 always corresponds to next_down(n).
86 if self.current > MAX_PRECISE_INTEGER:
87 self.delegate(
88 Integer,
89 convert_to=_float_to_position,
90 convert_from=_position_to_float,
91 )
92 return
93
94 # Finally we get to the important bit: Each of these is a small change
95 # to the floating point number that corresponds to a large change in
96 # the lexical representation. Trying these ensures that our floating
97 # point shrink can always move past these obstacles. In particular it
98 # ensures we can always move to integer boundaries and shrink past a
99 # change that would require shifting the exponent while not changing
100 # the float value much.
101
102 # First, try dropping precision bits by rounding the scaled value. We
103 # try values ordered from least-precise (integer) to more precise, ie.
104 # approximate lexicographical order. Once we find an acceptable shrink,
105 # self.consider discards the remaining attempts early and skips test
106 # invocation. The loop count sets max fractional bits to keep, and is a
107 # compromise between completeness and performance.
108
109 for p in range(10):
110 scaled = self.current * 2**p # note: self.current may change in loop
111 for truncate in [math.floor, math.ceil]:
112 self.consider(truncate(scaled) / 2**p)
113
114 if self.consider(int(self.current)):
115 self.debug("Just an integer now")
116 self.delegate(Integer, convert_to=int, convert_from=float)
117 return
118
119 # Now try to minimize the top part of the fraction as an integer. This
120 # basically splits the float as k + x with 0 <= x < 1 and minimizes
121 # k as an integer, but without the precision issues that would have.
122 m, n = self.current.as_integer_ratio()
123 i, r = divmod(m, n)
124 self.call_shrinker(Integer, i, lambda k: self.consider((k * n + r) / n))