Average Error: 0.5 → 0.5
Time: 52.1s
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)\]
↓
\[x1 + \left(\left(\left(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(\left(x1 \cdot 3\right) \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} + \left(1 + x1 \cdot x1\right) \cdot \left(\left(\left(x1 \cdot x1\right) \cdot \left(\frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} \cdot 4 - 6\right) + \mathsf{fma}\left(-3, 1, 3\right) \cdot \left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1}\right)\right) + \left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1}\right) \cdot \mathsf{fma}\left(\frac{1}{\sqrt{1 + x1 \cdot x1}}, \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{1 + x1 \cdot x1}}, -3\right)\right)\right)\right) + x1\right) + \frac{\left(\left(x1 \cdot 3\right) \cdot x1 - 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} \cdot 3\right)\]
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(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(\left(x1 \cdot 3\right) \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} + \left(1 + x1 \cdot x1\right) \cdot \left(\left(\left(x1 \cdot x1\right) \cdot \left(\frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} \cdot 4 - 6\right) + \mathsf{fma}\left(-3, 1, 3\right) \cdot \left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1}\right)\right) + \left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{1 + x1 \cdot x1}\right) \cdot \mathsf{fma}\left(\frac{1}{\sqrt{1 + x1 \cdot x1}}, \frac{\left(\left(x1 \cdot 3\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{1 + x1 \cdot x1}}, -3\right)\right)\right)\right) + x1\right) + \frac{\left(\left(x1 \cdot 3\right) \cdot x1 - 2 \cdot x2\right) - x1}{1 + x1 \cdot x1} \cdot 3\right)
double f(double x1, double x2) {
        double r2341423 = x1;
        double r2341424 = 2.0;
        double r2341425 = r2341424 * r2341423;
        double r2341426 = 3.0;
        double r2341427 = r2341426 * r2341423;
        double r2341428 = r2341427 * r2341423;
        double r2341429 = x2;
        double r2341430 = r2341424 * r2341429;
        double r2341431 = r2341428 + r2341430;
        double r2341432 = r2341431 - r2341423;
        double r2341433 = r2341423 * r2341423;
        double r2341434 = 1.0;
        double r2341435 = r2341433 + r2341434;
        double r2341436 = r2341432 / r2341435;
        double r2341437 = r2341425 * r2341436;
        double r2341438 = r2341436 - r2341426;
        double r2341439 = r2341437 * r2341438;
        double r2341440 = 4.0;
        double r2341441 = r2341440 * r2341436;
        double r2341442 = 6.0;
        double r2341443 = r2341441 - r2341442;
        double r2341444 = r2341433 * r2341443;
        double r2341445 = r2341439 + r2341444;
        double r2341446 = r2341445 * r2341435;
        double r2341447 = r2341428 * r2341436;
        double r2341448 = r2341446 + r2341447;
        double r2341449 = r2341433 * r2341423;
        double r2341450 = r2341448 + r2341449;
        double r2341451 = r2341450 + r2341423;
        double r2341452 = r2341428 - r2341430;
        double r2341453 = r2341452 - r2341423;
        double r2341454 = r2341453 / r2341435;
        double r2341455 = r2341426 * r2341454;
        double r2341456 = r2341451 + r2341455;
        double r2341457 = r2341423 + r2341456;
        return r2341457;
}
↓
double f(double x1, double x2) {
        double r2341458 = x1;
        double r2341459 = r2341458 * r2341458;
        double r2341460 = r2341458 * r2341459;
        double r2341461 = 3.0;
        double r2341462 = r2341458 * r2341461;
        double r2341463 = r2341462 * r2341458;
        double r2341464 = 2.0;
        double r2341465 = x2;
        double r2341466 = r2341464 * r2341465;
        double r2341467 = r2341463 + r2341466;
        double r2341468 = r2341467 - r2341458;
        double r2341469 = 1.0;
        double r2341470 = r2341469 + r2341459;
        double r2341471 = r2341468 / r2341470;
        double r2341472 = r2341463 * r2341471;
        double r2341473 = 4.0;
        double r2341474 = r2341471 * r2341473;
        double r2341475 = 6.0;
        double r2341476 = r2341474 - r2341475;
        double r2341477 = r2341459 * r2341476;
        double r2341478 = -3.0;
        double r2341479 = fma(r2341478, r2341469, r2341461);
        double r2341480 = r2341464 * r2341458;
        double r2341481 = r2341480 * r2341471;
        double r2341482 = r2341479 * r2341481;
        double r2341483 = r2341477 + r2341482;
        double r2341484 = sqrt(r2341470);
        double r2341485 = r2341469 / r2341484;
        double r2341486 = r2341468 / r2341484;
        double r2341487 = fma(r2341485, r2341486, r2341478);
        double r2341488 = r2341481 * r2341487;
        double r2341489 = r2341483 + r2341488;
        double r2341490 = r2341470 * r2341489;
        double r2341491 = r2341472 + r2341490;
        double r2341492 = r2341460 + r2341491;
        double r2341493 = r2341492 + r2341458;
        double r2341494 = r2341463 - r2341466;
        double r2341495 = r2341494 - r2341458;
        double r2341496 = r2341495 / r2341470;
        double r2341497 = r2341496 * r2341461;
        double r2341498 = r2341493 + r2341497;
        double r2341499 = r2341458 + r2341498;
        return r2341499;
}

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 *-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{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - \color{blue}{1 \cdot 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 add-sqr-sqrt0.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}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}}} - 1 \cdot 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 *-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)}}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}} - 1 \cdot 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 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{x1 \cdot x1 + 1}} \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}} - 1 \cdot 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. Applied prod-diff0.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}{\left(\mathsf{fma}\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt{x1 \cdot x1 + 1}}, -3 \cdot 1\right) + \mathsf{fma}\left(-3, 1, 3 \cdot 1\right)\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)\]

  8. Applied distribute-rgt-in0.5

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

  9. Applied associate-+l+0.5

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

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

Reproduce

herbie shell --seed 2019162 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  (+ 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))))))