Average Error: 14.7 → 0.1
Time: 3.7s
Precision: binary64
\[\frac{\left(x \cdot 2\right) \cdot y}{x - y}\]
↓
\[\frac{{0.5}^{-0.5}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]
\frac{\left(x \cdot 2\right) \cdot y}{x - y}
↓
\frac{{0.5}^{-0.5}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}
(FPCore (x y) :precision binary64 (/ (* (* x 2.0) y) (- x y)))
↓
(FPCore (x y)
 :precision binary64
 (/ (pow 0.5 -0.5) (- (/ (sqrt 0.5) y) (/ (sqrt 0.5) x))))
double code(double x, double y) {
	return ((x * 2.0) * y) / (x - y);
}
↓
double code(double x, double y) {
	return pow(0.5, -0.5) / ((sqrt(0.5) / y) - (sqrt(0.5) / x));
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original14.7
Target0.4
Herbie0.1
\[\begin{array}{l} \mathbf{if}\;x < -1.7210442634149447 \cdot 10^{+81}:\\ \;\;\;\;\frac{2 \cdot x}{x - y} \cdot y\\ \mathbf{elif}\;x < 8.364504563556443 \cdot 10^{+16}:\\ \;\;\;\;\frac{x \cdot 2}{\frac{x - y}{y}}\\ \mathbf{else}:\\ \;\;\;\;\frac{2 \cdot x}{x - y} \cdot y\\ \end{array}\]

Derivation

  1. Initial program 14.7

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

  3. Applied clear-num_binary6414.8

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

  4. Simplified0.2

    \[\leadsto \frac{1}{\color{blue}{\frac{0.5}{y} - \frac{0.5}{x}}}\]
  5. Using strategy rm

  6. Applied *-un-lft-identity_binary640.2

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

  7. Applied add-sqr-sqrt_binary640.7

    \[\leadsto \frac{1}{\frac{0.5}{y} - \frac{\color{blue}{\sqrt{0.5} \cdot \sqrt{0.5}}}{1 \cdot x}}\]

  8. Applied times-frac_binary640.5

    \[\leadsto \frac{1}{\frac{0.5}{y} - \color{blue}{\frac{\sqrt{0.5}}{1} \cdot \frac{\sqrt{0.5}}{x}}}\]

  9. Applied *-un-lft-identity_binary640.5

    \[\leadsto \frac{1}{\frac{0.5}{\color{blue}{1 \cdot y}} - \frac{\sqrt{0.5}}{1} \cdot \frac{\sqrt{0.5}}{x}}\]

  10. Applied add-sqr-sqrt_binary641.1

    \[\leadsto \frac{1}{\frac{\color{blue}{\sqrt{0.5} \cdot \sqrt{0.5}}}{1 \cdot y} - \frac{\sqrt{0.5}}{1} \cdot \frac{\sqrt{0.5}}{x}}\]

  11. Applied times-frac_binary640.9

    \[\leadsto \frac{1}{\color{blue}{\frac{\sqrt{0.5}}{1} \cdot \frac{\sqrt{0.5}}{y}} - \frac{\sqrt{0.5}}{1} \cdot \frac{\sqrt{0.5}}{x}}\]

  12. Applied distribute-lft-out--_binary640.9

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

  13. Applied add-sqr-sqrt_binary640.9

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

  14. Applied times-frac_binary641.0

    \[\leadsto \color{blue}{\frac{\sqrt{1}}{\frac{\sqrt{0.5}}{1}} \cdot \frac{\sqrt{1}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}}\]

  15. Simplified1.0

    \[\leadsto \color{blue}{\frac{1}{\sqrt{0.5}}} \cdot \frac{\sqrt{1}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]

  16. Simplified1.0

    \[\leadsto \frac{1}{\sqrt{0.5}} \cdot \color{blue}{\frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}}\]
  17. Using strategy rm

  18. Applied pow1/2_binary641.0

    \[\leadsto \frac{1}{\color{blue}{{0.5}^{0.5}}} \cdot \frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]

  19. Applied pow-flip_binary640.3

    \[\leadsto \color{blue}{{0.5}^{\left(-0.5\right)}} \cdot \frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]

  20. Simplified0.3

    \[\leadsto {0.5}^{\color{blue}{-0.5}} \cdot \frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]
  21. Using strategy rm

  22. Applied *-un-lft-identity_binary640.3

    \[\leadsto \color{blue}{\left(1 \cdot {0.5}^{-0.5}\right)} \cdot \frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]

  23. Applied associate-*l*_binary640.3

    \[\leadsto \color{blue}{1 \cdot \left({0.5}^{-0.5} \cdot \frac{1}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\right)}\]

  24. Simplified0.1

    \[\leadsto 1 \cdot \color{blue}{\frac{{0.5}^{-0.5}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}}\]

  25. Final simplification0.1

    \[\leadsto \frac{{0.5}^{-0.5}}{\frac{\sqrt{0.5}}{y} - \frac{\sqrt{0.5}}{x}}\]

Reproduce

herbie shell --seed 2021128 
(FPCore (x y)
  :name "Linear.Projection:perspective from linear-1.19.1.3, B"
  :precision binary64

  :herbie-target
  (if (< x -1.7210442634149447e+81) (* (/ (* 2.0 x) (- x y)) y) (if (< x 8.364504563556443e+16) (/ (* x 2.0) (/ (- x y) y)) (* (/ (* 2.0 x) (- x y)) y)))

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