Henrywood and Agarwal, Equation (13)

Average Error: 58.8 → 33.6

Time: 10.2s

Precision: 64

• could not determine a ground truth for program body

  1. c0 = -1.4114346242023061e-15
  2. w = -2.681276240238692e-213
  3. h = -6.25031775875522e-295
  4. D = 1.0832866769276086e-135
  5. d = -6.201413291767227e+130
  6. M = 8.545441081317027e-234

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

↓

\[c0 \cdot 0\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r168440 = c0;
        double r168441 = 2.0;
        double r168442 = w;
        double r168443 = r168441 * r168442;
        double r168444 = r168440 / r168443;
        double r168445 = d;
        double r168446 = r168445 * r168445;
        double r168447 = r168440 * r168446;
        double r168448 = h;
        double r168449 = r168442 * r168448;
        double r168450 = D;
        double r168451 = r168450 * r168450;
        double r168452 = r168449 * r168451;
        double r168453 = r168447 / r168452;
        double r168454 = r168453 * r168453;
        double r168455 = M;
        double r168456 = r168455 * r168455;
        double r168457 = r168454 - r168456;
        double r168458 = sqrt(r168457);
        double r168459 = r168453 + r168458;
        double r168460 = r168444 * r168459;
        return r168460;
}

↓

double f(double c0, double __attribute__((unused)) w, double __attribute__((unused)) h, double __attribute__((unused)) D, double __attribute__((unused)) d, double __attribute__((unused)) M) {
        double r168461 = c0;
        double r168462 = 0.0;
        double r168463 = r168461 * r168462;
        return r168463;
}

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. Initial program 58.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)\]

2. Taylor expanded around inf 35.5

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

4. Applied div-inv 35.5

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

5. Applied associate-*l* 33.6

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

6. Simplified 33.6

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

7. Final simplification 33.6

   \[\leadsto c0 \cdot 0\]

Reproduce

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