Average Error: 8.4 → 5.7
Time: 3.2s
Precision: 64
\[x0 = 1.855 \land x1 = 2.09000000000000012 \cdot 10^{-4} \lor x0 = 2.98499999999999988 \land x1 = 0.018599999999999998\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{\frac{\frac{{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3}\right)}^{3} - {\left({\left(x0 \cdot x0\right)}^{3}\right)}^{3}}{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{6} + {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3}\right) + {x0}^{12}}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\]
\frac{x0}{1 - x1} - x0
↓
\frac{\frac{\frac{{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3}\right)}^{3} - {\left({\left(x0 \cdot x0\right)}^{3}\right)}^{3}}{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{6} + {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3}\right) + {x0}^{12}}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}
double f(double x0, double x1) {
        double r143130 = x0;
        double r143131 = 1.0;
        double r143132 = x1;
        double r143133 = r143131 - r143132;
        double r143134 = r143130 / r143133;
        double r143135 = r143134 - r143130;
        return r143135;
}
↓
double f(double x0, double x1) {
        double r143136 = x0;
        double r143137 = 1.0;
        double r143138 = 1.0;
        double r143139 = x1;
        double r143140 = r143138 - r143139;
        double r143141 = r143137 / r143140;
        double r143142 = r143136 * r143141;
        double r143143 = r143136 / r143140;
        double r143144 = r143142 * r143143;
        double r143145 = 3.0;
        double r143146 = pow(r143144, r143145);
        double r143147 = pow(r143146, r143145);
        double r143148 = r143136 * r143136;
        double r143149 = pow(r143148, r143145);
        double r143150 = pow(r143149, r143145);
        double r143151 = r143147 - r143150;
        double r143152 = 6.0;
        double r143153 = pow(r143144, r143152);
        double r143154 = r143146 * r143149;
        double r143155 = r143153 + r143154;
        double r143156 = 12.0;
        double r143157 = pow(r143136, r143156);
        double r143158 = r143155 + r143157;
        double r143159 = r143151 / r143158;
        double r143160 = pow(r143143, r143145);
        double r143161 = pow(r143136, r143145);
        double r143162 = r143161 / r143140;
        double r143163 = r143160 + r143162;
        double r143164 = r143143 * r143163;
        double r143165 = 4.0;
        double r143166 = pow(r143136, r143165);
        double r143167 = r143164 + r143166;
        double r143168 = r143159 / r143167;
        double r143169 = r143143 + r143136;
        double r143170 = r143168 / r143169;
        return r143170;
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original8.4
Target0.5
Herbie5.7
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Initial program 8.4

    \[\frac{x0}{1 - x1} - x0\]
  2. Using strategy rm

  3. Applied flip--7.7

    \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]
  4. Using strategy rm

  5. Applied div-inv6.6

    \[\leadsto \frac{\color{blue}{\left(x0 \cdot \frac{1}{1 - x1}\right)} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}\]
  6. Using strategy rm

  7. Applied flip3--6.0

    \[\leadsto \frac{\color{blue}{\frac{{\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} - {\left(x0 \cdot x0\right)}^{3}}{\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right) \cdot \left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right) + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right) + \left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right) \cdot \left(x0 \cdot x0\right)\right)}}}{\frac{x0}{1 - x1} + x0}\]

  8. Simplified6.0

    \[\leadsto \frac{\frac{{\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} - {\left(x0 \cdot x0\right)}^{3}}{\color{blue}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}}{\frac{x0}{1 - x1} + x0}\]
  9. Using strategy rm

  10. Applied flip3--5.6

    \[\leadsto \frac{\frac{\color{blue}{\frac{{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3}\right)}^{3} - {\left({\left(x0 \cdot x0\right)}^{3}\right)}^{3}}{{\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} + \left({\left(x0 \cdot x0\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3} + {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3}\right)}}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\]

  11. Simplified5.7

    \[\leadsto \frac{\frac{\frac{{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3}\right)}^{3} - {\left({\left(x0 \cdot x0\right)}^{3}\right)}^{3}}{\color{blue}{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{6} + {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3}\right) + {x0}^{12}}}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\]

  12. Final simplification5.7

    \[\leadsto \frac{\frac{\frac{{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3}\right)}^{3} - {\left({\left(x0 \cdot x0\right)}^{3}\right)}^{3}}{\left({\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{6} + {\left(\left(x0 \cdot \frac{1}{1 - x1}\right) \cdot \frac{x0}{1 - x1}\right)}^{3} \cdot {\left(x0 \cdot x0\right)}^{3}\right) + {x0}^{12}}}{\frac{x0}{1 - x1} \cdot \left({\left(\frac{x0}{1 - x1}\right)}^{3} + \frac{{x0}^{3}}{1 - x1}\right) + {x0}^{4}}}{\frac{x0}{1 - x1} + x0}\]

Reproduce

herbie shell --seed 2020065 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1 x1))

  (- (/ x0 (- 1 x1)) x0))