Average Error: 11.6 → 1.3
Time: 3.3s
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(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \le 1.02419627893532343 \cdot 10^{179}:\\ \;\;\;\;x - \left(y \cdot 2\right) \cdot \frac{1}{2 \cdot z - \frac{t \cdot y}{z}}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y \cdot 2}{1 \cdot \left(2 \cdot z - t \cdot \frac{y}{z}\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(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \le 1.02419627893532343 \cdot 10^{179}:\\
\;\;\;\;x - \left(y \cdot 2\right) \cdot \frac{1}{2 \cdot z - \frac{t \cdot y}{z}}\\

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

\end{array}
double f(double x, double y, double z, double t) {
        double r504900 = x;
        double r504901 = y;
        double r504902 = 2.0;
        double r504903 = r504901 * r504902;
        double r504904 = z;
        double r504905 = r504903 * r504904;
        double r504906 = r504904 * r504902;
        double r504907 = r504906 * r504904;
        double r504908 = t;
        double r504909 = r504901 * r504908;
        double r504910 = r504907 - r504909;
        double r504911 = r504905 / r504910;
        double r504912 = r504900 - r504911;
        return r504912;
}
↓
double f(double x, double y, double z, double t) {
        double r504913 = x;
        double r504914 = y;
        double r504915 = 2.0;
        double r504916 = r504914 * r504915;
        double r504917 = z;
        double r504918 = r504916 * r504917;
        double r504919 = r504917 * r504915;
        double r504920 = r504919 * r504917;
        double r504921 = t;
        double r504922 = r504914 * r504921;
        double r504923 = r504920 - r504922;
        double r504924 = r504918 / r504923;
        double r504925 = r504913 - r504924;
        double r504926 = 1.0241962789353234e+179;
        bool r504927 = r504925 <= r504926;
        double r504928 = 1.0;
        double r504929 = r504915 * r504917;
        double r504930 = r504921 * r504914;
        double r504931 = r504930 / r504917;
        double r504932 = r504929 - r504931;
        double r504933 = r504928 / r504932;
        double r504934 = r504916 * r504933;
        double r504935 = r504913 - r504934;
        double r504936 = r504914 / r504917;
        double r504937 = r504921 * r504936;
        double r504938 = r504929 - r504937;
        double r504939 = r504928 * r504938;
        double r504940 = r504916 / r504939;
        double r504941 = r504913 - r504940;
        double r504942 = r504927 ? r504935 : r504941;
        return r504942;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original11.6
Target0.1
Herbie1.3
\[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)))) < 1.0241962789353234e+179

    1. Initial program 2.9

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

    3. Applied associate-/l*2.0

      \[\leadsto x - \color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\]
    4. Using strategy rm

    5. Applied *-un-lft-identity2.0

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

    6. Applied *-un-lft-identity2.0

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

    7. Applied times-frac2.0

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

    8. Simplified2.0

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

    9. Simplified1.2

      \[\leadsto x - \frac{y \cdot 2}{1 \cdot \color{blue}{\left(2 \cdot z - \frac{t \cdot y}{z}\right)}}\]
    10. Using strategy rm

    11. Applied div-inv1.3

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

    12. Simplified1.3

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

    if 1.0241962789353234e+179 < (- x (/ (* (* y 2.0) z) (- (* (* z 2.0) z) (* y t))))

    1. Initial program 39.3

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

    3. Applied associate-/l*21.7

      \[\leadsto x - \color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\]
    4. Using strategy rm

    5. Applied *-un-lft-identity21.7

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

    6. Applied *-un-lft-identity21.7

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

    7. Applied times-frac21.7

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

    8. Simplified21.7

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

    9. Simplified8.7

      \[\leadsto x - \frac{y \cdot 2}{1 \cdot \color{blue}{\left(2 \cdot z - \frac{t \cdot y}{z}\right)}}\]
    10. Using strategy rm

    11. Applied *-un-lft-identity8.7

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

    12. Applied times-frac1.4

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

    13. Simplified1.4

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

  4. Final simplification1.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \le 1.02419627893532343 \cdot 10^{179}:\\ \;\;\;\;x - \left(y \cdot 2\right) \cdot \frac{1}{2 \cdot z - \frac{t \cdot y}{z}}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{y \cdot 2}{1 \cdot \left(2 \cdot z - t \cdot \frac{y}{z}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 
(FPCore (x y z t)
  :name "Numeric.AD.Rank1.Halley:findZero from ad-4.2.4"
  :precision binary64

  :herbie-target
  (- x (/ 1 (- (/ z y) (/ (/ t 2) z))))

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