Average Error: 11.7 → 3.1
Time: 16.8s
Precision: 64
\[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\]
↓
\[\begin{array}{l} \mathbf{if}\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y} \le 6.699887162447185181796079741399604536537 \cdot 10^{61}:\\ \;\;\;\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{y}{\mathsf{fma}\left(\frac{y}{z}, -t, z \cdot 2\right)}, -2, x\right)\\ \end{array}\]
x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}
↓
\begin{array}{l}
\mathbf{if}\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y} \le 6.699887162447185181796079741399604536537 \cdot 10^{61}:\\
\;\;\;\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(\frac{y}{\mathsf{fma}\left(\frac{y}{z}, -t, z \cdot 2\right)}, -2, x\right)\\

\end{array}
double f(double x, double y, double z, double t) {
        double r335881 = x;
        double r335882 = y;
        double r335883 = 2.0;
        double r335884 = r335882 * r335883;
        double r335885 = z;
        double r335886 = r335884 * r335885;
        double r335887 = r335885 * r335883;
        double r335888 = r335887 * r335885;
        double r335889 = t;
        double r335890 = r335882 * r335889;
        double r335891 = r335888 - r335890;
        double r335892 = r335886 / r335891;
        double r335893 = r335881 - r335892;
        return r335893;
}
↓
double f(double x, double y, double z, double t) {
        double r335894 = x;
        double r335895 = 2.0;
        double r335896 = y;
        double r335897 = r335895 * r335896;
        double r335898 = z;
        double r335899 = r335897 * r335898;
        double r335900 = r335898 * r335895;
        double r335901 = r335900 * r335898;
        double r335902 = t;
        double r335903 = r335902 * r335896;
        double r335904 = r335901 - r335903;
        double r335905 = r335899 / r335904;
        double r335906 = r335894 - r335905;
        double r335907 = 6.699887162447185e+61;
        bool r335908 = r335906 <= r335907;
        double r335909 = r335896 / r335898;
        double r335910 = -r335902;
        double r335911 = fma(r335909, r335910, r335900);
        double r335912 = r335896 / r335911;
        double r335913 = -r335895;
        double r335914 = fma(r335912, r335913, r335894);
        double r335915 = r335908 ? r335906 : r335914;
        return r335915;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original11.7
Target0.1
Herbie3.1
\[x - \frac{1}{\frac{z}{y} - \frac{\frac{t}{2}}{z}}\]

Derivation

  1. Split input into 2 regimes

  2. if (- x (/ (* (* y 2.0) z) (- (* (* z 2.0) z) (* y t)))) < 6.699887162447185e+61

    1. Initial program 3.9

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\]

    if 6.699887162447185e+61 < (- x (/ (* (* y 2.0) z) (- (* (* z 2.0) z) (* y t))))

    1. Initial program 27.4

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\]

    2. Simplified1.6

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y}{\mathsf{fma}\left(\frac{y}{z}, -t, z \cdot 2\right)}, -2, x\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification3.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y} \le 6.699887162447185181796079741399604536537 \cdot 10^{61}:\\ \;\;\;\;x - \frac{\left(2 \cdot y\right) \cdot z}{\left(z \cdot 2\right) \cdot z - t \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{y}{\mathsf{fma}\left(\frac{y}{z}, -t, z \cdot 2\right)}, -2, x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 +o rules:numerics
(FPCore (x y z t)
  :name "Numeric.AD.Rank1.Halley:findZero from ad-4.2.4"

  :herbie-target
  (- x (/ 1.0 (- (/ z y) (/ (/ t 2.0) z))))

  (- x (/ (* (* y 2.0) z) (- (* (* z 2.0) z) (* y t)))))