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

Average Error: 3.5 → 1.1

Time: 23.3s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \cdot 3.0 \le -7.705332731478375 \cdot 10^{+43}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{3.0}}{z \cdot y}\\ \mathbf{elif}\;z \cdot 3.0 \le 1.640266769777498 \cdot 10^{+158}:\\ \;\;\;\;\frac{\frac{\frac{t}{y}}{3.0}}{z} + \left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{1}{y} \cdot \left(\frac{1}{z} \cdot \frac{t}{3.0}\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r23628035 = x;
        double r23628036 = y;
        double r23628037 = z;
        double r23628038 = 3.0;
        double r23628039 = r23628037 * r23628038;
        double r23628040 = r23628036 / r23628039;
        double r23628041 = r23628035 - r23628040;
        double r23628042 = t;
        double r23628043 = r23628039 * r23628036;
        double r23628044 = r23628042 / r23628043;
        double r23628045 = r23628041 + r23628044;
        return r23628045;
}

↓

double f(double x, double y, double z, double t) {
        double r23628046 = z;
        double r23628047 = 3.0;
        double r23628048 = r23628046 * r23628047;
        double r23628049 = -7.705332731478375e+43;
        bool r23628050 = r23628048 <= r23628049;
        double r23628051 = x;
        double r23628052 = y;
        double r23628053 = r23628052 / r23628047;
        double r23628054 = 1.0;
        double r23628055 = r23628054 / r23628046;
        double r23628056 = r23628053 * r23628055;
        double r23628057 = r23628051 - r23628056;
        double r23628058 = t;
        double r23628059 = r23628058 / r23628047;
        double r23628060 = r23628046 * r23628052;
        double r23628061 = r23628059 / r23628060;
        double r23628062 = r23628057 + r23628061;
        double r23628063 = 1.640266769777498e+158;
        bool r23628064 = r23628048 <= r23628063;
        double r23628065 = r23628058 / r23628052;
        double r23628066 = r23628065 / r23628047;
        double r23628067 = r23628066 / r23628046;
        double r23628068 = r23628067 + r23628057;
        double r23628069 = r23628054 / r23628052;
        double r23628070 = r23628055 * r23628059;
        double r23628071 = r23628069 * r23628070;
        double r23628072 = r23628057 + r23628071;
        double r23628073 = r23628064 ? r23628068 : r23628072;
        double r23628074 = r23628050 ? r23628062 : r23628073;
        return r23628074;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	3.5
Target	1.9
Herbie	1.1

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

Derivation

1. Split input into 3 regimes

2. if (* z 3.0) < -7.705332731478375e+43

   1. Initial program 0.4

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 0.7

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

   4. Applied times-frac 1.8

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

   6. Applied div-inv 1.9

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

   7. Applied associate-*r* 1.8

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

   8. Simplified 1.5

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

   10. Applied *-un-lft-identity 1.5

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

   11. Applied times-frac 1.5

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

   13. Applied frac-times 0.4

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

   14. Simplified 0.4

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

   if -7.705332731478375e+43 < (* z 3.0) < 1.640266769777498e+158

   1. Initial program 6.0

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 6.3

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

   4. Applied times-frac 1.0

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

   6. Applied div-inv 1.0

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

   7. Applied associate-*r* 2.6

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

   8. Simplified 2.3

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

   10. Applied *-un-lft-identity 2.3

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

   11. Applied times-frac 2.3

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

   13. Applied associate-*l/ 1.3

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

   14. Simplified 1.3

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

   if 1.640266769777498e+158 < (* z 3.0)

   1. Initial program 0.7

      \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
   2. Using strategy rm

   3. Applied add-cube-cbrt 0.9

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

   4. Applied times-frac 3.3

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

   6. Applied div-inv 3.3

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

   7. Applied associate-*r* 1.5

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

   8. Simplified 1.3

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

   10. Applied *-un-lft-identity 1.3

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

   11. Applied times-frac 1.3

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

   13. Applied div-inv 1.3

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

4. Final simplification 1.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3.0 \le -7.705332731478375 \cdot 10^{+43}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{3.0}}{z \cdot y}\\ \mathbf{elif}\;z \cdot 3.0 \le 1.640266769777498 \cdot 10^{+158}:\\ \;\;\;\;\frac{\frac{\frac{t}{y}}{3.0}}{z} + \left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{1}{y} \cdot \left(\frac{1}{z} \cdot \frac{t}{3.0}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019158 +o rules:numerics
(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))))