Average Error: 0.5 → 0.5
Time: 56.7s
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(\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(\left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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)\]
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(\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(\left(4 \cdot \frac{\mathsf{fma}\left(3 \cdot x1, x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}\right) \cdot \left(x1 \cdot x1\right) + \left(-6\right) \cdot \left(x1 \cdot x1\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)
double f(double x1, double x2) {
        double r99146 = x1;
        double r99147 = 2.0;
        double r99148 = r99147 * r99146;
        double r99149 = 3.0;
        double r99150 = r99149 * r99146;
        double r99151 = r99150 * r99146;
        double r99152 = x2;
        double r99153 = r99147 * r99152;
        double r99154 = r99151 + r99153;
        double r99155 = r99154 - r99146;
        double r99156 = r99146 * r99146;
        double r99157 = 1.0;
        double r99158 = r99156 + r99157;
        double r99159 = r99155 / r99158;
        double r99160 = r99148 * r99159;
        double r99161 = r99159 - r99149;
        double r99162 = r99160 * r99161;
        double r99163 = 4.0;
        double r99164 = r99163 * r99159;
        double r99165 = 6.0;
        double r99166 = r99164 - r99165;
        double r99167 = r99156 * r99166;
        double r99168 = r99162 + r99167;
        double r99169 = r99168 * r99158;
        double r99170 = r99151 * r99159;
        double r99171 = r99169 + r99170;
        double r99172 = r99156 * r99146;
        double r99173 = r99171 + r99172;
        double r99174 = r99173 + r99146;
        double r99175 = r99151 - r99153;
        double r99176 = r99175 - r99146;
        double r99177 = r99176 / r99158;
        double r99178 = r99149 * r99177;
        double r99179 = r99174 + r99178;
        double r99180 = r99146 + r99179;
        return r99180;
}
↓
double f(double x1, double x2) {
        double r99181 = x1;
        double r99182 = 2.0;
        double r99183 = r99182 * r99181;
        double r99184 = 3.0;
        double r99185 = r99184 * r99181;
        double r99186 = r99185 * r99181;
        double r99187 = x2;
        double r99188 = r99182 * r99187;
        double r99189 = r99186 + r99188;
        double r99190 = r99189 - r99181;
        double r99191 = r99181 * r99181;
        double r99192 = 1.0;
        double r99193 = r99191 + r99192;
        double r99194 = r99190 / r99193;
        double r99195 = r99183 * r99194;
        double r99196 = r99194 - r99184;
        double r99197 = r99195 * r99196;
        double r99198 = 4.0;
        double r99199 = fma(r99185, r99181, r99188);
        double r99200 = r99199 - r99181;
        double r99201 = fma(r99181, r99181, r99192);
        double r99202 = r99200 / r99201;
        double r99203 = r99198 * r99202;
        double r99204 = r99203 * r99191;
        double r99205 = 6.0;
        double r99206 = -r99205;
        double r99207 = r99206 * r99191;
        double r99208 = r99204 + r99207;
        double r99209 = r99197 + r99208;
        double r99210 = r99209 * r99193;
        double r99211 = r99186 * r99194;
        double r99212 = r99210 + r99211;
        double r99213 = r99191 * r99181;
        double r99214 = r99212 + r99213;
        double r99215 = r99214 + r99181;
        double r99216 = r99186 - r99188;
        double r99217 = r99216 - r99181;
        double r99218 = r99217 / r99193;
        double r99219 = r99184 * r99218;
        double r99220 = r99215 + r99219;
        double r99221 = r99181 + r99220;
        return r99221;
}

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 sub-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 \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 \color{blue}{\left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} + \left(-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)\]

  4. Applied distribute-lft-in0.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} - 3\right) + \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(-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)\]

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

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

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

Reproduce

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