Average Error: 8.4 → 3.9
Time: 7.4s
Precision: binary64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(1 + \sqrt{x1}\right)}^{12} \cdot {\left(1 - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
\frac{x0}{1 - x1} - x0
↓
\begin{array}{l}
\mathbf{if}\;1 - x1 \leq 0.9814:\\
\;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\

\mathbf{else}:\\
\;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(1 + \sqrt{x1}\right)}^{12} \cdot {\left(1 - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\

\end{array}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (if (<= (- 1.0 x1) 0.9814)
   (/
    (*
     x0
     (/
      (-
       (/
        (pow x0 3.0)
        (* (pow (+ 1.0 (sqrt x1)) 6.0) (pow (- 1.0 (sqrt x1)) 6.0)))
       (pow x0 3.0))
      (+
       (* x0 x0)
       (*
        (/ x0 (- 1.0 x1))
        (+ (/ x0 (- 1.0 x1)) (/ x0 (pow (- 1.0 x1) 3.0)))))))
    (+ x0 (/ x0 (- 1.0 x1))))
   (/
    (*
     x0
     (/
      (/
       (-
        (pow (/ (pow x0 3.0) (pow (- 1.0 x1) 6.0)) 3.0)
        (pow (pow x0 3.0) 3.0))
       (+
        (/
         (pow x0 6.0)
         (* (pow (+ 1.0 (sqrt x1)) 12.0) (pow (- 1.0 (sqrt x1)) 12.0)))
        (+ (pow x0 6.0) (pow (/ x0 (- 1.0 x1)) 6.0))))
      (+
       (* x0 x0)
       (*
        (/ x0 (- 1.0 x1))
        (+ (/ x0 (- 1.0 x1)) (/ x0 (pow (- 1.0 x1) 3.0)))))))
    (+ x0 (/ x0 (- 1.0 x1))))))
double code(double x0, double x1) {
	return (x0 / (1.0 - x1)) - x0;
}
↓
double code(double x0, double x1) {
	double tmp;
	if ((1.0 - x1) <= 0.9814) {
		tmp = (x0 * (((pow(x0, 3.0) / (pow((1.0 + sqrt(x1)), 6.0) * pow((1.0 - sqrt(x1)), 6.0))) - pow(x0, 3.0)) / ((x0 * x0) + ((x0 / (1.0 - x1)) * ((x0 / (1.0 - x1)) + (x0 / pow((1.0 - x1), 3.0))))))) / (x0 + (x0 / (1.0 - x1)));
	} else {
		tmp = (x0 * (((pow((pow(x0, 3.0) / pow((1.0 - x1), 6.0)), 3.0) - pow(pow(x0, 3.0), 3.0)) / ((pow(x0, 6.0) / (pow((1.0 + sqrt(x1)), 12.0) * pow((1.0 - sqrt(x1)), 12.0))) + (pow(x0, 6.0) + pow((x0 / (1.0 - x1)), 6.0)))) / ((x0 * x0) + ((x0 / (1.0 - x1)) * ((x0 / (1.0 - x1)) + (x0 / pow((1.0 - x1), 3.0))))))) / (x0 + (x0 / (1.0 - x1)));
	}
	return tmp;
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original8.4
Target0.5
Herbie3.9
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Split input into 2 regimes

  2. if (-.f64 1 x1) < 0.98140000000000005

    1. Initial program 5.5

      \[\frac{x0}{1 - x1} - x0\]
    2. Using strategy rm

    3. Applied flip--_binary64_31224.0

      \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

    4. Simplified4.7

      \[\leadsto \frac{\color{blue}{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]

    5. Simplified4.7

      \[\leadsto \frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\color{blue}{x0 + \frac{x0}{1 - x1}}}\]
    6. Using strategy rm

    7. Applied flip3--_binary64_31514.4

      \[\leadsto \frac{x0 \cdot \color{blue}{\frac{{\left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}^{3} - {x0}^{3}}{\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + \left(x0 \cdot x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot x0\right)}}}{x0 + \frac{x0}{1 - x1}}\]

    8. Simplified4.4

      \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}}{\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + \left(x0 \cdot x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot x0\right)}}{x0 + \frac{x0}{1 - x1}}\]

    9. Simplified4.4

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}{\color{blue}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}}{x0 + \frac{x0}{1 - x1}}\]
    10. Using strategy rm

    11. Applied add-sqr-sqrt_binary64_31694.4

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    12. Applied add-sqr-sqrt_binary64_31694.4

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    13. Applied difference-of-squares_binary64_31164.4

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\color{blue}{\left(\left(\sqrt{1} + \sqrt{x1}\right) \cdot \left(\sqrt{1} - \sqrt{x1}\right)\right)}}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    14. Applied unpow-prod-down_binary64_32261.6

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    15. Simplified1.6

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{\color{blue}{{\left(1 + \sqrt{x1}\right)}^{6}} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    16. Simplified1.6

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot \color{blue}{{\left(1 - \sqrt{x1}\right)}^{6}}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    if 0.98140000000000005 < (-.f64 1 x1)

    1. Initial program 11.3

      \[\frac{x0}{1 - x1} - x0\]
    2. Using strategy rm

    3. Applied flip--_binary64_312211.4

      \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

    4. Simplified9.1

      \[\leadsto \frac{\color{blue}{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]

    5. Simplified9.1

      \[\leadsto \frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\color{blue}{x0 + \frac{x0}{1 - x1}}}\]
    6. Using strategy rm

    7. Applied flip3--_binary64_31517.8

      \[\leadsto \frac{x0 \cdot \color{blue}{\frac{{\left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}^{3} - {x0}^{3}}{\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + \left(x0 \cdot x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot x0\right)}}}{x0 + \frac{x0}{1 - x1}}\]

    8. Simplified7.8

      \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}}{\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} + \left(x0 \cdot x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} \cdot x0\right)}}{x0 + \frac{x0}{1 - x1}}\]

    9. Simplified7.8

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}{\color{blue}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}}{x0 + \frac{x0}{1 - x1}}\]
    10. Using strategy rm

    11. Applied flip3--_binary64_31516.3

      \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} \cdot \frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} + \left({x0}^{3} \cdot {x0}^{3} + \frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} \cdot {x0}^{3}\right)}}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    12. Simplified6.3

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\color{blue}{\frac{{x0}^{6}}{{\left(1 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]
    13. Using strategy rm

    14. Applied add-sqr-sqrt_binary64_31696.3

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    15. Applied add-sqr-sqrt_binary64_31696.3

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    16. Applied difference-of-squares_binary64_31166.2

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\color{blue}{\left(\left(\sqrt{1} + \sqrt{x1}\right) \cdot \left(\sqrt{1} - \sqrt{x1}\right)\right)}}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    17. Applied unpow-prod-down_binary64_32266.2

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    18. Simplified6.2

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{\color{blue}{{\left(1 + \sqrt{x1}\right)}^{12}} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

    19. Simplified6.2

      \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(1 + \sqrt{x1}\right)}^{12} \cdot \color{blue}{{\left(1 - \sqrt{x1}\right)}^{12}}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification3.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(1 + \sqrt{x1}\right)}^{12} \cdot {\left(1 - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020356 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1.0 x1))

  (- (/ x0 (- 1.0 x1)) x0))