Henrywood and Agarwal, Equation (13)

Average Error: 58.2 → 51.1

Time: 2.7m

Precision: 64

• could not determine a ground truth for program body

  1. c0 = 3.17180604621685e+229
  2. w = -6.0148333844790955e-55
  3. h = 2.124206871236763e-145
  4. D = -3.2024855525006606e-197
  5. d = 8.652459337637894e+67
  6. M = 3.2784584263384346e+125

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}{w \cdot 2} \cdot \left(\sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} - M \cdot M} + \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)}\right) = -\infty:\\ \;\;\;\;\frac{\frac{c0}{w} \cdot \left(\sqrt{M + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}} \cdot \sqrt{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} - M} + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}\right)}{2}\\ \mathbf{elif}\;\frac{c0}{w \cdot 2} \cdot \left(\sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} - M \cdot M} + \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)}\right) \le 1.5526347653738955 \cdot 10^{-242}:\\ \;\;\;\;\frac{c0}{w \cdot 2} \cdot \left(\sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)} - M \cdot M} + \frac{c0 \cdot \left(d \cdot d\right)}{\left(D \cdot D\right) \cdot \left(w \cdot h\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\sqrt{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} + \sqrt{\left(M + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}\right) \cdot \left(\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} - M\right)}} \cdot \sqrt{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} + \sqrt{\left(M + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}\right) \cdot \left(\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} - M\right)}}\right) \cdot \frac{c0}{w}}{2}\\ \end{array}\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r57960153 = c0;
        double r57960154 = 2.0;
        double r57960155 = w;
        double r57960156 = r57960154 * r57960155;
        double r57960157 = r57960153 / r57960156;
        double r57960158 = d;
        double r57960159 = r57960158 * r57960158;
        double r57960160 = r57960153 * r57960159;
        double r57960161 = h;
        double r57960162 = r57960155 * r57960161;
        double r57960163 = D;
        double r57960164 = r57960163 * r57960163;
        double r57960165 = r57960162 * r57960164;
        double r57960166 = r57960160 / r57960165;
        double r57960167 = r57960166 * r57960166;
        double r57960168 = M;
        double r57960169 = r57960168 * r57960168;
        double r57960170 = r57960167 - r57960169;
        double r57960171 = sqrt(r57960170);
        double r57960172 = r57960166 + r57960171;
        double r57960173 = r57960157 * r57960172;
        return r57960173;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r57960174 = c0;
        double r57960175 = w;
        double r57960176 = 2.0;
        double r57960177 = r57960175 * r57960176;
        double r57960178 = r57960174 / r57960177;
        double r57960179 = d;
        double r57960180 = r57960179 * r57960179;
        double r57960181 = r57960174 * r57960180;
        double r57960182 = D;
        double r57960183 = r57960182 * r57960182;
        double r57960184 = h;
        double r57960185 = r57960175 * r57960184;
        double r57960186 = r57960183 * r57960185;
        double r57960187 = r57960181 / r57960186;
        double r57960188 = r57960187 * r57960187;
        double r57960189 = M;
        double r57960190 = r57960189 * r57960189;
        double r57960191 = r57960188 - r57960190;
        double r57960192 = sqrt(r57960191);
        double r57960193 = r57960192 + r57960187;
        double r57960194 = r57960178 * r57960193;
        double r57960195 = -inf.0;
        bool r57960196 = r57960194 <= r57960195;
        double r57960197 = r57960174 / r57960175;
        double r57960198 = r57960179 / r57960182;
        double r57960199 = r57960198 * r57960198;
        double r57960200 = r57960199 * r57960197;
        double r57960201 = r57960200 / r57960184;
        double r57960202 = r57960189 + r57960201;
        double r57960203 = sqrt(r57960202);
        double r57960204 = r57960201 - r57960189;
        double r57960205 = sqrt(r57960204);
        double r57960206 = r57960203 * r57960205;
        double r57960207 = r57960206 + r57960201;
        double r57960208 = r57960197 * r57960207;
        double r57960209 = r57960208 / r57960176;
        double r57960210 = 1.5526347653738955e-242;
        bool r57960211 = r57960194 <= r57960210;
        double r57960212 = r57960202 * r57960204;
        double r57960213 = sqrt(r57960212);
        double r57960214 = r57960201 + r57960213;
        double r57960215 = sqrt(r57960214);
        double r57960216 = r57960215 * r57960215;
        double r57960217 = r57960216 * r57960197;
        double r57960218 = r57960217 / r57960176;
        double r57960219 = r57960211 ? r57960194 : r57960218;
        double r57960220 = r57960196 ? r57960209 : r57960219;
        return r57960220;
}

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 3 regimes

2. if (* (/ 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))))) < -inf.0

   1. Initial program 61.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. Simplified 54.8

      \[\leadsto \color{blue}{\frac{\left(\sqrt{\left(M + \frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h}\right) \cdot \left(\frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h} - M\right)} + \frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h}\right) \cdot \frac{c0}{w}}{2}}\]
   3. Using strategy rm

   4. Applied sqrt-prod 42.9

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

   if -inf.0 < (* (/ 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))))) < 1.5526347653738955e-242

   1. Initial program 23.8

      \[\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)\]

   if 1.5526347653738955e-242 < (* (/ 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)))))

   1. Initial program 61.7

      \[\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. Simplified 54.2

      \[\leadsto \color{blue}{\frac{\left(\sqrt{\left(M + \frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h}\right) \cdot \left(\frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h} - M\right)} + \frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{h}\right) \cdot \frac{c0}{w}}{2}}\]
   3. Using strategy rm

   4. Applied add-sqr-sqrt 54.5

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

4. Final simplification 51.1

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

Reproduce

herbie shell --seed 2019121 
(FPCore (c0 w h D d M)
  :name "Henrywood and Agarwal, Equation (13)"
  (* (/ 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))))))