Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.5

Time: 18.2s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

↓

\[x1 + \left(\left(\left(\left(\left(\mathsf{fma}\left(\frac{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \left(2 \cdot x1\right)}{\mathsf{fma}\left(x1, x1, 1\right)}, \mathsf{fma}\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1, \frac{1}{\mathsf{fma}\left(x1, x1, 1\right)}, -3\right), \left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right)\right) + \left(x1 \cdot x1\right) \cdot \left(-6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

C

double f(double x1, double x2) {
        double r49269 = x1;
        double r49270 = 2.0;
        double r49271 = r49270 * r49269;
        double r49272 = 3.0;
        double r49273 = r49272 * r49269;
        double r49274 = r49273 * r49269;
        double r49275 = x2;
        double r49276 = r49270 * r49275;
        double r49277 = r49274 + r49276;
        double r49278 = r49277 - r49269;
        double r49279 = r49269 * r49269;
        double r49280 = 1.0;
        double r49281 = r49279 + r49280;
        double r49282 = r49278 / r49281;
        double r49283 = r49271 * r49282;
        double r49284 = r49282 - r49272;
        double r49285 = r49283 * r49284;
        double r49286 = 4.0;
        double r49287 = r49286 * r49282;
        double r49288 = 6.0;
        double r49289 = r49287 - r49288;
        double r49290 = r49279 * r49289;
        double r49291 = r49285 + r49290;
        double r49292 = r49291 * r49281;
        double r49293 = r49274 * r49282;
        double r49294 = r49292 + r49293;
        double r49295 = r49279 * r49269;
        double r49296 = r49294 + r49295;
        double r49297 = r49296 + r49269;
        double r49298 = r49274 - r49276;
        double r49299 = r49298 - r49269;
        double r49300 = r49299 / r49281;
        double r49301 = r49272 * r49300;
        double r49302 = r49297 + r49301;
        double r49303 = r49269 + r49302;
        return r49303;
}

↓

double f(double x1, double x2) {
        double r49304 = x1;
        double r49305 = 3.0;
        double r49306 = r49305 * r49304;
        double r49307 = 2.0;
        double r49308 = x2;
        double r49309 = r49307 * r49308;
        double r49310 = fma(r49306, r49304, r49309);
        double r49311 = r49310 - r49304;
        double r49312 = r49307 * r49304;
        double r49313 = r49311 * r49312;
        double r49314 = 1.0;
        double r49315 = fma(r49304, r49304, r49314);
        double r49316 = r49313 / r49315;
        double r49317 = 1.0;
        double r49318 = r49317 / r49315;
        double r49319 = -r49305;
        double r49320 = fma(r49311, r49318, r49319);
        double r49321 = 4.0;
        double r49322 = r49311 / r49315;
        double r49323 = r49321 * r49322;
        double r49324 = r49304 * r49304;
        double r49325 = r49323 * r49324;
        double r49326 = fma(r49316, r49320, r49325);
        double r49327 = 6.0;
        double r49328 = -r49327;
        double r49329 = r49324 * r49328;
        double r49330 = r49326 + r49329;
        double r49331 = r49324 + r49314;
        double r49332 = r49330 * r49331;
        double r49333 = r49306 * r49304;
        double r49334 = r49333 + r49309;
        double r49335 = r49334 - r49304;
        double r49336 = r49335 / r49331;
        double r49337 = r49333 * r49336;
        double r49338 = r49332 + r49337;
        double r49339 = r49324 * r49304;
        double r49340 = r49338 + r49339;
        double r49341 = r49340 + r49304;
        double r49342 = r49333 - r49309;
        double r49343 = r49342 - r49304;
        double r49344 = r49343 / r49331;
        double r49345 = r49305 * r49344;
        double r49346 = r49341 + r49345;
        double r49347 = r49304 + r49346;
        return r49347;
}

Error

Bits error versus x1

Bits error versus x2

Derivation

1. Initial program 0.5

   \[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
2. Using strategy rm

3. Applied sub-neg 0.5

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

4. Applied distribute-lft-in 0.5

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

5. Applied associate-+r+ 0.5

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

6. Simplified 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\color{blue}{\mathsf{fma}\left(\frac{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \left(2 \cdot x1\right)}{\mathsf{fma}\left(x1, x1, 1\right)}, \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)} - 3, \left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right)\right)} + \left(x1 \cdot x1\right) \cdot \left(-6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
7. Using strategy rm

8. Applied div-inv 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\mathsf{fma}\left(\frac{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \left(2 \cdot x1\right)}{\mathsf{fma}\left(x1, x1, 1\right)}, \color{blue}{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \frac{1}{\mathsf{fma}\left(x1, x1, 1\right)}} - 3, \left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right)\right) + \left(x1 \cdot x1\right) \cdot \left(-6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

9. Applied fma-neg 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\mathsf{fma}\left(\frac{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \left(2 \cdot x1\right)}{\mathsf{fma}\left(x1, x1, 1\right)}, \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1, \frac{1}{\mathsf{fma}\left(x1, x1, 1\right)}, -3\right)}, \left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right)\right) + \left(x1 \cdot x1\right) \cdot \left(-6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

10. Final simplification 0.5

    \[\leadsto x1 + \left(\left(\left(\left(\left(\mathsf{fma}\left(\frac{\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1\right) \cdot \left(2 \cdot x1\right)}{\mathsf{fma}\left(x1, x1, 1\right)}, \mathsf{fma}\left(\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1, \frac{1}{\mathsf{fma}\left(x1, x1, 1\right)}, -3\right), \left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right)\right) + \left(x1 \cdot x1\right) \cdot \left(-6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

Reproduce

herbie shell --seed 2020042 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  :precision binary64
  (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))))