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

Average Error: 8.4 → 3.9

Time: 6.6s

Precision: binary64

\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x1 \leq 0.004257901367187499:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{4}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{4}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]

FPCore

(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))

↓

(FPCore (x0 x1)
 :precision binary64
 (if (<= x1 0.004257901367187499)
   (/
    (*
     x0
     (/
      (/
       (-
        (pow (/ (pow x0 3.0) (pow (- 1.0 x1) 6.0)) 3.0)
        (pow (pow x0 3.0) 3.0))
       (+
        (/
         (pow x0 6.0)
         (*
          (pow (+ (sqrt 1.0) (sqrt x1)) 12.0)
          (pow (- (sqrt 1.0) (sqrt x1)) 12.0)))
        (+ (pow x0 6.0) (pow (/ x0 (- 1.0 x1)) 6.0))))
      (+
       (/ (* x0 x0) (pow (- 1.0 x1) 4.0))
       (* x0 (+ x0 (/ x0 (* (- 1.0 x1) (- 1.0 x1))))))))
    (+ x0 (/ x0 (- 1.0 x1))))
   (/
    (*
     x0
     (/
      (-
       (/
        (pow x0 3.0)
        (*
         (pow (+ (sqrt 1.0) (sqrt x1)) 6.0)
         (pow (- (sqrt 1.0) (sqrt x1)) 6.0)))
       (pow x0 3.0))
      (+
       (/ (* x0 x0) (pow (- 1.0 x1) 4.0))
       (* x0 (+ x0 (/ x0 (* (- 1.0 x1) (- 1.0 x1))))))))
    (+ x0 (/ x0 (- 1.0 x1))))))

C

double code(double x0, double x1) {
	return ((double) ((x0 / ((double) (1.0 - x1))) - x0));
}

↓

double code(double x0, double x1) {
	double tmp;
	if ((x1 <= 0.004257901367187499)) {
		tmp = (((double) (x0 * ((((double) (((double) pow((((double) pow(x0, 3.0)) / ((double) pow(((double) (1.0 - x1)), 6.0))), 3.0)) - ((double) pow(((double) pow(x0, 3.0)), 3.0)))) / ((double) ((((double) pow(x0, 6.0)) / ((double) (((double) pow(((double) (((double) sqrt(1.0)) + ((double) sqrt(x1)))), 12.0)) * ((double) pow(((double) (((double) sqrt(1.0)) - ((double) sqrt(x1)))), 12.0))))) + ((double) (((double) pow(x0, 6.0)) + ((double) pow((x0 / ((double) (1.0 - x1))), 6.0))))))) / ((double) ((((double) (x0 * x0)) / ((double) pow(((double) (1.0 - x1)), 4.0))) + ((double) (x0 * ((double) (x0 + (x0 / ((double) (((double) (1.0 - x1)) * ((double) (1.0 - x1)))))))))))))) / ((double) (x0 + (x0 / ((double) (1.0 - x1))))));
	} else {
		tmp = (((double) (x0 * (((double) ((((double) pow(x0, 3.0)) / ((double) (((double) pow(((double) (((double) sqrt(1.0)) + ((double) sqrt(x1)))), 6.0)) * ((double) pow(((double) (((double) sqrt(1.0)) - ((double) sqrt(x1)))), 6.0))))) - ((double) pow(x0, 3.0)))) / ((double) ((((double) (x0 * x0)) / ((double) pow(((double) (1.0 - x1)), 4.0))) + ((double) (x0 * ((double) (x0 + (x0 / ((double) (((double) (1.0 - x1)) * ((double) (1.0 - x1)))))))))))))) / ((double) (x0 + (x0 / ((double) (1.0 - x1))))));
	}
	return tmp;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.4
Target	0.5
Herbie	3.9

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

Derivation

1. Split input into 2 regimes

2. if x1 < 0.0042579013671874989

   1. Initial program 11.3

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

   3. Applied flip--_binary64 11.4

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

   4. Simplified 9.1

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

   5. Simplified 9.1

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

   7. Applied flip3--_binary64 7.8

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

   8. Simplified 7.8

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

   9. Simplified 7.8

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

   11. Applied flip3--_binary64 6.3

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

   12. Simplified 6.3

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

   14. Applied add-sqr-sqrt_binary64 6.3

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

   15. Applied add-sqr-sqrt_binary64 6.3

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

   16. Applied difference-of-squares_binary64 6.2

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

   17. Applied unpow-prod-down_binary64 6.2

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

   if 0.0042579013671874989 < x1

   1. Initial program 5.5

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

   3. Applied flip--_binary64 4.0

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

   4. Simplified 4.7

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

   5. Simplified 4.7

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

   7. Applied flip3--_binary64 4.4

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

   8. Simplified 4.4

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

   9. Simplified 4.4

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

   11. Applied add-sqr-sqrt_binary64 4.4

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

   12. Applied add-sqr-sqrt_binary64 4.4

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

   13. Applied difference-of-squares_binary64 4.4

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

   14. Applied unpow-prod-down_binary64 1.6

       \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}}} - {x0}^{3}}{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{4}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 3.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;x1 \leq 0.004257901367187499:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{4}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{4}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020210 
(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.0 x1))

  (- (/ x0 (- 1.0 x1)) x0))