Average Error: 20.2 → 5.4
Time: 10.8s
Precision: 64
\[0.0 \lt x \lt 1 \land y \lt 1\]
\[\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\]
↓
\[\begin{array}{l} \mathbf{if}\;y \le -1.932020237295699754397731718583308763603 \cdot 10^{146}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -1.096966360472084014807421275653766954731 \cdot 10^{-152}:\\ \;\;\;\;-\left(\frac{y \cdot y}{x \cdot x + y \cdot y} - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\ \mathbf{elif}\;y \le 8.13631030027101224197389572102430694003 \cdot 10^{-165}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-\left(\log \left(e^{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\ \end{array}\]
\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}
↓
\begin{array}{l}
\mathbf{if}\;y \le -1.932020237295699754397731718583308763603 \cdot 10^{146}:\\
\;\;\;\;-1\\

\mathbf{elif}\;y \le -1.096966360472084014807421275653766954731 \cdot 10^{-152}:\\
\;\;\;\;-\left(\frac{y \cdot y}{x \cdot x + y \cdot y} - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\

\mathbf{elif}\;y \le 8.13631030027101224197389572102430694003 \cdot 10^{-165}:\\
\;\;\;\;1\\

\mathbf{else}:\\
\;\;\;\;-\left(\log \left(e^{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\

\end{array}
double f(double x, double y) {
        double r6958695 = x;
        double r6958696 = y;
        double r6958697 = r6958695 - r6958696;
        double r6958698 = r6958695 + r6958696;
        double r6958699 = r6958697 * r6958698;
        double r6958700 = r6958695 * r6958695;
        double r6958701 = r6958696 * r6958696;
        double r6958702 = r6958700 + r6958701;
        double r6958703 = r6958699 / r6958702;
        return r6958703;
}
↓
double f(double x, double y) {
        double r6958704 = y;
        double r6958705 = -1.9320202372956998e+146;
        bool r6958706 = r6958704 <= r6958705;
        double r6958707 = -1.0;
        double r6958708 = -1.096966360472084e-152;
        bool r6958709 = r6958704 <= r6958708;
        double r6958710 = r6958704 * r6958704;
        double r6958711 = x;
        double r6958712 = r6958711 * r6958711;
        double r6958713 = r6958712 + r6958710;
        double r6958714 = r6958710 / r6958713;
        double r6958715 = r6958712 / r6958713;
        double r6958716 = r6958714 - r6958715;
        double r6958717 = -r6958716;
        double r6958718 = 8.136310300271012e-165;
        bool r6958719 = r6958704 <= r6958718;
        double r6958720 = 1.0;
        double r6958721 = exp(r6958714);
        double r6958722 = log(r6958721);
        double r6958723 = r6958722 - r6958715;
        double r6958724 = -r6958723;
        double r6958725 = r6958719 ? r6958720 : r6958724;
        double r6958726 = r6958709 ? r6958717 : r6958725;
        double r6958727 = r6958706 ? r6958707 : r6958726;
        return r6958727;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original20.2
Target0.1
Herbie5.4
\[\begin{array}{l} \mathbf{if}\;0.5 \lt \left|\frac{x}{y}\right| \lt 2:\\ \;\;\;\;\frac{\left(x - y\right) \cdot \left(x + y\right)}{x \cdot x + y \cdot y}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{2}{1 + \frac{x}{y} \cdot \frac{x}{y}}\\ \end{array}\]

Derivation

  1. Split input into 4 regimes

  2. if y < -1.9320202372956998e+146

    1. Initial program 60.8

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

    2. Simplified60.8

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

    3. Taylor expanded around inf 0

      \[\leadsto -\color{blue}{1}\]

    if -1.9320202372956998e+146 < y < -1.096966360472084e-152

    1. Initial program 0.0

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

    2. Simplified0.0

      \[\leadsto \color{blue}{-\frac{y \cdot y - x \cdot x}{x \cdot x + y \cdot y}}\]
    3. Using strategy rm

    4. Applied div-sub0.0

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

    if -1.096966360472084e-152 < y < 8.136310300271012e-165

    1. Initial program 29.0

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

    2. Simplified29.0

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

    3. Taylor expanded around 0 16.0

      \[\leadsto -\color{blue}{-1}\]

    if 8.136310300271012e-165 < y

    1. Initial program 0.7

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

    2. Simplified0.7

      \[\leadsto \color{blue}{-\frac{y \cdot y - x \cdot x}{x \cdot x + y \cdot y}}\]
    3. Using strategy rm

    4. Applied div-sub0.7

      \[\leadsto -\color{blue}{\left(\frac{y \cdot y}{x \cdot x + y \cdot y} - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)}\]
    5. Using strategy rm

    6. Applied add-log-exp0.7

      \[\leadsto -\left(\color{blue}{\log \left(e^{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right)} - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\]
  3. Recombined 4 regimes into one program.

  4. Final simplification5.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.932020237295699754397731718583308763603 \cdot 10^{146}:\\ \;\;\;\;-1\\ \mathbf{elif}\;y \le -1.096966360472084014807421275653766954731 \cdot 10^{-152}:\\ \;\;\;\;-\left(\frac{y \cdot y}{x \cdot x + y \cdot y} - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\ \mathbf{elif}\;y \le 8.13631030027101224197389572102430694003 \cdot 10^{-165}:\\ \;\;\;\;1\\ \mathbf{else}:\\ \;\;\;\;-\left(\log \left(e^{\frac{y \cdot y}{x \cdot x + y \cdot y}}\right) - \frac{x \cdot x}{x \cdot x + y \cdot y}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019171 
(FPCore (x y)
  :name "Kahan p9 Example"
  :pre (and (< 0.0 x 1.0) (< y 1.0))

  :herbie-target
  (if (< 0.5 (fabs (/ x y)) 2.0) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- 1.0 (/ 2.0 (+ 1.0 (* (/ x y) (/ x y))))))

  (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))))