Henrywood and Agarwal, Equation (13)

Average Error: 58.0 → 52.0

Time: 2.7m

Precision: 64

• could not determine a ground truth for program body

  1. c0 = 3.156694138789694e+305
  2. w = -2.544427667827882e-153
  3. h = 1.6411170280794751e+38
  4. D = 2.00565441440197e-258
  5. d = -8.42406018902754e+41
  6. M = -1.1769902212814621e-17

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(\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} + \sqrt{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} - M} \cdot \sqrt{\frac{\sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}} \cdot \left(\sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}} \cdot \sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}\right)}{h} + M}\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.7395290708437503 \cdot 10^{+272}:\\ \;\;\;\;\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(\frac{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{\sqrt[3]{h} \cdot \sqrt[3]{h}}}{\sqrt[3]{h}} + \sqrt{\frac{\left(\frac{\sqrt[3]{c0}}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)\right) \cdot \left(\sqrt[3]{c0} \cdot \sqrt[3]{c0}\right)}{h} - M} \cdot \sqrt{M + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}}\right) \cdot \frac{c0}{w}}{2}\\ \end{array}\]

C

double f(double c0, double w, double h, double D, double d, double M) {
        double r27157911 = c0;
        double r27157912 = 2.0;
        double r27157913 = w;
        double r27157914 = r27157912 * r27157913;
        double r27157915 = r27157911 / r27157914;
        double r27157916 = d;
        double r27157917 = r27157916 * r27157916;
        double r27157918 = r27157911 * r27157917;
        double r27157919 = h;
        double r27157920 = r27157913 * r27157919;
        double r27157921 = D;
        double r27157922 = r27157921 * r27157921;
        double r27157923 = r27157920 * r27157922;
        double r27157924 = r27157918 / r27157923;
        double r27157925 = r27157924 * r27157924;
        double r27157926 = M;
        double r27157927 = r27157926 * r27157926;
        double r27157928 = r27157925 - r27157927;
        double r27157929 = sqrt(r27157928);
        double r27157930 = r27157924 + r27157929;
        double r27157931 = r27157915 * r27157930;
        return r27157931;
}

↓

double f(double c0, double w, double h, double D, double d, double M) {
        double r27157932 = c0;
        double r27157933 = w;
        double r27157934 = 2.0;
        double r27157935 = r27157933 * r27157934;
        double r27157936 = r27157932 / r27157935;
        double r27157937 = d;
        double r27157938 = r27157937 * r27157937;
        double r27157939 = r27157932 * r27157938;
        double r27157940 = D;
        double r27157941 = r27157940 * r27157940;
        double r27157942 = h;
        double r27157943 = r27157933 * r27157942;
        double r27157944 = r27157941 * r27157943;
        double r27157945 = r27157939 / r27157944;
        double r27157946 = r27157945 * r27157945;
        double r27157947 = M;
        double r27157948 = r27157947 * r27157947;
        double r27157949 = r27157946 - r27157948;
        double r27157950 = sqrt(r27157949);
        double r27157951 = r27157950 + r27157945;
        double r27157952 = r27157936 * r27157951;
        double r27157953 = -inf.0;
        bool r27157954 = r27157952 <= r27157953;
        double r27157955 = r27157932 / r27157933;
        double r27157956 = r27157937 / r27157940;
        double r27157957 = r27157956 * r27157956;
        double r27157958 = r27157957 * r27157955;
        double r27157959 = r27157958 / r27157942;
        double r27157960 = r27157959 - r27157947;
        double r27157961 = sqrt(r27157960);
        double r27157962 = cbrt(r27157958);
        double r27157963 = r27157962 * r27157962;
        double r27157964 = r27157962 * r27157963;
        double r27157965 = r27157964 / r27157942;
        double r27157966 = r27157965 + r27157947;
        double r27157967 = sqrt(r27157966);
        double r27157968 = r27157961 * r27157967;
        double r27157969 = r27157959 + r27157968;
        double r27157970 = r27157955 * r27157969;
        double r27157971 = r27157970 / r27157934;
        double r27157972 = 1.7395290708437503e+272;
        bool r27157973 = r27157952 <= r27157972;
        double r27157974 = cbrt(r27157942);
        double r27157975 = r27157974 * r27157974;
        double r27157976 = r27157958 / r27157975;
        double r27157977 = r27157976 / r27157974;
        double r27157978 = cbrt(r27157932);
        double r27157979 = r27157978 / r27157933;
        double r27157980 = r27157979 * r27157957;
        double r27157981 = r27157978 * r27157978;
        double r27157982 = r27157980 * r27157981;
        double r27157983 = r27157982 / r27157942;
        double r27157984 = r27157983 - r27157947;
        double r27157985 = sqrt(r27157984);
        double r27157986 = r27157947 + r27157959;
        double r27157987 = sqrt(r27157986);
        double r27157988 = r27157985 * r27157987;
        double r27157989 = r27157977 + r27157988;
        double r27157990 = r27157989 * r27157955;
        double r27157991 = r27157990 / r27157934;
        double r27157992 = r27157973 ? r27157952 : r27157991;
        double r27157993 = r27157954 ? r27157971 : r27157992;
        return r27157993;
}

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

   2. Simplified 55.7

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

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

   6. Applied add-cube-cbrt 46.3

      \[\leadsto \frac{\left(\sqrt{M + \frac{\color{blue}{\left(\sqrt[3]{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)} \cdot \sqrt[3]{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}\right) \cdot \sqrt[3]{\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.7395290708437503e+272

   1. Initial program 22.1

      \[\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.7395290708437503e+272 < (* (/ 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 62.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 55.0

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

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

   6. Applied add-cube-cbrt 56.2

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

   7. Applied associate-/r* 56.2

      \[\leadsto \frac{\left(\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} + \color{blue}{\frac{\frac{\frac{c0}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)}{\sqrt[3]{h} \cdot \sqrt[3]{h}}}{\sqrt[3]{h}}}\right) \cdot \frac{c0}{w}}{2}\]
   8. Using strategy rm

   9. Applied *-un-lft-identity 56.2

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

   10. Applied add-cube-cbrt 56.2

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

   11. Applied times-frac 56.2

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

   12. Applied associate-*l* 56.4

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

   13. Simplified 56.4

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

4. Final simplification 52.0

   \[\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(\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} + \sqrt{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h} - M} \cdot \sqrt{\frac{\sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}} \cdot \left(\sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}} \cdot \sqrt[3]{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}\right)}{h} + M}\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.7395290708437503 \cdot 10^{+272}:\\ \;\;\;\;\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(\frac{\frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{\sqrt[3]{h} \cdot \sqrt[3]{h}}}{\sqrt[3]{h}} + \sqrt{\frac{\left(\frac{\sqrt[3]{c0}}{w} \cdot \left(\frac{d}{D} \cdot \frac{d}{D}\right)\right) \cdot \left(\sqrt[3]{c0} \cdot \sqrt[3]{c0}\right)}{h} - M} \cdot \sqrt{M + \frac{\left(\frac{d}{D} \cdot \frac{d}{D}\right) \cdot \frac{c0}{w}}{h}}\right) \cdot \frac{c0}{w}}{2}\\ \end{array}\]

Reproduce

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