Average Error: 0.5 → 0.5
Time: 54.6s
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 r2335111 = x1;
        double r2335112 = 2.0;
        double r2335113 = r2335112 * r2335111;
        double r2335114 = 3.0;
        double r2335115 = r2335114 * r2335111;
        double r2335116 = r2335115 * r2335111;
        double r2335117 = x2;
        double r2335118 = r2335112 * r2335117;
        double r2335119 = r2335116 + r2335118;
        double r2335120 = r2335119 - r2335111;
        double r2335121 = r2335111 * r2335111;
        double r2335122 = 1.0;
        double r2335123 = r2335121 + r2335122;
        double r2335124 = r2335120 / r2335123;
        double r2335125 = r2335113 * r2335124;
        double r2335126 = r2335124 - r2335114;
        double r2335127 = r2335125 * r2335126;
        double r2335128 = 4.0;
        double r2335129 = r2335128 * r2335124;
        double r2335130 = 6.0;
        double r2335131 = r2335129 - r2335130;
        double r2335132 = r2335121 * r2335131;
        double r2335133 = r2335127 + r2335132;
        double r2335134 = r2335133 * r2335123;
        double r2335135 = r2335116 * r2335124;
        double r2335136 = r2335134 + r2335135;
        double r2335137 = r2335121 * r2335111;
        double r2335138 = r2335136 + r2335137;
        double r2335139 = r2335138 + r2335111;
        double r2335140 = r2335116 - r2335118;
        double r2335141 = r2335140 - r2335111;
        double r2335142 = r2335141 / r2335123;
        double r2335143 = r2335114 * r2335142;
        double r2335144 = r2335139 + r2335143;
        double r2335145 = r2335111 + r2335144;
        return r2335145;
}
↓
double f(double x1, double x2) {
        double r2335146 = x1;
        double r2335147 = r2335146 * r2335146;
        double r2335148 = r2335146 * r2335147;
        double r2335149 = 3.0;
        double r2335150 = r2335146 * r2335149;
        double r2335151 = r2335150 * r2335146;
        double r2335152 = 2.0;
        double r2335153 = x2;
        double r2335154 = r2335152 * r2335153;
        double r2335155 = r2335151 + r2335154;
        double r2335156 = r2335155 - r2335146;
        double r2335157 = 1.0;
        double r2335158 = r2335157 + r2335147;
        double r2335159 = r2335156 / r2335158;
        double r2335160 = r2335151 * r2335159;
        double r2335161 = 4.0;
        double r2335162 = r2335159 * r2335161;
        double r2335163 = 6.0;
        double r2335164 = r2335162 - r2335163;
        double r2335165 = r2335147 * r2335164;
        double r2335166 = -3.0;
        double r2335167 = fma(r2335166, r2335157, r2335149);
        double r2335168 = r2335152 * r2335146;
        double r2335169 = r2335168 * r2335159;
        double r2335170 = r2335167 * r2335169;
        double r2335171 = r2335165 + r2335170;
        double r2335172 = sqrt(r2335158);
        double r2335173 = r2335157 / r2335172;
        double r2335174 = r2335156 / r2335172;
        double r2335175 = fma(r2335173, r2335174, r2335166);
        double r2335176 = r2335169 * r2335175;
        double r2335177 = r2335171 + r2335176;
        double r2335178 = r2335158 * r2335177;
        double r2335179 = r2335160 + r2335178;
        double r2335180 = r2335148 + r2335179;
        double r2335181 = r2335180 + r2335146;
        double r2335182 = r2335151 - r2335154;
        double r2335183 = r2335182 - r2335146;
        double r2335184 = r2335183 / r2335158;
        double r2335185 = r2335184 * r2335149;
        double r2335186 = r2335181 + r2335185;
        double r2335187 = r2335146 + r2335186;
        return r2335187;
}

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