expq3 (problem 3.4.2)

Average Error: 60.3 → 52.8

Time: 25.0s

Precision: 64

• could not determine a ground truth for program body

  1. a = -4.7556502650462125e+294
  2. b = 2.729864436188278e+247
  3. eps = -3.4107494527315723e-29

\[-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.182965375521188910108414184421595961036 \cdot 10^{212}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(\left(\sqrt[3]{e^{a \cdot \varepsilon} - 1} \cdot \sqrt[3]{e^{a \cdot \varepsilon} - 1}\right) \cdot \sqrt[3]{e^{a \cdot \varepsilon} - 1}\right) \cdot \left(\frac{1}{6} \cdot {\left(\varepsilon \cdot b\right)}^{3} + b \cdot \left(\varepsilon + \left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b\right)\right)}\\ \mathbf{elif}\;a \le -5.631940663491904405136254441698421041501 \cdot 10^{81}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(\left(\sqrt{e^{a \cdot \varepsilon}} + \sqrt{1}\right) \cdot \left(\sqrt{e^{a \cdot \varepsilon}} - \sqrt{1}\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\\ \mathbf{elif}\;a \le 8962964499692349440:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(\frac{1}{6} \cdot \left({a}^{3} \cdot {\varepsilon}^{3}\right) + \varepsilon \cdot \left(\left(\frac{1}{2} \cdot {a}^{2}\right) \cdot \varepsilon + a\right)\right) \cdot \left(e^{b \cdot \varepsilon} - 1\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\left(e^{a \cdot \varepsilon} - 1\right) \cdot \left(\frac{1}{6} \cdot {\left(\varepsilon \cdot b\right)}^{3} + b \cdot \left(\varepsilon + \left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r79951 = eps;
        double r79952 = a;
        double r79953 = b;
        double r79954 = r79952 + r79953;
        double r79955 = r79954 * r79951;
        double r79956 = exp(r79955);
        double r79957 = 1.0;
        double r79958 = r79956 - r79957;
        double r79959 = r79951 * r79958;
        double r79960 = r79952 * r79951;
        double r79961 = exp(r79960);
        double r79962 = r79961 - r79957;
        double r79963 = r79953 * r79951;
        double r79964 = exp(r79963);
        double r79965 = r79964 - r79957;
        double r79966 = r79962 * r79965;
        double r79967 = r79959 / r79966;
        return r79967;
}

↓

double f(double a, double b, double eps) {
        double r79968 = a;
        double r79969 = -2.182965375521189e+212;
        bool r79970 = r79968 <= r79969;
        double r79971 = eps;
        double r79972 = b;
        double r79973 = r79968 + r79972;
        double r79974 = r79973 * r79971;
        double r79975 = exp(r79974);
        double r79976 = 1.0;
        double r79977 = r79975 - r79976;
        double r79978 = r79971 * r79977;
        double r79979 = r79968 * r79971;
        double r79980 = exp(r79979);
        double r79981 = r79980 - r79976;
        double r79982 = cbrt(r79981);
        double r79983 = r79982 * r79982;
        double r79984 = r79983 * r79982;
        double r79985 = 0.16666666666666666;
        double r79986 = r79971 * r79972;
        double r79987 = 3.0;
        double r79988 = pow(r79986, r79987);
        double r79989 = r79985 * r79988;
        double r79990 = 0.5;
        double r79991 = 2.0;
        double r79992 = pow(r79971, r79991);
        double r79993 = r79990 * r79992;
        double r79994 = r79993 * r79972;
        double r79995 = r79971 + r79994;
        double r79996 = r79972 * r79995;
        double r79997 = r79989 + r79996;
        double r79998 = r79984 * r79997;
        double r79999 = r79978 / r79998;
        double r80000 = -5.631940663491904e+81;
        bool r80001 = r79968 <= r80000;
        double r80002 = sqrt(r79980);
        double r80003 = sqrt(r79976);
        double r80004 = r80002 + r80003;
        double r80005 = r80002 - r80003;
        double r80006 = r80004 * r80005;
        double r80007 = r79972 * r79971;
        double r80008 = exp(r80007);
        double r80009 = r80008 - r79976;
        double r80010 = r80006 * r80009;
        double r80011 = r79978 / r80010;
        double r80012 = 8.962964499692349e+18;
        bool r80013 = r79968 <= r80012;
        double r80014 = pow(r79968, r79987);
        double r80015 = pow(r79971, r79987);
        double r80016 = r80014 * r80015;
        double r80017 = r79985 * r80016;
        double r80018 = pow(r79968, r79991);
        double r80019 = r79990 * r80018;
        double r80020 = r80019 * r79971;
        double r80021 = r80020 + r79968;
        double r80022 = r79971 * r80021;
        double r80023 = r80017 + r80022;
        double r80024 = r80023 * r80009;
        double r80025 = r79978 / r80024;
        double r80026 = r79981 * r79997;
        double r80027 = r79978 / r80026;
        double r80028 = r80013 ? r80025 : r80027;
        double r80029 = r80001 ? r80011 : r80028;
        double r80030 = r79970 ? r79999 : r80029;
        return r80030;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.3
Target	14.3
Herbie	52.8

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

Derivation

1. Split input into 4 regimes

2. if a < -2.182965375521189e+212

   1. Initial program 51.3

      \[\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 38.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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}}\]

   3. Simplified 38.5

      \[\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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + b \cdot \left(\varepsilon + \left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b\right)\right)}}\]
   4. Using strategy rm

   5. Applied pow-prod-down 31.2

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

   7. Applied add-cube-cbrt 31.3

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

   if -2.182965375521189e+212 < a < -5.631940663491904e+81

   1. Initial program 55.6

      \[\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-sqr-sqrt 55.6

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

   4. Applied add-sqr-sqrt 55.6

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

   5. Applied difference-of-squares 55.6

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

   if -5.631940663491904e+81 < a < 8.962964499692349e+18

   1. Initial program 63.7

      \[\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.1

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

   3. Simplified 56.1

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

   if 8.962964499692349e+18 < a

   1. Initial program 55.0

      \[\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 49.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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}}\]

   3. Simplified 49.4

      \[\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(\frac{1}{6} \cdot \left({\varepsilon}^{3} \cdot {b}^{3}\right) + b \cdot \left(\varepsilon + \left(\frac{1}{2} \cdot {\varepsilon}^{2}\right) \cdot b\right)\right)}}\]
   4. Using strategy rm

   5. Applied pow-prod-down 47.1

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

4. Final simplification 52.8

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

Reproduce

herbie shell --seed 2019347 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :precision binary64
  :pre (and (< -1 eps) (< eps 1))

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

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