Henrywood and Agarwal, Equation (13)

Average Error: 59.4 → 31.9

Time: 35.6s

Precision: 64

• could not determine a ground truth for program body

  1. c0 = -7.445886573290126e+150
  2. w = 1.4951439070500593e-167
  3. h = 1.1234319124140777e-63
  4. D = 1.4687448223423728e-136
  5. d = -2.9292428393042427e+268
  6. M = -1.737537130071185e+306

Math

\[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) = -\infty \lor \neg \left(\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \le 1.227496136123471417705745916826608723776 \cdot 10^{222}\right):\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)\\ \end{array}\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r98154 = c0;
        double r98155 = 2.0;
        double r98156 = w;
        double r98157 = r98155 * r98156;
        double r98158 = r98154 / r98157;
        double r98159 = d;
        double r98160 = r98159 * r98159;
        double r98161 = r98154 * r98160;
        double r98162 = h;
        double r98163 = r98156 * r98162;
        double r98164 = D;
        double r98165 = r98164 * r98164;
        double r98166 = r98163 * r98165;
        double r98167 = r98161 / r98166;
        double r98168 = r98167 * r98167;
        double r98169 = M;
        double r98170 = r98169 * r98169;
        double r98171 = r98168 - r98170;
        double r98172 = sqrt(r98171);
        double r98173 = r98167 + r98172;
        double r98174 = r98158 * r98173;
        return r98174;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r98175 = c0;
        double r98176 = 2.0;
        double r98177 = w;
        double r98178 = r98176 * r98177;
        double r98179 = r98175 / r98178;
        double r98180 = d;
        double r98181 = r98180 * r98180;
        double r98182 = r98175 * r98181;
        double r98183 = h;
        double r98184 = r98177 * r98183;
        double r98185 = D;
        double r98186 = r98185 * r98185;
        double r98187 = r98184 * r98186;
        double r98188 = r98182 / r98187;
        double r98189 = r98188 * r98188;
        double r98190 = M;
        double r98191 = r98190 * r98190;
        double r98192 = r98189 - r98191;
        double r98193 = sqrt(r98192);
        double r98194 = r98188 + r98193;
        double r98195 = r98179 * r98194;
        double r98196 = -inf.0;
        bool r98197 = r98195 <= r98196;
        double r98198 = 1.2274961361234714e+222;
        bool r98199 = r98195 <= r98198;
        double r98200 = !r98199;
        bool r98201 = r98197 || r98200;
        double r98202 = 0.0;
        double r98203 = r98201 ? r98202 : r98195;
        return r98203;
}

Error

Bits error versus c0

Bits error versus w

Bits error versus h

Bits error versus D

Bits error versus d

Bits error versus M

Derivation

1. Split input into 2 regimes

2. if (* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))) < -inf.0 or 1.2274961361234714e+222 < (* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M)))))

   1. Initial program 63.9

      \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)\]

   2. Taylor expanded around inf 35.3

      \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{0}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt 35.3

      \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(\sqrt{0} \cdot \sqrt{0}\right)}\]

   5. Applied associate-*r* 35.3

      \[\leadsto \color{blue}{\left(\frac{c0}{2 \cdot w} \cdot \sqrt{0}\right) \cdot \sqrt{0}}\]

   6. Simplified 33.1

      \[\leadsto \color{blue}{0} \cdot \sqrt{0}\]

   if -inf.0 < (* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))) < 1.2274961361234714e+222

   1. Initial program 21.9

      \[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)\]
3. Recombined 2 regimes into one program.

4. Final simplification 31.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) = -\infty \lor \neg \left(\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right) \le 1.227496136123471417705745916826608723776 \cdot 10^{222}\right):\\ \;\;\;\;0\\ \mathbf{else}:\\ \;\;\;\;\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019208 
(FPCore (c0 w h D d M)
  :name "Henrywood and Agarwal, Equation (13)"
  :precision binary64
  (* (/ c0 (* 2 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))))