Henrywood and Agarwal, Equation (13)

Average Error: 59.0 → 33.0

Time: 10.6s

Precision: 64

• could not determine a ground truth for program body

  1. c0 = -5.752605726985497e+235
  2. w = 5.554989461521103e-176
  3. h = 4.422134863045769e-57
  4. D = 1.2465098660616616e-166
  5. d = -1.3259787995368483e+39
  6. M = 25578463216848876.0

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) \le 3.520739595750297835234163123325064435018 \cdot 10^{131}:\\ \;\;\;\;\frac{c0}{2 \cdot w} \cdot \left(\sqrt{\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}} \cdot \sqrt{\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)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array}\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r175981 = c0;
        double r175982 = 2.0;
        double r175983 = w;
        double r175984 = r175982 * r175983;
        double r175985 = r175981 / r175984;
        double r175986 = d;
        double r175987 = r175986 * r175986;
        double r175988 = r175981 * r175987;
        double r175989 = h;
        double r175990 = r175983 * r175989;
        double r175991 = D;
        double r175992 = r175991 * r175991;
        double r175993 = r175990 * r175992;
        double r175994 = r175988 / r175993;
        double r175995 = r175994 * r175994;
        double r175996 = M;
        double r175997 = r175996 * r175996;
        double r175998 = r175995 - r175997;
        double r175999 = sqrt(r175998);
        double r176000 = r175994 + r175999;
        double r176001 = r175985 * r176000;
        return r176001;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r176002 = c0;
        double r176003 = 2.0;
        double r176004 = w;
        double r176005 = r176003 * r176004;
        double r176006 = r176002 / r176005;
        double r176007 = d;
        double r176008 = r176007 * r176007;
        double r176009 = r176002 * r176008;
        double r176010 = h;
        double r176011 = r176004 * r176010;
        double r176012 = D;
        double r176013 = r176012 * r176012;
        double r176014 = r176011 * r176013;
        double r176015 = r176009 / r176014;
        double r176016 = r176015 * r176015;
        double r176017 = M;
        double r176018 = r176017 * r176017;
        double r176019 = r176016 - r176018;
        double r176020 = sqrt(r176019);
        double r176021 = r176015 + r176020;
        double r176022 = r176006 * r176021;
        double r176023 = 3.520739595750298e+131;
        bool r176024 = r176022 <= r176023;
        double r176025 = sqrt(r176021);
        double r176026 = r176025 * r176025;
        double r176027 = r176006 * r176026;
        double r176028 = 0.0;
        double r176029 = r176024 ? r176027 : r176028;
        return r176029;
}

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))))) < 3.520739595750298e+131

   1. Initial program 35.2

      \[\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. Using strategy rm

   3. Applied add-sqr-sqrt 36.0

      \[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(\sqrt{\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}} \cdot \sqrt{\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)}\]

   if 3.520739595750298e+131 < (* (/ 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.6

      \[\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 34.4

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

   4. Applied *-un-lft-identity 34.4

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

   5. Applied associate-*l* 34.4

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

   6. Simplified 32.4

      \[\leadsto 1 \cdot \color{blue}{0}\]
3. Recombined 2 regimes into one program.

4. Final simplification 33.0

   \[\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) \le 3.520739595750297835234163123325064435018 \cdot 10^{131}:\\ \;\;\;\;\frac{c0}{2 \cdot w} \cdot \left(\sqrt{\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}} \cdot \sqrt{\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)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array}\]

Reproduce

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