Average Error: 0.5 → 0.3
Time: 3.8m
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 + (3 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left(x1 + (x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(x1 \cdot \left(x1 \cdot 3\right)\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(x1 \cdot \left(x1 \cdot 3\right)\right) + \left((\left((\left(\frac{(x2 \cdot 2 + \left(x1 \cdot \left(x1 \cdot 3\right)\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\frac{\left(\left(2 \cdot x1\right) \cdot \left((x2 \cdot 2 + \left(x1 \cdot \left(x1 \cdot 3\right)\right))_* - x1\right)\right) \cdot (\left(\frac{1}{\sqrt{(x1 \cdot x1 + 1)_*}}\right) \cdot \left(\frac{(x2 \cdot 2 + \left(x1 \cdot \left(x1 \cdot 3\right)\right))_* - x1}{\sqrt{(x1 \cdot x1 + 1)_*}}\right) + -3)_*}{(x1 \cdot x1 + 1)_*}\right))_* \cdot (x1 \cdot x1 + 1)_*\right))_*\right))_*\right))_*\]
double f(double x1, double x2) {
        double r21434086 = x1;
        double r21434087 = 2.0;
        double r21434088 = r21434087 * r21434086;
        double r21434089 = 3.0;
        double r21434090 = r21434089 * r21434086;
        double r21434091 = r21434090 * r21434086;
        double r21434092 = x2;
        double r21434093 = r21434087 * r21434092;
        double r21434094 = r21434091 + r21434093;
        double r21434095 = r21434094 - r21434086;
        double r21434096 = r21434086 * r21434086;
        double r21434097 = 1.0;
        double r21434098 = r21434096 + r21434097;
        double r21434099 = r21434095 / r21434098;
        double r21434100 = r21434088 * r21434099;
        double r21434101 = r21434099 - r21434089;
        double r21434102 = r21434100 * r21434101;
        double r21434103 = 4.0;
        double r21434104 = r21434103 * r21434099;
        double r21434105 = 6.0;
        double r21434106 = r21434104 - r21434105;
        double r21434107 = r21434096 * r21434106;
        double r21434108 = r21434102 + r21434107;
        double r21434109 = r21434108 * r21434098;
        double r21434110 = r21434091 * r21434099;
        double r21434111 = r21434109 + r21434110;
        double r21434112 = r21434096 * r21434086;
        double r21434113 = r21434111 + r21434112;
        double r21434114 = r21434113 + r21434086;
        double r21434115 = r21434091 - r21434093;
        double r21434116 = r21434115 - r21434086;
        double r21434117 = r21434116 / r21434098;
        double r21434118 = r21434089 * r21434117;
        double r21434119 = r21434114 + r21434118;
        double r21434120 = r21434086 + r21434119;
        return r21434120;
}
↓
double f(double x1, double x2) {
        double r21434121 = x1;
        double r21434122 = 3.0;
        double r21434123 = r21434121 * r21434122;
        double r21434124 = r21434121 * r21434123;
        double r21434125 = 2.0;
        double r21434126 = x2;
        double r21434127 = fma(r21434125, r21434126, r21434121);
        double r21434128 = r21434124 - r21434127;
        double r21434129 = 1.0;
        double r21434130 = fma(r21434121, r21434121, r21434129);
        double r21434131 = r21434128 / r21434130;
        double r21434132 = r21434121 * r21434121;
        double r21434133 = fma(r21434126, r21434125, r21434124);
        double r21434134 = r21434133 - r21434121;
        double r21434135 = r21434134 / r21434130;
        double r21434136 = 4.0;
        double r21434137 = -6.0;
        double r21434138 = fma(r21434135, r21434136, r21434137);
        double r21434139 = r21434125 * r21434121;
        double r21434140 = r21434139 * r21434134;
        double r21434141 = sqrt(r21434130);
        double r21434142 = r21434129 / r21434141;
        double r21434143 = r21434134 / r21434141;
        double r21434144 = -3.0;
        double r21434145 = fma(r21434142, r21434143, r21434144);
        double r21434146 = r21434140 * r21434145;
        double r21434147 = r21434146 / r21434130;
        double r21434148 = fma(r21434138, r21434132, r21434147);
        double r21434149 = r21434148 * r21434130;
        double r21434150 = fma(r21434135, r21434124, r21434149);
        double r21434151 = fma(r21434121, r21434132, r21434150);
        double r21434152 = r21434121 + r21434151;
        double r21434153 = fma(r21434122, r21434131, r21434152);
        double r21434154 = r21434121 + r21434153;
        return r21434154;
}


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

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. Simplified0.3

    \[\leadsto \color{blue}{x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*} - 3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right)\right))_*\right))_*\right))_* + x1\right))_*}\]
  3. Using strategy rm

  4. Applied associate-*r/0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*} - 3\right) \cdot \color{blue}{\frac{\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)}{(x1 \cdot x1 + 1)_*}}\right))_*\right))_*\right))_* + x1\right))_*\]

  5. Applied associate-*r/0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \color{blue}{\left(\frac{\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*} - 3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)\right)}{(x1 \cdot x1 + 1)_*}\right)})_*\right))_*\right))_* + x1\right))_*\]
  6. Using strategy rm

  7. Applied add-sqr-sqrt0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\frac{\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{\color{blue}{\sqrt{(x1 \cdot x1 + 1)_*} \cdot \sqrt{(x1 \cdot x1 + 1)_*}}} - 3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)\right)}{(x1 \cdot x1 + 1)_*}\right))_*\right))_*\right))_* + x1\right))_*\]

  8. Applied *-un-lft-identity0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\frac{\left(\frac{\color{blue}{1 \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)}}{\sqrt{(x1 \cdot x1 + 1)_*} \cdot \sqrt{(x1 \cdot x1 + 1)_*}} - 3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)\right)}{(x1 \cdot x1 + 1)_*}\right))_*\right))_*\right))_* + x1\right))_*\]

  9. Applied times-frac0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\frac{\left(\color{blue}{\frac{1}{\sqrt{(x1 \cdot x1 + 1)_*}} \cdot \frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{\sqrt{(x1 \cdot x1 + 1)_*}}} - 3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)\right)}{(x1 \cdot x1 + 1)_*}\right))_*\right))_*\right))_* + x1\right))_*\]

  10. Applied fma-neg0.3

    \[\leadsto x1 + (3 \cdot \left(\frac{\left(3 \cdot x1\right) \cdot x1 - (2 \cdot x2 + x1)_*}{(x1 \cdot x1 + 1)_*}\right) + \left((x1 \cdot \left(x1 \cdot x1\right) + \left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot \left(\left(3 \cdot x1\right) \cdot x1\right) + \left((x1 \cdot x1 + 1)_* \cdot (\left((\left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{(x1 \cdot x1 + 1)_*}\right) \cdot 4 + -6)_*\right) \cdot \left(x1 \cdot x1\right) + \left(\frac{\color{blue}{(\left(\frac{1}{\sqrt{(x1 \cdot x1 + 1)_*}}\right) \cdot \left(\frac{(x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1}{\sqrt{(x1 \cdot x1 + 1)_*}}\right) + \left(-3\right))_*} \cdot \left(\left(x1 \cdot 2\right) \cdot \left((x2 \cdot 2 + \left(\left(3 \cdot x1\right) \cdot x1\right))_* - x1\right)\right)}{(x1 \cdot x1 + 1)_*}\right))_*\right))_*\right))_* + x1\right))_*\]

  11. Final simplification0.3

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

Reproduce

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