Average Error: 0.5 → 0.5
Time: 1.2m
Precision: 64
\[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(\left(\left(\left(x1 \cdot x1\right) \cdot \left(\frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1} \cdot 4 - 6\right) + \left(\left(2 \cdot x1\right) \cdot \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}, -3\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1} \cdot \left(\left(3 \cdot x1\right) \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot x1\right)\right) + x1\right) + \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{x1 \cdot x1 + 1} \cdot 3\right) + x1\]
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(\left(\left(\left(x1 \cdot x1\right) \cdot \left(\frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1} \cdot 4 - 6\right) + \left(\left(2 \cdot x1\right) \cdot \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}, -3\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \frac{\left(x2 \cdot 2 + \left(3 \cdot x1\right) \cdot x1\right) - x1}{x1 \cdot x1 + 1} \cdot \left(\left(3 \cdot x1\right) \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot x1\right)\right) + x1\right) + \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{x1 \cdot x1 + 1} \cdot 3\right) + x1
double f(double x1, double x2) {
        double r2594419 = x1;
        double r2594420 = 2.0;
        double r2594421 = r2594420 * r2594419;
        double r2594422 = 3.0;
        double r2594423 = r2594422 * r2594419;
        double r2594424 = r2594423 * r2594419;
        double r2594425 = x2;
        double r2594426 = r2594420 * r2594425;
        double r2594427 = r2594424 + r2594426;
        double r2594428 = r2594427 - r2594419;
        double r2594429 = r2594419 * r2594419;
        double r2594430 = 1.0;
        double r2594431 = r2594429 + r2594430;
        double r2594432 = r2594428 / r2594431;
        double r2594433 = r2594421 * r2594432;
        double r2594434 = r2594432 - r2594422;
        double r2594435 = r2594433 * r2594434;
        double r2594436 = 4.0;
        double r2594437 = r2594436 * r2594432;
        double r2594438 = 6.0;
        double r2594439 = r2594437 - r2594438;
        double r2594440 = r2594429 * r2594439;
        double r2594441 = r2594435 + r2594440;
        double r2594442 = r2594441 * r2594431;
        double r2594443 = r2594424 * r2594432;
        double r2594444 = r2594442 + r2594443;
        double r2594445 = r2594429 * r2594419;
        double r2594446 = r2594444 + r2594445;
        double r2594447 = r2594446 + r2594419;
        double r2594448 = r2594424 - r2594426;
        double r2594449 = r2594448 - r2594419;
        double r2594450 = r2594449 / r2594431;
        double r2594451 = r2594422 * r2594450;
        double r2594452 = r2594447 + r2594451;
        double r2594453 = r2594419 + r2594452;
        return r2594453;
}
↓
double f(double x1, double x2) {
        double r2594454 = x1;
        double r2594455 = r2594454 * r2594454;
        double r2594456 = x2;
        double r2594457 = 2.0;
        double r2594458 = r2594456 * r2594457;
        double r2594459 = 3.0;
        double r2594460 = r2594459 * r2594454;
        double r2594461 = r2594460 * r2594454;
        double r2594462 = r2594458 + r2594461;
        double r2594463 = r2594462 - r2594454;
        double r2594464 = 1.0;
        double r2594465 = r2594455 + r2594464;
        double r2594466 = r2594463 / r2594465;
        double r2594467 = 4.0;
        double r2594468 = r2594466 * r2594467;
        double r2594469 = 6.0;
        double r2594470 = r2594468 - r2594469;
        double r2594471 = r2594455 * r2594470;
        double r2594472 = r2594457 * r2594454;
        double r2594473 = r2594472 * r2594466;
        double r2594474 = 1.0;
        double r2594475 = cbrt(r2594465);
        double r2594476 = r2594475 * r2594475;
        double r2594477 = r2594474 / r2594476;
        double r2594478 = r2594463 / r2594475;
        double r2594479 = -r2594459;
        double r2594480 = fma(r2594477, r2594478, r2594479);
        double r2594481 = r2594473 * r2594480;
        double r2594482 = r2594471 + r2594481;
        double r2594483 = r2594482 * r2594465;
        double r2594484 = r2594466 * r2594461;
        double r2594485 = r2594483 + r2594484;
        double r2594486 = r2594454 * r2594455;
        double r2594487 = r2594485 + r2594486;
        double r2594488 = r2594487 + r2594454;
        double r2594489 = r2594461 - r2594458;
        double r2594490 = r2594489 - r2594454;
        double r2594491 = r2594490 / r2594465;
        double r2594492 = r2594491 * r2594459;
        double r2594493 = r2594488 + r2594492;
        double r2594494 = r2594493 + r2594454;
        return r2594494;
}

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 add-cube-cbrt0.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}{\color{blue}{\left(\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}\right) \cdot \sqrt[3]{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)\]

  4. Applied *-un-lft-identity0.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{\color{blue}{1 \cdot \left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right)}}{\left(\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}\right) \cdot \sqrt[3]{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)\]

  5. Applied times-frac0.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(\color{blue}{\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}} \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{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)\]

  6. Applied fma-neg0.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 \color{blue}{\mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{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)\]

  7. Final simplification0.5

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

Reproduce

herbie shell --seed 2019200 +o rules:numerics
(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))))))