Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.5

Time: 36.6s

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

↓

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

C

double f(double x1, double x2) {
        double r848649 = x1;
        double r848650 = 2.0;
        double r848651 = r848650 * r848649;
        double r848652 = 3.0;
        double r848653 = r848652 * r848649;
        double r848654 = r848653 * r848649;
        double r848655 = x2;
        double r848656 = r848650 * r848655;
        double r848657 = r848654 + r848656;
        double r848658 = r848657 - r848649;
        double r848659 = r848649 * r848649;
        double r848660 = 1.0;
        double r848661 = r848659 + r848660;
        double r848662 = r848658 / r848661;
        double r848663 = r848651 * r848662;
        double r848664 = r848662 - r848652;
        double r848665 = r848663 * r848664;
        double r848666 = 4.0;
        double r848667 = r848666 * r848662;
        double r848668 = 6.0;
        double r848669 = r848667 - r848668;
        double r848670 = r848659 * r848669;
        double r848671 = r848665 + r848670;
        double r848672 = r848671 * r848661;
        double r848673 = r848654 * r848662;
        double r848674 = r848672 + r848673;
        double r848675 = r848659 * r848649;
        double r848676 = r848674 + r848675;
        double r848677 = r848676 + r848649;
        double r848678 = r848654 - r848656;
        double r848679 = r848678 - r848649;
        double r848680 = r848679 / r848661;
        double r848681 = r848652 * r848680;
        double r848682 = r848677 + r848681;
        double r848683 = r848649 + r848682;
        return r848683;
}

↓

double f(double x1, double x2) {
        double r848684 = x1;
        double r848685 = 3.0;
        double r848686 = r848685 * r848684;
        double r848687 = r848686 * r848684;
        double r848688 = x2;
        double r848689 = 2.0;
        double r848690 = r848688 * r848689;
        double r848691 = r848687 - r848690;
        double r848692 = r848691 - r848684;
        double r848693 = 1.0;
        double r848694 = r848684 * r848684;
        double r848695 = r848693 + r848694;
        double r848696 = r848692 / r848695;
        double r848697 = r848685 * r848696;
        double r848698 = r848684 * r848694;
        double r848699 = r848687 + r848690;
        double r848700 = r848699 - r848684;
        double r848701 = r848700 / r848695;
        double r848702 = 4.0;
        double r848703 = r848701 * r848702;
        double r848704 = r848703 * r848694;
        double r848705 = -6.0;
        double r848706 = r848684 * r848705;
        double r848707 = r848706 * r848684;
        double r848708 = r848704 + r848707;
        double r848709 = r848684 * r848689;
        double r848710 = r848709 * r848701;
        double r848711 = r848693 / r848695;
        double r848712 = -3.0;
        double r848713 = fma(r848700, r848711, r848712);
        double r848714 = r848710 * r848713;
        double r848715 = r848708 + r848714;
        double r848716 = r848695 * r848715;
        double r848717 = r848687 * r848701;
        double r848718 = r848716 + r848717;
        double r848719 = r848698 + r848718;
        double r848720 = r848684 + r848719;
        double r848721 = r848697 + r848720;
        double r848722 = r848684 + r848721;
        return r848722;
}

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 div-inv 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(\color{blue}{\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right) \cdot \frac{1}{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 fma-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 \color{blue}{\mathsf{fma}\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1, \frac{1}{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. Simplified 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 \mathsf{fma}\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1, \frac{1}{x1 \cdot x1 + 1}, \color{blue}{-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. Using strategy rm

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

9. 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 \mathsf{fma}\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1, \frac{1}{x1 \cdot x1 + 1}, -3\right) + \color{blue}{\left(\left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(-\sqrt{6}, \sqrt{6}, \sqrt{6} \cdot \sqrt{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. Simplified 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 \mathsf{fma}\left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1, \frac{1}{x1 \cdot x1 + 1}, -3\right) + \left(\left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \color{blue}{0}\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. Using strategy rm

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

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

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

15. Final simplification 0.5

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

Reproduce

herbie shell --seed 2019153 +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))))))