expq3 (problem 3.4.2)

Average Error: 60.1 → 54.1

Time: 33.8s

Precision: 64

• could not determine a ground truth for program body

  1. a = 1.6319567410786448e+172
  2. b = -2.2165513848511907e-128
  3. eps = 3.719314440668339e-44

\[-1 \lt \varepsilon \land \varepsilon \lt 1\]

Math

\[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

↓

\[\begin{array}{l} \mathbf{if}\;a \le -2.072555863211773238369992508225931930817 \cdot 10^{161}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\sqrt[3]{\left(\left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right)\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right)}}\\ \mathbf{elif}\;a \le 7.839366344298225314827142646080308114179 \cdot 10^{152}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(\left(\frac{1}{6} \cdot \left(a \cdot a\right)\right) \cdot a\right) \cdot \varepsilon + \left(a \cdot a\right) \cdot \frac{1}{2}\right) + \varepsilon \cdot a\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\sqrt[3]{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)\right)} \cdot \left(\left(b \cdot \left(b \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{1}{6} \cdot \varepsilon\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \frac{1}{2}\right)\right) \cdot b + \varepsilon \cdot b\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r4642856 = eps;
        double r4642857 = a;
        double r4642858 = b;
        double r4642859 = r4642857 + r4642858;
        double r4642860 = r4642859 * r4642856;
        double r4642861 = exp(r4642860);
        double r4642862 = 1.0;
        double r4642863 = r4642861 - r4642862;
        double r4642864 = r4642856 * r4642863;
        double r4642865 = r4642857 * r4642856;
        double r4642866 = exp(r4642865);
        double r4642867 = r4642866 - r4642862;
        double r4642868 = r4642858 * r4642856;
        double r4642869 = exp(r4642868);
        double r4642870 = r4642869 - r4642862;
        double r4642871 = r4642867 * r4642870;
        double r4642872 = r4642864 / r4642871;
        return r4642872;
}

↓

