Numeric.SpecFunctions:choose from math-functions-0.1.5.2

Average Error: 12.4 → 0.8

Time: 23.3s

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 \lor \neg \left(\frac{x \cdot \left(y + z\right)}{z} \le -4.045134593776475081238842750214028354482 \cdot 10^{44} \lor \neg \left(\frac{x \cdot \left(y + z\right)}{z} \le 2.695397302024607118954686919516299646759 \cdot 10^{-102}\right) \land \frac{x \cdot \left(y + z\right)}{z} \le 1.963982869283896660652236439582473717883 \cdot 10^{219}\right):\\ \;\;\;\;x \cdot \frac{y + z}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \end{array}\]

C

double f(double x, double y, double z) {
        double r330716 = x;
        double r330717 = y;
        double r330718 = z;
        double r330719 = r330717 + r330718;
        double r330720 = r330716 * r330719;
        double r330721 = r330720 / r330718;
        return r330721;
}

↓

double f(double x, double y, double z) {
        double r330722 = x;
        double r330723 = y;
        double r330724 = z;
        double r330725 = r330723 + r330724;
        double r330726 = r330722 * r330725;
        double r330727 = r330726 / r330724;
        double r330728 = -inf.0;
        bool r330729 = r330727 <= r330728;
        double r330730 = -4.045134593776475e+44;
        bool r330731 = r330727 <= r330730;
        double r330732 = 2.695397302024607e-102;
        bool r330733 = r330727 <= r330732;
        double r330734 = !r330733;
        double r330735 = 1.9639828692838967e+219;
        bool r330736 = r330727 <= r330735;
        bool r330737 = r330734 && r330736;
        bool r330738 = r330731 || r330737;
        double r330739 = !r330738;
        bool r330740 = r330729 || r330739;
        double r330741 = r330725 / r330724;
        double r330742 = r330722 * r330741;
        double r330743 = r330740 ? r330742 : r330727;
        return r330743;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	12.4
Target	3.0
Herbie	0.8

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

Derivation

1. Split input into 2 regimes

2. if (/ (* x (+ y z)) z) < -inf.0 or -4.045134593776475e+44 < (/ (* x (+ y z)) z) < 2.695397302024607e-102 or 1.9639828692838967e+219 < (/ (* x (+ y z)) z)

   1. Initial program 21.1

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

   3. Applied *-un-lft-identity 21.1

      \[\leadsto \frac{x \cdot \left(y + z\right)}{\color{blue}{1 \cdot z}}\]

   4. Applied times-frac 1.3

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

   5. Simplified 1.3

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

   if -inf.0 < (/ (* x (+ y z)) z) < -4.045134593776475e+44 or 2.695397302024607e-102 < (/ (* x (+ y z)) z) < 1.9639828692838967e+219

   1. Initial program 0.3

      \[\frac{x \cdot \left(y + z\right)}{z}\]
3. Recombined 2 regimes into one program.

4. Final simplification 0.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot \left(y + z\right)}{z} = -\infty \lor \neg \left(\frac{x \cdot \left(y + z\right)}{z} \le -4.045134593776475081238842750214028354482 \cdot 10^{44} \lor \neg \left(\frac{x \cdot \left(y + z\right)}{z} \le 2.695397302024607118954686919516299646759 \cdot 10^{-102}\right) \land \frac{x \cdot \left(y + z\right)}{z} \le 1.963982869283896660652236439582473717883 \cdot 10^{219}\right):\\ \;\;\;\;x \cdot \frac{y + z}{z}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot \left(y + z\right)}{z}\\ \end{array}\]

Reproduce

herbie shell --seed 2019326 
(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))