Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, H

Average Error: 3.4 → 0.8

Time: 6.4s

Precision: binary64

Math

\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)} \leq -3.152584455246644 \cdot 10^{+305}:\\ \;\;\;\;x + -0.3333333333333333 \cdot \frac{y - \frac{t}{y}}{z}\\ \mathbf{elif}\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)} \leq 1.7119330914986298 \cdot 10^{+305}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{0.3333333333333333}{\frac{z}{t} \cdot \left(y + \frac{{y}^{3}}{t}\right)}\\ \end{array}\]

FPCore

(FPCore (x y z t)
 :precision binary64
 (+ (- x (/ y (* z 3.0))) (/ t (* (* z 3.0) y))))

↓

(FPCore (x y z t)
 :precision binary64
 (if (<=
      (+ (- x (/ y (* z 3.0))) (/ t (* y (* z 3.0))))
      -3.152584455246644e+305)
   (+ x (* -0.3333333333333333 (/ (- y (/ t y)) z)))
   (if (<=
        (+ (- x (/ y (* z 3.0))) (/ t (* y (* z 3.0))))
        1.7119330914986298e+305)
     (+ (- x (/ y (* z 3.0))) (/ t (* y (* z 3.0))))
     (+ x (/ 0.3333333333333333 (* (/ z t) (+ y (/ (pow y 3.0) t))))))))

C

double code(double x, double y, double z, double t) {
	return (x - (y / (z * 3.0))) + (t / ((z * 3.0) * y));
}

↓

double code(double x, double y, double z, double t) {
	double tmp;
	if (((x - (y / (z * 3.0))) + (t / (y * (z * 3.0)))) <= -3.152584455246644e+305) {
		tmp = x + (-0.3333333333333333 * ((y - (t / y)) / z));
	} else if (((x - (y / (z * 3.0))) + (t / (y * (z * 3.0)))) <= 1.7119330914986298e+305) {
		tmp = (x - (y / (z * 3.0))) + (t / (y * (z * 3.0)));
	} else {
		tmp = x + (0.3333333333333333 / ((z / t) * (y + (pow(y, 3.0) / t))));
	}
	return tmp;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	3.4
Target	1.6
Herbie	0.8

\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]

Derivation

1. Split input into 3 regimes

2. if (+.f64 (-.f64 x (/.f64 y (*.f64 z 3))) (/.f64 t (*.f64 (*.f64 z 3) y))) < -3.15258445524664416e305

   1. Initial program 55.0

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

   2. Simplified 1.3

      \[\leadsto \color{blue}{x + \frac{-0.3333333333333333}{z} \cdot \left(y - \frac{t}{y}\right)}\]

   3. Taylor expanded around 0 2.2

      \[\leadsto x + \color{blue}{-0.3333333333333333 \cdot \frac{y - \frac{t}{y}}{z}}\]

   if -3.15258445524664416e305 < (+.f64 (-.f64 x (/.f64 y (*.f64 z 3))) (/.f64 t (*.f64 (*.f64 z 3) y))) < 1.71193309149862979e305

   1. Initial program 0.5

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

   if 1.71193309149862979e305 < (+.f64 (-.f64 x (/.f64 y (*.f64 z 3))) (/.f64 t (*.f64 (*.f64 z 3) y)))

   1. Initial program 52.1

      \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

   2. Simplified 1.2

      \[\leadsto \color{blue}{x + \frac{-0.3333333333333333}{z} \cdot \left(y - \frac{t}{y}\right)}\]
   3. Using strategy rm

   4. Applied pow1_binary64 1.2

      \[\leadsto x + \frac{-0.3333333333333333}{z} \cdot \color{blue}{{\left(y - \frac{t}{y}\right)}^{1}}\]

   5. Applied pow1_binary64 1.2

      \[\leadsto x + \color{blue}{{\left(\frac{-0.3333333333333333}{z}\right)}^{1}} \cdot {\left(y - \frac{t}{y}\right)}^{1}\]

   6. Applied pow-prod-down_binary64 1.2

      \[\leadsto x + \color{blue}{{\left(\frac{-0.3333333333333333}{z} \cdot \left(y - \frac{t}{y}\right)\right)}^{1}}\]

   7. Simplified 1.6

      \[\leadsto x + {\color{blue}{\left(-0.3333333333333333 \cdot \frac{y - \frac{t}{y}}{z}\right)}}^{1}\]
   8. Using strategy rm

   9. Applied div-inv_binary64 1.6

      \[\leadsto x + {\left(-0.3333333333333333 \cdot \color{blue}{\left(\left(y - \frac{t}{y}\right) \cdot \frac{1}{z}\right)}\right)}^{1}\]

   10. Applied associate-*r*_binary64 1.2

       \[\leadsto x + {\color{blue}{\left(\left(-0.3333333333333333 \cdot \left(y - \frac{t}{y}\right)\right) \cdot \frac{1}{z}\right)}}^{1}\]

   11. Simplified 1.2

       \[\leadsto x + {\left(\color{blue}{\left(\left(y - \frac{t}{y}\right) \cdot -0.3333333333333333\right)} \cdot \frac{1}{z}\right)}^{1}\]

   12. Taylor expanded around 0 1.6

       \[\leadsto x + {\color{blue}{\left(-0.3333333333333333 \cdot \frac{y - \frac{t}{y}}{z}\right)}}^{1}\]

   13. Simplified 1.2

       \[\leadsto x + {\color{blue}{\left(\frac{0.3333333333333333}{\frac{z}{\frac{t}{y} - y}}\right)}}^{1}\]

   14. Taylor expanded around inf 58.8

       \[\leadsto x + {\left(\frac{0.3333333333333333}{\color{blue}{\frac{z \cdot y}{t} + \frac{z \cdot {y}^{3}}{{t}^{2}}}}\right)}^{1}\]

   15. Simplified 10.0

       \[\leadsto x + {\left(\frac{0.3333333333333333}{\color{blue}{\frac{z}{t} \cdot \left(y + \frac{{y}^{3}}{t}\right)}}\right)}^{1}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.8

   \[\leadsto \begin{array}{l} \mathbf{if}\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)} \leq -3.152584455246644 \cdot 10^{+305}:\\ \;\;\;\;x + -0.3333333333333333 \cdot \frac{y - \frac{t}{y}}{z}\\ \mathbf{elif}\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)} \leq 1.7119330914986298 \cdot 10^{+305}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{y \cdot \left(z \cdot 3\right)}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{0.3333333333333333}{\frac{z}{t} \cdot \left(y + \frac{{y}^{3}}{t}\right)}\\ \end{array}\]

Alternatives

Reproduce

herbie shell --seed 2021118 
(FPCore (x y z t)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, H"
  :precision binary64

  :herbie-target
  (+ (- x (/ y (* z 3.0))) (/ (/ t (* z 3.0)) y))

  (+ (- x (/ y (* z 3.0))) (/ t (* (* z 3.0) y))))