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

Average Error: 3.6 → 0.7

Time: 14.1s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;t \le -590899592270418110820309280073564815360:\\ \;\;\;\;\frac{\frac{t}{3}}{y \cdot z} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{elif}\;t \le 1.835348449183070959810035931972584701578 \cdot 10^{-76}:\\ \;\;\;\;x + \left(\frac{0}{z \cdot 3} - \left(\frac{y}{z \cdot 3} - \frac{\frac{t}{y}}{z \cdot 3}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(\frac{\frac{-y}{z}}{3} + \frac{\frac{t}{z \cdot 3}}{y}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r605231 = x;
        double r605232 = y;
        double r605233 = z;
        double r605234 = 3.0;
        double r605235 = r605233 * r605234;
        double r605236 = r605232 / r605235;
        double r605237 = r605231 - r605236;
        double r605238 = t;
        double r605239 = r605235 * r605232;
        double r605240 = r605238 / r605239;
        double r605241 = r605237 + r605240;
        return r605241;
}

↓

double f(double x, double y, double z, double t) {
        double r605242 = t;
        double r605243 = -5.908995922704181e+38;
        bool r605244 = r605242 <= r605243;
        double r605245 = 3.0;
        double r605246 = r605242 / r605245;
        double r605247 = y;
        double r605248 = z;
        double r605249 = r605247 * r605248;
        double r605250 = r605246 / r605249;
        double r605251 = x;
        double r605252 = r605248 * r605245;
        double r605253 = r605247 / r605252;
        double r605254 = r605251 - r605253;
        double r605255 = r605250 + r605254;
        double r605256 = 1.835348449183071e-76;
        bool r605257 = r605242 <= r605256;
        double r605258 = 0.0;
        double r605259 = r605258 / r605252;
        double r605260 = r605242 / r605247;
        double r605261 = r605260 / r605252;
        double r605262 = r605253 - r605261;
        double r605263 = r605259 - r605262;
        double r605264 = r605251 + r605263;
        double r605265 = -r605247;
        double r605266 = r605265 / r605248;
        double r605267 = r605266 / r605245;
        double r605268 = r605242 / r605252;
        double r605269 = r605268 / r605247;
        double r605270 = r605267 + r605269;
        double r605271 = r605251 + r605270;
        double r605272 = r605257 ? r605264 : r605271;
        double r605273 = r605244 ? r605255 : r605272;
        return r605273;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	3.6
Target	1.6
Herbie	0.7

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

Derivation

1. Split input into 3 regimes

2. if t < -5.908995922704181e+38

   1. Initial program 0.7

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

   2. Simplified 0.7

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

   4. Applied *-un-lft-identity 0.7

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

   5. Applied times-frac 3.2

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

   6. Simplified 3.1

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

   8. Applied frac-times 0.6

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

   9. Simplified 0.6

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

   10. Simplified 0.6

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

   if -5.908995922704181e+38 < t < 1.835348449183071e-76

   1. Initial program 6.0

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

   2. Simplified 6.0

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

   4. Applied *-un-lft-identity 6.0

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

   5. Applied times-frac 1.1

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

   6. Simplified 1.1

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

   8. Applied sub-neg 1.1

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

   9. Applied associate-+l+ 1.1

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

   10. Simplified 1.0

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

   12. Applied neg-sub0 1.0

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

   13. Applied div-sub 1.0

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

   14. Applied associate-+l- 1.0

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

   15. Simplified 0.2

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

   if 1.835348449183071e-76 < t

   1. Initial program 0.9

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

   2. Simplified 0.9

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

   4. Applied *-un-lft-identity 0.9

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

   5. Applied times-frac 1.8

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

   6. Simplified 1.7

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

   8. Applied sub-neg 1.7

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

   9. Applied associate-+l+ 1.7

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

   10. Simplified 1.8

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

   12. Applied associate-/r* 1.8

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

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -590899592270418110820309280073564815360:\\ \;\;\;\;\frac{\frac{t}{3}}{y \cdot z} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{elif}\;t \le 1.835348449183070959810035931972584701578 \cdot 10^{-76}:\\ \;\;\;\;x + \left(\frac{0}{z \cdot 3} - \left(\frac{y}{z \cdot 3} - \frac{\frac{t}{y}}{z \cdot 3}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(\frac{\frac{-y}{z}}{3} + \frac{\frac{t}{z \cdot 3}}{y}\right)\\ \end{array}\]

Reproduce

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

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

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