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

Average Error: 3.8 → 1.5

Time: 6.3s

Precision: binary64

Math

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

↓

\[\begin{array}{l} t_1 := -0.3333333333333333 \cdot \frac{y}{z} + x\\ t_2 := \frac{-0.3333333333333333 \cdot \frac{t}{z}}{-y}\\ \mathbf{if}\;z \cdot 3 \leq -4.5958281934156114 \cdot 10^{+148}:\\ \;\;\;\;t_1 + t_2\\ \mathbf{elif}\;z \cdot 3 \leq 1.3458777268875003 \cdot 10^{-66}:\\ \;\;\;\;t_1 + \frac{0.3333333333333333 \cdot \frac{t}{y}}{z}\\ \mathbf{else}:\\ \;\;\;\;t_2 + \left(x + \frac{-0.3333333333333333 \cdot y}{z}\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
 (let* ((t_1 (+ (* -0.3333333333333333 (/ y z)) x))
        (t_2 (/ (* -0.3333333333333333 (/ t z)) (- y))))
   (if (<= (* z 3.0) -4.5958281934156114e+148)
     (+ t_1 t_2)
     (if (<= (* z 3.0) 1.3458777268875003e-66)
       (+ t_1 (/ (* 0.3333333333333333 (/ t y)) z))
       (+ t_2 (+ x (/ (* -0.3333333333333333 y) z)))))))

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 t_1 = (-0.3333333333333333 * (y / z)) + x;
	double t_2 = (-0.3333333333333333 * (t / z)) / -y;
	double tmp;
	if ((z * 3.0) <= -4.5958281934156114e+148) {
		tmp = t_1 + t_2;
	} else if ((z * 3.0) <= 1.3458777268875003e-66) {
		tmp = t_1 + ((0.3333333333333333 * (t / y)) / z);
	} else {
		tmp = t_2 + (x + ((-0.3333333333333333 * y) / z));
	}
	return tmp;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	3.8
Target	1.8
Herbie	1.5

\[\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 z 3) < -4.5958281934156114e148

   1. Initial program 0.6

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

   2. Simplified 7.8

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

   4. Applied div-inv_binary64 7.8

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

   5. Applied cancel-sign-sub-inv_binary64 7.8

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

   6. Applied distribute-rgt-in_binary64 7.8

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

   7. Applied associate-+r+_binary64 7.8

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

   8. Simplified 7.8

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

   10. Applied un-div-inv_binary64 7.8

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

   11. Applied associate-*l/_binary64 1.3

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

   12. Simplified 1.3

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

   14. Applied frac-2neg_binary64 1.3

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

   15. Simplified 1.3

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

   if -4.5958281934156114e148 < (*.f64 z 3) < 1.34587772688750032e-66

   1. Initial program 8.2

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

   2. Simplified 1.7

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

   4. Applied div-inv_binary64 1.7

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

   5. Applied cancel-sign-sub-inv_binary64 1.7

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

   6. Applied distribute-rgt-in_binary64 1.7

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

   7. Applied associate-+r+_binary64 1.7

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

   8. Simplified 1.8

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

   10. Applied associate-*r/_binary64 1.7

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

   11. Simplified 1.7

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

   if 1.34587772688750032e-66 < (*.f64 z 3)

   1. Initial program 0.5

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

   2. Simplified 5.2

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

   4. Applied div-inv_binary64 5.2

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

   5. Applied cancel-sign-sub-inv_binary64 5.2

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

   6. Applied distribute-rgt-in_binary64 5.2

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

   7. Applied associate-+r+_binary64 5.2

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

   8. Simplified 5.2

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

   10. Applied un-div-inv_binary64 5.2

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

   11. Applied associate-*l/_binary64 1.3

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

   12. Simplified 1.3

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

   14. Applied frac-2neg_binary64 1.3

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

   15. Simplified 1.3

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

   17. Applied associate-*r/_binary64 1.3

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

   18. Simplified 1.3

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

4. Final simplification 1.5

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

Reproduce

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