Henrywood and Agarwal, Equation (13)

Average Error: 59.5 → 32.3

Time: 12.8s

Precision: 64

• could not determine a ground truth for program body

  1. c0 = 1.5863584066323896e+218
  2. w = -6.40936314096827e-121
  3. h = 2.916611589221061e-242
  4. D = -6.236227832420654e-232
  5. d = 1.237914391097949e+188
  6. M = -9.846484118939197e-181

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 5.3726004056106396 \cdot 10^{222}:\\ \;\;\;\;\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)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array}\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r256328 = c0;
        double r256329 = 2.0;
        double r256330 = w;
        double r256331 = r256329 * r256330;
        double r256332 = r256328 / r256331;
        double r256333 = d;
        double r256334 = r256333 * r256333;
        double r256335 = r256328 * r256334;
        double r256336 = h;
        double r256337 = r256330 * r256336;
        double r256338 = D;
        double r256339 = r256338 * r256338;
        double r256340 = r256337 * r256339;
        double r256341 = r256335 / r256340;
        double r256342 = r256341 * r256341;
        double r256343 = M;
        double r256344 = r256343 * r256343;
        double r256345 = r256342 - r256344;
        double r256346 = sqrt(r256345);
        double r256347 = r256341 + r256346;
        double r256348 = r256332 * r256347;
        return r256348;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r256349 = c0;
        double r256350 = 2.0;
        double r256351 = w;
        double r256352 = r256350 * r256351;
        double r256353 = r256349 / r256352;
        double r256354 = d;
        double r256355 = r256354 * r256354;
        double r256356 = r256349 * r256355;
        double r256357 = h;
        double r256358 = r256351 * r256357;
        double r256359 = D;
        double r256360 = r256359 * r256359;
        double r256361 = r256358 * r256360;
        double r256362 = r256356 / r256361;
        double r256363 = r256362 * r256362;
        double r256364 = M;
        double r256365 = r256364 * r256364;
        double r256366 = r256363 - r256365;
        double r256367 = sqrt(r256366);
        double r256368 = r256362 + r256367;
        double r256369 = r256353 * r256368;
        double r256370 = 5.3726004056106396e+222;
        bool r256371 = r256369 <= r256370;
        double r256372 = 0.0;
        double r256373 = r256371 ? r256369 : r256372;
        return r256373;
}

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))))) < 5.3726004056106396e+222

   1. Initial program 36.0

      \[\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 5.3726004056106396e+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 34.0

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

   4. Applied mul0 31.6

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

4. Final simplification 32.3

   \[\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 5.3726004056106396 \cdot 10^{222}:\\ \;\;\;\;\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)\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array}\]

Reproduce

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