Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.6

Time: 1.9m

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

C

double f(double x1, double x2) {
        double r224367 = x1;
        double r224368 = 2.0;
        double r224369 = r224368 * r224367;
        double r224370 = 3.0;
        double r224371 = r224370 * r224367;
        double r224372 = r224371 * r224367;
        double r224373 = x2;
        double r224374 = r224368 * r224373;
        double r224375 = r224372 + r224374;
        double r224376 = r224375 - r224367;
        double r224377 = r224367 * r224367;
        double r224378 = 1.0;
        double r224379 = r224377 + r224378;
        double r224380 = r224376 / r224379;
        double r224381 = r224369 * r224380;
        double r224382 = r224380 - r224370;
        double r224383 = r224381 * r224382;
        double r224384 = 4.0;
        double r224385 = r224384 * r224380;
        double r224386 = 6.0;
        double r224387 = r224385 - r224386;
        double r224388 = r224377 * r224387;
        double r224389 = r224383 + r224388;
        double r224390 = r224389 * r224379;
        double r224391 = r224372 * r224380;
        double r224392 = r224390 + r224391;
        double r224393 = r224377 * r224367;
        double r224394 = r224392 + r224393;
        double r224395 = r224394 + r224367;
        double r224396 = r224372 - r224374;
        double r224397 = r224396 - r224367;
        double r224398 = r224397 / r224379;
        double r224399 = r224370 * r224398;
        double r224400 = r224395 + r224399;
        double r224401 = r224367 + r224400;
        return r224401;
}

↓

double f(double x1, double x2) {
        double r224402 = 3.0;
        double r224403 = x1;
        double r224404 = r224402 * r224403;
        double r224405 = r224404 * r224403;
        double r224406 = 2.0;
        double r224407 = x2;
        double r224408 = r224406 * r224407;
        double r224409 = r224405 + r224408;
        double r224410 = r224409 - r224403;
        double r224411 = r224403 * r224403;
        double r224412 = 1.0;
        double r224413 = r224411 + r224412;
        double r224414 = r224410 / r224413;
        double r224415 = r224414 - r224402;
        double r224416 = r224406 * r224403;
        double r224417 = r224415 * r224416;
        double r224418 = r224417 * r224413;
        double r224419 = r224405 + r224418;
        double r224420 = cbrt(r224419);
        double r224421 = r224420 * r224420;
        double r224422 = r224414 * r224421;
        double r224423 = r224422 * r224420;
        double r224424 = 4.0;
        double r224425 = r224424 * r224414;
        double r224426 = r224411 * r224425;
        double r224427 = r224413 * r224426;
        double r224428 = r224423 + r224427;
        double r224429 = 6.0;
        double r224430 = -r224429;
        double r224431 = r224411 * r224430;
        double r224432 = r224413 * r224431;
        double r224433 = r224428 + r224432;
        double r224434 = 3.0;
        double r224435 = pow(r224403, r224434);
        double r224436 = r224405 - r224408;
        double r224437 = r224436 - r224403;
        double r224438 = r224437 / r224413;
        double r224439 = r224402 * r224438;
        double r224440 = r224403 + r224439;
        double r224441 = r224440 + r224403;
        double r224442 = r224435 + r224441;
        double r224443 = r224433 + r224442;
        return r224443;
}

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. Simplified 0.5

   \[\leadsto \color{blue}{\left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} \cdot \left(\left(3 \cdot x1\right) \cdot x1 + \left(\left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) \cdot \left(2 \cdot x1\right)\right) \cdot \left(x1 \cdot x1 + 1\right)\right) + \left(x1 \cdot x1 + 1\right) \cdot \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} - 6\right)\right)\right) + \left({x1}^{3} + \left(\left(x1 + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + x1\right)\right)}\]
3. Using strategy rm

4. Applied sub-neg 0.5

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

5. Applied distribute-lft-in 0.5

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

6. Applied distribute-lft-in 0.5

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

7. Applied associate-+r+ 0.5

   \[\leadsto \color{blue}{\left(\left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} \cdot \left(\left(3 \cdot x1\right) \cdot x1 + \left(\left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) \cdot \left(2 \cdot x1\right)\right) \cdot \left(x1 \cdot x1 + 1\right)\right) + \left(x1 \cdot x1 + 1\right) \cdot \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)\right)\right) + \left(x1 \cdot x1 + 1\right) \cdot \left(\left(x1 \cdot x1\right) \cdot \left(-6\right)\right)\right)} + \left({x1}^{3} + \left(\left(x1 + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + x1\right)\right)\]
8. Using strategy rm

9. Applied add-cube-cbrt 0.6

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

10. Applied associate-*r* 0.6

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

11. Final simplification 0.6

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

Reproduce

herbie shell --seed 2019323 
(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))))))