Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.5

Time: 50.8s

Precision: 64

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)\]

↓

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

C

double f(double x1, double x2) {
        double r2031368 = x1;
        double r2031369 = 2.0;
        double r2031370 = r2031369 * r2031368;
        double r2031371 = 3.0;
        double r2031372 = r2031371 * r2031368;
        double r2031373 = r2031372 * r2031368;
        double r2031374 = x2;
        double r2031375 = r2031369 * r2031374;
        double r2031376 = r2031373 + r2031375;
        double r2031377 = r2031376 - r2031368;
        double r2031378 = r2031368 * r2031368;
        double r2031379 = 1.0;
        double r2031380 = r2031378 + r2031379;
        double r2031381 = r2031377 / r2031380;
        double r2031382 = r2031370 * r2031381;
        double r2031383 = r2031381 - r2031371;
        double r2031384 = r2031382 * r2031383;
        double r2031385 = 4.0;
        double r2031386 = r2031385 * r2031381;
        double r2031387 = 6.0;
        double r2031388 = r2031386 - r2031387;
        double r2031389 = r2031378 * r2031388;
        double r2031390 = r2031384 + r2031389;
        double r2031391 = r2031390 * r2031380;
        double r2031392 = r2031373 * r2031381;
        double r2031393 = r2031391 + r2031392;
        double r2031394 = r2031378 * r2031368;
        double r2031395 = r2031393 + r2031394;
        double r2031396 = r2031395 + r2031368;
        double r2031397 = r2031373 - r2031375;
        double r2031398 = r2031397 - r2031368;
        double r2031399 = r2031398 / r2031380;
        double r2031400 = r2031371 * r2031399;
        double r2031401 = r2031396 + r2031400;
        double r2031402 = r2031368 + r2031401;
        return r2031402;
}

↓

double f(double x1, double x2) {
        double r2031403 = x1;
        double r2031404 = 3.0;
        double r2031405 = r2031404 * r2031403;
        double r2031406 = r2031405 * r2031403;
        double r2031407 = x2;
        double r2031408 = 2.0;
        double r2031409 = r2031407 * r2031408;
        double r2031410 = r2031406 + r2031409;
        double r2031411 = r2031410 - r2031403;
        double r2031412 = 1.0;
        double r2031413 = r2031403 * r2031403;
        double r2031414 = r2031412 + r2031413;
        double r2031415 = r2031411 / r2031414;
        double r2031416 = r2031406 * r2031415;
        double r2031417 = 6.0;
        double r2031418 = -r2031413;
        double r2031419 = r2031417 * r2031418;
        double r2031420 = r2031415 - r2031404;
        double r2031421 = r2031403 * r2031408;
        double r2031422 = r2031421 * r2031415;
        double r2031423 = r2031420 * r2031422;
        double r2031424 = 8.0;
        double r2031425 = r2031407 * r2031424;
        double r2031426 = r2031425 * r2031413;
        double r2031427 = 12.0;
        double r2031428 = r2031413 * r2031413;
        double r2031429 = r2031427 * r2031428;
        double r2031430 = 4.0;
        double r2031431 = r2031430 * r2031403;
        double r2031432 = r2031431 * r2031413;
        double r2031433 = r2031429 - r2031432;
        double r2031434 = r2031426 + r2031433;
        double r2031435 = r2031434 / r2031414;
        double r2031436 = r2031423 + r2031435;
        double r2031437 = r2031419 + r2031436;
        double r2031438 = r2031414 * r2031437;
        double r2031439 = r2031416 + r2031438;
        double r2031440 = r2031403 * r2031413;
        double r2031441 = r2031439 + r2031440;
        double r2031442 = r2031403 + r2031441;
        double r2031443 = r2031406 - r2031409;
        double r2031444 = r2031443 - r2031403;
        double r2031445 = r2031444 / r2031414;
        double r2031446 = r2031404 * r2031445;
        double r2031447 = r2031442 + r2031446;
        double r2031448 = r2031447 + r2031403;
        return r2031448;
}

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-rgt-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(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(x1 \cdot x1\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(x1 \cdot x1\right)\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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. Using strategy rm

7. Applied associate-*r/ 0.5

   \[\leadsto x1 + \left(\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}{\frac{4 \cdot \left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right)}{x1 \cdot x1 + 1}} \cdot \left(x1 \cdot x1\right)\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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)\]

8. Applied associate-*l/ 0.5

   \[\leadsto x1 + \left(\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}{\frac{\left(4 \cdot \left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right)\right) \cdot \left(x1 \cdot x1\right)}{x1 \cdot x1 + 1}}\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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. Taylor expanded around 0 0.5

   \[\leadsto x1 + \left(\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) + \frac{\color{blue}{\left(8 \cdot \left({x1}^{2} \cdot x2\right) + 12 \cdot {x1}^{4}\right) - 4 \cdot {x1}^{3}}}{x1 \cdot x1 + 1}\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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. Simplified 0.5

    \[\leadsto x1 + \left(\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) + \frac{\color{blue}{\left(8 \cdot x2\right) \cdot \left(x1 \cdot x1\right) + \left(12 \cdot \left(\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right)\right) - \left(4 \cdot x1\right) \cdot \left(x1 \cdot x1\right)\right)}}{x1 \cdot x1 + 1}\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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)\]

11. Final simplification 0.5

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

Reproduce

herbie shell --seed 2019179 
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2.0 x1) (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))) (- (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0)) 3.0)) (* (* x1 x1) (- (* 4.0 (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))) 6.0))) (+ (* x1 x1) 1.0)) (* (* (* 3.0 x1) x1) (/ (- (+ (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0)))) (* (* x1 x1) x1)) x1) (* 3.0 (/ (- (- (* (* 3.0 x1) x1) (* 2.0 x2)) x1) (+ (* x1 x1) 1.0))))))