double f(double a, double b, double eps) {
        double r4642873 = a;
        double r4642874 = -2.0725558632117732e+161;
        bool r4642875 = r4642873 <= r4642874;
        double r4642876 = eps;
        double r4642877 = b;
        double r4642878 = r4642873 + r4642877;
        double r4642879 = r4642876 * r4642878;
        double r4642880 = exp(r4642879);
        double r4642881 = 1.0;
        double r4642882 = r4642880 - r4642881;
        double r4642883 = r4642876 * r4642882;
        double r4642884 = r4642876 * r4642873;
        double r4642885 = exp(r4642884);
        double r4642886 = r4642885 - r4642881;
        double r4642887 = r4642876 * r4642877;
        double r4642888 = exp(r4642887);
        double r4642889 = r4642888 - r4642881;
        double r4642890 = r4642886 * r4642889;
        double r4642891 = r4642890 * r4642890;
        double r4642892 = r4642891 * r4642890;
        double r4642893 = cbrt(r4642892);
        double r4642894 = r4642883 / r4642893;
        double r4642895 = 7.839366344298225e+152;
        bool r4642896 = r4642873 <= r4642895;
        double r4642897 = r4642876 * r4642876;
        double r4642898 = 0.16666666666666666;
        double r4642899 = r4642873 * r4642873;
        double r4642900 = r4642898 * r4642899;
        double r4642901 = r4642900 * r4642873;
        double r4642902 = r4642901 * r4642876;
        double r4642903 = 0.5;
        double r4642904 = r4642899 * r4642903;
        double r4642905 = r4642902 + r4642904;
        double r4642906 = r4642897 * r4642905;
        double r4642907 = r4642906 + r4642884;
        double r4642908 = r4642889 * r4642907;
        double r4642909 = r4642883 / r4642908;
        double r4642910 = r4642886 * r4642886;
        double r4642911 = r4642886 * r4642910;
        double r4642912 = cbrt(r4642911);
        double r4642913 = r4642898 * r4642876;
        double r4642914 = r4642897 * r4642913;
        double r4642915 = r4642877 * r4642914;
        double r4642916 = r4642897 * r4642903;
        double r4642917 = r4642915 + r4642916;
        double r4642918 = r4642877 * r4642917;
        double r4642919 = r4642918 * r4642877;
        double r4642920 = r4642919 + r4642887;
        double r4642921 = r4642912 * r4642920;
        double r4642922 = r4642883 / r4642921;
        double r4642923 = r4642896 ? r4642909 : r4642922;
        double r4642924 = r4642875 ? r4642894 : r4642923;
        return r4642924;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.1
Target	15.2
Herbie	54.1

\[\frac{a + b}{a \cdot b}\]

Derivation

1. Split input into 3 regimes

2. if a < -2.0725558632117732e+161

   1. Initial program 49.1

      \[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]
   2. Using strategy rm

   3. Applied add-cbrt-cube 49.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \color{blue}{\sqrt[3]{\left(\left(e^{b \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}}}\]

   4. Applied add-cbrt-cube 49.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\sqrt[3]{\left(\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)}} \cdot \sqrt[3]{\left(\left(e^{b \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}}\]

   5. Applied cbrt-unprod 49.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\sqrt[3]{\left(\left(\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)\right) \cdot \left(\left(\left(e^{b \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)\right)}}}\]

   6. Simplified 49.1

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\sqrt[3]{\color{blue}{\left(\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)\right) \cdot \left(\left(\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)\right) \cdot \left(\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)\right)\right)}}}\]

   if -2.0725558632117732e+161 < a < 7.839366344298225e+152

   1. Initial program 62.4

      \[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   2. Taylor expanded around 0 56.7

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\frac{1}{2} \cdot \left({a}^{2} \cdot {\varepsilon}^{2}\right) + \left(\frac{1}{6} \cdot \left({a}^{3} \cdot {\varepsilon}^{3}\right) + a \cdot \varepsilon\right)\right)} \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   3. Simplified 56.7

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(a \cdot a\right) \cdot \frac{1}{2} + \left(\left(\frac{1}{6} \cdot \left(a \cdot a\right)\right) \cdot a\right) \cdot \varepsilon\right) + \varepsilon \cdot a\right)} \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   if 7.839366344298225e+152 < a

   1. Initial program 51.9

      \[\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\]

   2. Taylor expanded around 0 43.6

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \color{blue}{\left(\varepsilon \cdot b + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right)\right)\right)}}\]

   3. Simplified 40.8

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \color{blue}{\left(\varepsilon \cdot b + \left(b \cdot b\right) \cdot \left(\left(\left(\frac{1}{6} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot b + \left(\varepsilon \cdot \varepsilon\right) \cdot \frac{1}{2}\right)\right)}}\]
   4. Using strategy rm

   5. Applied associate-*l* 38.3

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(\varepsilon \cdot b + \color{blue}{b \cdot \left(b \cdot \left(\left(\left(\frac{1}{6} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot b + \left(\varepsilon \cdot \varepsilon\right) \cdot \frac{1}{2}\right)\right)}\right)}\]
   6. Using strategy rm

   7. Applied add-cbrt-cube 38.4

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\sqrt[3]{\left(\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)\right) \cdot \left(e^{a \cdot \varepsilon} - 1\right)}} \cdot \left(\varepsilon \cdot b + b \cdot \left(b \cdot \left(\left(\left(\frac{1}{6} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot b + \left(\varepsilon \cdot \varepsilon\right) \cdot \frac{1}{2}\right)\right)\right)}\]
3. Recombined 3 regimes into one program.

4. Final simplification 54.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;a \le -2.072555863211773238369992508225931930817 \cdot 10^{161}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\sqrt[3]{\left(\left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right)\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot b} - 1\right)\right)}}\\ \mathbf{elif}\;a \le 7.839366344298225314827142646080308114179 \cdot 10^{152}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(\left(\frac{1}{6} \cdot \left(a \cdot a\right)\right) \cdot a\right) \cdot \varepsilon + \left(a \cdot a\right) \cdot \frac{1}{2}\right) + \varepsilon \cdot a\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(a + b\right)} - 1\right)}{\sqrt[3]{\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(\left(e^{\varepsilon \cdot a} - 1\right) \cdot \left(e^{\varepsilon \cdot a} - 1\right)\right)} \cdot \left(\left(b \cdot \left(b \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{1}{6} \cdot \varepsilon\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \frac{1}{2}\right)\right) \cdot b + \varepsilon \cdot b\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019171 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :pre (and (< -1.0 eps) (< eps 1.0))

  :herbie-target
  (/ (+ a b) (* a b))

  (/ (* eps (- (exp (* (+ a b) eps)) 1.0)) (* (- (exp (* a eps)) 1.0) (- (exp (* b eps)) 1.0))))