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

Average Error: 7.9 → 6.3

Time: 13.3s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 1.855
  2. x1 = 0.0186

\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]

Math

\[\frac{x0}{1 - x1} - x0\]

↓

\[\frac{\frac{\frac{\left({\left(\sqrt{{\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3}}\right)}^{3} + {\left({x0}^{3}\right)}^{\frac{3}{2}}\right) \cdot \left({\left(\sqrt{{\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3}}\right)}^{3} - {\left({x0}^{3}\right)}^{\frac{3}{2}}\right)}{{\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{6} + {x0}^{3} \cdot \left({x0}^{3} + {\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3}\right)}}{\frac{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{3}}}{1 - x1} + x0 \cdot \left(\frac{\frac{x0}{1 - x1}}{1 - x1} + x0\right)} \cdot x0}{\frac{x0}{1 - x1} + x0}\]

C

double f(double x0, double x1) {
        double r309198 = x0;
        double r309199 = 1.0;
        double r309200 = x1;
        double r309201 = r309199 - r309200;
        double r309202 = r309198 / r309201;
        double r309203 = r309202 - r309198;
        return r309203;
}

↓

double f(double x0, double x1) {
        double r309204 = x0;
        double r309205 = 1.0;
        double r309206 = x1;
        double r309207 = r309205 - r309206;
        double r309208 = r309204 / r309207;
        double r309209 = r309208 / r309207;
        double r309210 = 3.0;
        double r309211 = pow(r309209, r309210);
        double r309212 = sqrt(r309211);
        double r309213 = pow(r309212, r309210);
        double r309214 = pow(r309204, r309210);
        double r309215 = 1.5;
        double r309216 = pow(r309214, r309215);
        double r309217 = r309213 + r309216;
        double r309218 = r309213 - r309216;
        double r309219 = r309217 * r309218;
        double r309220 = 6.0;
        double r309221 = pow(r309209, r309220);
        double r309222 = r309214 + r309211;
        double r309223 = r309214 * r309222;
        double r309224 = r309221 + r309223;
        double r309225 = r309219 / r309224;
        double r309226 = r309204 * r309204;
        double r309227 = pow(r309207, r309210);
        double r309228 = r309226 / r309227;
        double r309229 = r309228 / r309207;
        double r309230 = r309209 + r309204;
        double r309231 = r309204 * r309230;
        double r309232 = r309229 + r309231;
        double r309233 = r309225 / r309232;
        double r309234 = r309233 * r309204;
        double r309235 = r309208 + r309204;
        double r309236 = r309234 / r309235;
        return r309236;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.9
Target	0.3
Herbie	6.3

\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

1. Initial program 7.9

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

3. Applied flip-- 7.3

   \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

4. Simplified 6.9

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

6. Applied flip3-- 6.7

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

7. Simplified 6.6

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

9. Applied flip3-- 6.3

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

10. Simplified 6.3

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

12. Applied sqr-pow 6.3

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

13. Applied add-sqr-sqrt 6.6

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

14. Applied unpow-prod-down 6.2

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

15. Applied difference-of-squares 6.3

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

16. Final simplification 6.3

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

Reproduce

herbie shell --seed 2019323 
(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))