Henrywood and Agarwal, Equation (13)

Average Error: 59.1 → 31.7

Time: 11.4s

Precision: 64

• could not determine a ground truth for program body

  1. c0 = 7.190535231823611e+139
  2. w = -1.0596051947488466e-101
  3. h = 1.5747379203905758e-165
  4. D = -2.312346079725117e-165
  5. d = 1.1303772059324865e+213
  6. M = 1.4174677448928467e-291

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 1.148139620531012480241636539527967342378 \cdot 10^{279}:\\ \;\;\;\;\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 r259930 = c0;
        double r259931 = 2.0;
        double r259932 = w;
        double r259933 = r259931 * r259932;
        double r259934 = r259930 / r259933;
        double r259935 = d;
        double r259936 = r259935 * r259935;
        double r259937 = r259930 * r259936;
        double r259938 = h;
        double r259939 = r259932 * r259938;
        double r259940 = D;
        double r259941 = r259940 * r259940;
        double r259942 = r259939 * r259941;
        double r259943 = r259937 / r259942;
        double r259944 = r259943 * r259943;
        double r259945 = M;
        double r259946 = r259945 * r259945;
        double r259947 = r259944 - r259946;
        double r259948 = sqrt(r259947);
        double r259949 = r259943 + r259948;
        double r259950 = r259934 * r259949;
        return r259950;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r259951 = c0;
        double r259952 = 2.0;
        double r259953 = w;
        double r259954 = r259952 * r259953;
        double r259955 = r259951 / r259954;
        double r259956 = d;
        double r259957 = r259956 * r259956;
        double r259958 = r259951 * r259957;
        double r259959 = h;
        double r259960 = r259953 * r259959;
        double r259961 = D;
        double r259962 = r259961 * r259961;
        double r259963 = r259960 * r259962;
        double r259964 = r259958 / r259963;
        double r259965 = r259964 * r259964;
        double r259966 = M;
        double r259967 = r259966 * r259966;
        double r259968 = r259965 - r259967;
        double r259969 = sqrt(r259968);
        double r259970 = r259964 + r259969;
        double r259971 = r259955 * r259970;
        double r259972 = 1.1481396205310125e+279;
        bool r259973 = r259971 <= r259972;
        double r259974 = 0.0;
        double r259975 = r259973 ? r259971 : r259974;
        return r259975;
}

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))))) < 1.1481396205310125e+279

   1. Initial program 34.3

      \[\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.1481396205310125e+279 < (* (/ 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 33.2

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

   4. Applied mul0 31.2

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

4. Final simplification 31.7

   \[\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 1.148139620531012480241636539527967342378 \cdot 10^{279}:\\ \;\;\;\;\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 2019362 
(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))))))