AI.Clustering.Hierarchical.Internal:ward from clustering-0.2.1

Average Error: 26.4 → 7.5

Time: 13.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} = -\infty \lor \neg \left(\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} \le 1.3789470957892983 \cdot 10^{302}\right):\\ \;\;\;\;\left(a + z\right) - b\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1} \cdot \frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{y + \left(x + t\right)}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r936104 = x;
        double r936105 = y;
        double r936106 = r936104 + r936105;
        double r936107 = z;
        double r936108 = r936106 * r936107;
        double r936109 = t;
        double r936110 = r936109 + r936105;
        double r936111 = a;
        double r936112 = r936110 * r936111;
        double r936113 = r936108 + r936112;
        double r936114 = b;
        double r936115 = r936105 * r936114;
        double r936116 = r936113 - r936115;
        double r936117 = r936104 + r936109;
        double r936118 = r936117 + r936105;
        double r936119 = r936116 / r936118;
        return r936119;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r936120 = x;
        double r936121 = y;
        double r936122 = r936120 + r936121;
        double r936123 = z;
        double r936124 = r936122 * r936123;
        double r936125 = t;
        double r936126 = r936125 + r936121;
        double r936127 = a;
        double r936128 = r936126 * r936127;
        double r936129 = r936124 + r936128;
        double r936130 = b;
        double r936131 = r936121 * r936130;
        double r936132 = r936129 - r936131;
        double r936133 = r936120 + r936125;
        double r936134 = r936133 + r936121;
        double r936135 = r936132 / r936134;
        double r936136 = -inf.0;
        bool r936137 = r936135 <= r936136;
        double r936138 = 1.3789470957892983e+302;
        bool r936139 = r936135 <= r936138;
        double r936140 = !r936139;
        bool r936141 = r936137 || r936140;
        double r936142 = r936127 + r936123;
        double r936143 = r936142 - r936130;
        double r936144 = 1.0;
        double r936145 = sqrt(r936144);
        double r936146 = r936121 + r936133;
        double r936147 = r936132 / r936146;
        double r936148 = r936145 * r936147;
        double r936149 = r936141 ? r936143 : r936148;
        return r936149;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original	26.4
Target	11.3
Herbie	7.5

\[\begin{array}{l} \mathbf{if}\;\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} \lt -3.5813117084150564 \cdot 10^{153}:\\ \;\;\;\;\left(z + a\right) - b\\ \mathbf{elif}\;\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} \lt 1.2285964308315609 \cdot 10^{82}:\\ \;\;\;\;\frac{1}{\frac{\left(x + t\right) + y}{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}}\\ \mathbf{else}:\\ \;\;\;\;\left(z + a\right) - b\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) < -inf.0 or 1.3789470957892983e+302 < (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y))

   1. Initial program 63.8

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

   3. Applied clear-num 63.8

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

   4. Taylor expanded around 0 17.9

      \[\leadsto \color{blue}{\left(a + z\right) - b}\]

   if -inf.0 < (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) < 1.3789470957892983e+302

   1. Initial program 0.3

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

   3. Applied clear-num 0.5

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

   5. Applied div-inv 0.6

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

   6. Applied add-cube-cbrt 0.6

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

   7. Applied times-frac 0.6

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

   8. Simplified 0.6

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

   9. Simplified 0.5

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

   11. Applied *-un-lft-identity 0.5

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

   12. Applied add-sqr-sqrt 0.5

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

   13. Applied times-frac 0.5

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

   14. Applied associate-*l* 0.5

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

   15. Simplified 0.3

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

4. Final simplification 7.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} = -\infty \lor \neg \left(\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y} \le 1.3789470957892983 \cdot 10^{302}\right):\\ \;\;\;\;\left(a + z\right) - b\\ \mathbf{else}:\\ \;\;\;\;\sqrt{1} \cdot \frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{y + \left(x + t\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2020047 
(FPCore (x y z t a b)
  :name "AI.Clustering.Hierarchical.Internal:ward from clustering-0.2.1"
  :precision binary64

  :herbie-target
  (if (< (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) -3.5813117084150564e+153) (- (+ z a) b) (if (< (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) 1.2285964308315609e+82) (/ 1 (/ (+ (+ x t) y) (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)))) (- (+ z a) b)))

  (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)))