Numeric.SpecFunctions:choose from math-functions-0.1.5.2

Average Error: 12.6 → 0.3

Time: 1.8s

Precision: 64

Math

\[\frac{x \cdot \left(y + z\right)}{z}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{x \cdot \left(y + z\right)}{z} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z}, y, x\right)\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le -11788.3655307668978:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le 5.3596908162343409 \cdot 10^{-20}:\\ \;\;\;\;\frac{x}{\frac{z}{y + z}}\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le 3.48840688713487176 \cdot 10^{297}:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z}, y, x\right)\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r413273 = x;
        double r413274 = y;
        double r413275 = z;
        double r413276 = r413274 + r413275;
        double r413277 = r413273 * r413276;
        double r413278 = r413277 / r413275;
        return r413278;
}

↓

double f(double x, double y, double z) {
        double r413279 = x;
        double r413280 = y;
        double r413281 = z;
        double r413282 = r413280 + r413281;
        double r413283 = r413279 * r413282;
        double r413284 = r413283 / r413281;
        double r413285 = -inf.0;
        bool r413286 = r413284 <= r413285;
        double r413287 = r413279 / r413281;
        double r413288 = fma(r413287, r413280, r413279);
        double r413289 = -11788.365530766898;
        bool r413290 = r413284 <= r413289;
        double r413291 = 5.359690816234341e-20;
        bool r413292 = r413284 <= r413291;
        double r413293 = r413281 / r413282;
        double r413294 = r413279 / r413293;
        double r413295 = 3.488406887134872e+297;
        bool r413296 = r413284 <= r413295;
        double r413297 = r413296 ? r413284 : r413288;
        double r413298 = r413292 ? r413294 : r413297;
        double r413299 = r413290 ? r413284 : r413298;
        double r413300 = r413286 ? r413288 : r413299;
        return r413300;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	12.6
Target	2.9
Herbie	0.3

\[\frac{x}{\frac{z}{y + z}}\]

Derivation

1. Split input into 3 regimes

2. if (/ (* x (+ y z)) z) < -inf.0 or 3.488406887134872e+297 < (/ (* x (+ y z)) z)

   1. Initial program 61.4

      \[\frac{x \cdot \left(y + z\right)}{z}\]

   2. Taylor expanded around 0 20.2

      \[\leadsto \color{blue}{\frac{x \cdot y}{z} + x}\]

   3. Simplified 1.1

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{x}{z}, y, x\right)}\]

   if -inf.0 < (/ (* x (+ y z)) z) < -11788.365530766898 or 5.359690816234341e-20 < (/ (* x (+ y z)) z) < 3.488406887134872e+297

   1. Initial program 0.2

      \[\frac{x \cdot \left(y + z\right)}{z}\]

   if -11788.365530766898 < (/ (* x (+ y z)) z) < 5.359690816234341e-20

   1. Initial program 6.4

      \[\frac{x \cdot \left(y + z\right)}{z}\]
   2. Using strategy rm

   3. Applied associate-/l* 0.1

      \[\leadsto \color{blue}{\frac{x}{\frac{z}{y + z}}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot \left(y + z\right)}{z} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z}, y, x\right)\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le -11788.3655307668978:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le 5.3596908162343409 \cdot 10^{-20}:\\ \;\;\;\;\frac{x}{\frac{z}{y + z}}\\ \mathbf{elif}\;\frac{x \cdot \left(y + z\right)}{z} \le 3.48840688713487176 \cdot 10^{297}:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{z}, y, x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020027 +o rules:numerics
(FPCore (x y z)
  :name "Numeric.SpecFunctions:choose from math-functions-0.1.5.2"
  :precision binary64

  :herbie-target
  (/ x (/ z (+ y z)))

  (/ (* x (+ y z)) z))