Average Error: 64.0 → 64.0
Time: 1.2min
Precision: binary64
Cost: 4736
\[1.9 \leq t \land t \leq 2.1\]
\[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308}\]
\[\frac{\frac{\sqrt{+\infty} + {\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308}
\frac{\frac{\sqrt{+\infty} + {\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}
(FPCore (t) :precision binary64 (- (* 1.7e+308 t) 1.7e+308))
(FPCore (t)
 :precision binary64
 (*
  (/
   (/
    (+ (sqrt +inf.0) (pow (* t 1.7e+308) 1.5))
    (cbrt
     (*
      (cbrt (+ +inf.0 (* t (+ +inf.0 (* t +inf.0)))))
      (cbrt (+ +inf.0 (* t (+ +inf.0 (* t +inf.0))))))))
   (*
    (cbrt (+ +inf.0 (* t (+ +inf.0 (* t +inf.0)))))
    (cbrt (+ +inf.0 (* t (+ +inf.0 (* t +inf.0)))))))
  (/
   (- (pow (* t 1.7e+308) 1.5) (sqrt +inf.0))
   (cbrt (cbrt (+ +inf.0 (* t (+ +inf.0 (* t +inf.0)))))))))
double code(double t) {
	return (1.7e+308 * t) - 1.7e+308;
}
double code(double t) {
	return (((sqrt(+inf.0) + pow((t * 1.7e+308), 1.5)) / cbrt(cbrt(+inf.0 + (t * (+inf.0 + (t * +inf.0)))) * cbrt(+inf.0 + (t * (+inf.0 + (t * +inf.0)))))) / (cbrt(+inf.0 + (t * (+inf.0 + (t * +inf.0)))) * cbrt(+inf.0 + (t * (+inf.0 + (t * +inf.0)))))) * ((pow((t * 1.7e+308), 1.5) - sqrt(+inf.0)) / cbrt(cbrt(+inf.0 + (t * (+inf.0 + (t * +inf.0))))));
}

Error

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original64.0
Target0
Herbie64.0
\[\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right)\]

Derivation

  1. Initial program 64.0

    \[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308}\]
  2. Using strategy rm
  3. Applied flip3--_binary64_76464.0

    \[\leadsto \color{blue}{\frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - {\left( 1.7 \cdot 10^{+308} \right)}^{3}}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)}}\]
  4. Simplified64.0

    \[\leadsto \frac{\color{blue}{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}}{\left(1.7 \cdot 10^{+308} \cdot t\right) \cdot \left(1.7 \cdot 10^{+308} \cdot t\right) + \left(1.7 \cdot 10^{+308} \cdot 1.7 \cdot 10^{+308} + \left(1.7 \cdot 10^{+308} \cdot t\right) \cdot 1.7 \cdot 10^{+308}\right)}\]
  5. Simplified64.0

    \[\leadsto \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}{\color{blue}{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}\]
  6. Using strategy rm
  7. Applied add-cube-cbrt_binary64_79564.0

    \[\leadsto \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}{\color{blue}{\left(\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}\right) \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  8. Applied *-un-lft-identity_binary64_76064.0

    \[\leadsto \frac{\color{blue}{1 \cdot \left({\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty\right)}}{\left(\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}\right) \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}\]
  9. Applied times-frac_binary64_76664.0

    \[\leadsto \color{blue}{\frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  10. Using strategy rm
  11. Applied add-cube-cbrt_binary64_79564.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}{\sqrt[3]{\color{blue}{\left(\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}\right) \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}\]
  12. Applied cbrt-prod_binary64_79164.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - +\infty}{\color{blue}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}\]
  13. Applied add-sqr-sqrt_binary64_78264.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{3} - \color{blue}{\sqrt{+\infty} \cdot \sqrt{+\infty}}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  14. Applied sqr-pow_binary64_73264.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{\color{blue}{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} \cdot {\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)}} - \sqrt{+\infty} \cdot \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  15. Applied difference-of-squares_binary64_72964.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{\color{blue}{\left({\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} + \sqrt{+\infty}\right) \cdot \left({\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} - \sqrt{+\infty}\right)}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  16. Applied times-frac_binary64_76664.0

    \[\leadsto \frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \color{blue}{\left(\frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} + \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\right)}\]
  17. Applied associate-*r*_binary64_70064.0

    \[\leadsto \color{blue}{\left(\frac{1}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} + \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\right) \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}\]
  18. Simplified64.0

    \[\leadsto \color{blue}{\frac{\frac{\sqrt{+\infty} + {\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + +\infty \cdot t\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + +\infty \cdot t\right)}}}}{\sqrt[3]{+\infty + t \cdot \left(+\infty + +\infty \cdot t\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + +\infty \cdot t\right)}}} \cdot \frac{{\left(1.7 \cdot 10^{+308} \cdot t\right)}^{\left(\frac{3}{2}\right)} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]
  19. Final simplification64.0

    \[\leadsto \frac{\frac{\sqrt{+\infty} + {\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}}{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)} \cdot \sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}} \cdot \frac{{\left(t \cdot 1.7 \cdot 10^{+308}\right)}^{1.5} - \sqrt{+\infty}}{\sqrt[3]{\sqrt[3]{+\infty + t \cdot \left(+\infty + t \cdot +\infty\right)}}}\]

Reproduce

herbie shell --seed 2020322 
(FPCore (t)
  :name "fma_test2"
  :precision binary64
  :pre (<= 1.9 t 2.1)

  :herbie-target
  (fma 1.7e+308 t (- 1.7e+308))

  (- (* 1.7e+308 t) 1.7e+308))