1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}(FPCore (x) :precision binary64 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
double code(double x) {
return 1.0 - sqrt(0.5 * (1.0 + (1.0 / hypot(1.0, x))));
}
Please include this information when filing a bug report:
herbie shell --seed 2021060
(FPCore (x)
:name "Given's Rotation SVD example, simplified"
:precision binary64
(- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
| Failed to produce proof for (*.f64 (neg.f64 (*.f64 (cbrt.f64 (sqrt.f64 (+.f64 1/2 (/.f64 1/2 (hypot.f64 1 x))))) (cbrt.f64 (sqrt.f64 (+.f64 1/2 (/.f64 1/2 (hypot.f64 1 x))))))) (cbrt.f64 (sqrt.f64 (+.f64 1/2 (/.f64 1/2 (hypot.f64 1 x)))))) to (neg.f64 (sqrt.f64 (+.f64 1/2 (/.f64 1/2 (hypot.f64 1 x))))) | L | C | |
|---|---|---|---|
| for-loop | /data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt | 167 | 8 |
| (unnamed) | /data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt | 149 | 6 |
| egraph-add-exprs | /data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt | 154 | 0 |
| with-egraph | /data/pavpan/nightlies/herbie/egg-generate-proof/egg-herbie/main.rkt | 74 | 0 |
| (unnamed) | /data/pavpan/nightlies/herbie/egg-generate-proof/src/core/simplify.rkt | 79 | 0 |
| simplify! | /data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt | 236 | 0 |
| run-iter! | /data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt | 360 | 0 |
| run-improve | /data/pavpan/nightlies/herbie/egg-generate-proof/src/mainloop.rkt | 377 | 0 |
| (unnamed) | /data/pavpan/nightlies/herbie/egg-generate-proof/src/sandbox.rkt | 54 | 6 |
| run | /opt/racket-7.9/share/pkgs/profile-lib/main.rkt | 39 | 2 |
| profile-thunk | /opt/racket-7.9/share/pkgs/profile-lib/main.rkt | 9 | 0 |
| (unnamed) | /opt/racket-7.9/collects/racket/engine.rkt | 42 | 24 |