expq3 (problem 3.4.2)

Average Error: 60.6 → 52.4

Time: 13.1s

Precision: 64

• could not determine a ground truth for program body

  1. a = -2.925724657482853e-101
  2. b = -1.1070142065036704e+182
  3. eps = -2.8844001543230743e-81

\[-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 -346828314544410.562:\\ \;\;\;\;\frac{\varepsilon \cdot \frac{\left(-1 \cdot 1\right) + {\left(e^{a + b}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{\left(a + b\right) \cdot \varepsilon} + 1}}{\frac{\left(-1 \cdot 1\right) + {\left(e^{a}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{a \cdot \varepsilon} + 1} \cdot \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)}\\ \mathbf{elif}\;a \le 3.5459178958752838 \cdot 10^{64}:\\ \;\;\;\;\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) + \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)}\\ \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(\left(\left({\varepsilon}^{3} \cdot b\right) \cdot b\right) \cdot b\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r106681 = eps;
        double r106682 = a;
        double r106683 = b;
        double r106684 = r106682 + r106683;
        double r106685 = r106684 * r106681;
        double r106686 = exp(r106685);
        double r106687 = 1.0;
        double r106688 = r106686 - r106687;
        double r106689 = r106681 * r106688;
        double r106690 = r106682 * r106681;
        double r106691 = exp(r106690);
        double r106692 = r106691 - r106687;
        double r106693 = r106683 * r106681;
        double r106694 = exp(r106693);
        double r106695 = r106694 - r106687;
        double r106696 = r106692 * r106695;
        double r106697 = r106689 / r106696;
        return r106697;
}

↓

double f(double a, double b, double eps) {
        double r106698 = a;
        double r106699 = -346828314544410.56;
        bool r106700 = r106698 <= r106699;
        double r106701 = eps;
        double r106702 = 1.0;
        double r106703 = r106702 * r106702;
        double r106704 = -r106703;
        double r106705 = b;
        double r106706 = r106698 + r106705;
        double r106707 = exp(r106706);
        double r106708 = 2.0;
        double r106709 = r106708 * r106701;
        double r106710 = pow(r106707, r106709);
        double r106711 = r106704 + r106710;
        double r106712 = r106706 * r106701;
        double r106713 = exp(r106712);
        double r106714 = r106713 + r106702;
        double r106715 = r106711 / r106714;
        double r106716 = r106701 * r106715;
        double r106717 = exp(r106698);
        double r106718 = pow(r106717, r106709);
        double r106719 = r106704 + r106718;
        double r106720 = r106698 * r106701;
        double r106721 = exp(r106720);
        double r106722 = r106721 + r106702;
        double r106723 = r106719 / r106722;
        double r106724 = 0.16666666666666666;
        double r106725 = 3.0;
        double r106726 = pow(r106701, r106725);
        double r106727 = pow(r106705, r106725);
        double r106728 = r106726 * r106727;
        double r106729 = r106724 * r106728;
        double r106730 = 0.5;
        double r106731 = pow(r106701, r106708);
        double r106732 = pow(r106705, r106708);
        double r106733 = r106731 * r106732;
        double r106734 = r106730 * r106733;
        double r106735 = r106701 * r106705;
        double r106736 = r106734 + r106735;
        double r106737 = r106729 + r106736;
        double r106738 = r106723 * r106737;
        double r106739 = r106716 / r106738;
        double r106740 = 3.545917895875284e+64;
        bool r106741 = r106698 <= r106740;
        double r106742 = r106713 - r106702;
        double r106743 = r106701 * r106742;
        double r106744 = pow(r106698, r106725);
        double r106745 = r106744 * r106726;
        double r106746 = r106724 * r106745;
        double r106747 = pow(r106698, r106708);
        double r106748 = r106747 * r106731;
        double r106749 = r106730 * r106748;
        double r106750 = r106749 + r106720;
        double r106751 = r106746 + r106750;
        double r106752 = r106705 * r106701;
        double r106753 = exp(r106752);
        double r106754 = r106753 - r106702;
        double r106755 = r106751 * r106754;
        double r106756 = r106743 / r106755;
        double r106757 = r106721 - r106702;
        double r106758 = r106726 * r106705;
        double r106759 = r106758 * r106705;
        double r106760 = r106759 * r106705;
        double r106761 = r106724 * r106760;
        double r106762 = r106761 + r106736;
        double r106763 = r106757 * r106762;
        double r106764 = r106743 / r106763;
        double r106765 = r106741 ? r106756 : r106764;
        double r106766 = r106700 ? r106739 : r106765;
        return r106766;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	60.6
Target	14.7
Herbie	52.4

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

Derivation

1. Split input into 3 regimes

2. if a < -346828314544410.56

   1. Initial program 55.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 49.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. Using strategy rm

   4. Applied flip-- 50.2

      \[\leadsto \frac{\varepsilon \cdot \left(e^{\left(a + b\right) \cdot \varepsilon} - 1\right)}{\color{blue}{\frac{e^{a \cdot \varepsilon} \cdot e^{a \cdot \varepsilon} - 1 \cdot 1}{e^{a \cdot \varepsilon} + 1}} \cdot \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)}\]

   5. Simplified 51.4

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

   7. Applied flip-- 51.4

      \[\leadsto \frac{\varepsilon \cdot \color{blue}{\frac{e^{\left(a + b\right) \cdot \varepsilon} \cdot e^{\left(a + b\right) \cdot \varepsilon} - 1 \cdot 1}{e^{\left(a + b\right) \cdot \varepsilon} + 1}}}{\frac{\left(-1 \cdot 1\right) + {\left(e^{a}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{a \cdot \varepsilon} + 1} \cdot \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)}\]

   8. Simplified 45.4

      \[\leadsto \frac{\varepsilon \cdot \frac{\color{blue}{\left(-1 \cdot 1\right) + {\left(e^{a + b}\right)}^{\left(2 \cdot \varepsilon\right)}}}{e^{\left(a + b\right) \cdot \varepsilon} + 1}}{\frac{\left(-1 \cdot 1\right) + {\left(e^{a}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{a \cdot \varepsilon} + 1} \cdot \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)}\]

   if -346828314544410.56 < a < 3.545917895875284e+64

   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.4

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

   if 3.545917895875284e+64 < 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 47.3

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

   4. Applied unpow3 47.3

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

   5. Applied associate-*r* 46.4

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

   6. Simplified 45.7

      \[\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 \left(\color{blue}{\left(\left({\varepsilon}^{3} \cdot b\right) \cdot b\right)} \cdot b\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}\]
3. Recombined 3 regimes into one program.

4. Final simplification 52.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;a \le -346828314544410.562:\\ \;\;\;\;\frac{\varepsilon \cdot \frac{\left(-1 \cdot 1\right) + {\left(e^{a + b}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{\left(a + b\right) \cdot \varepsilon} + 1}}{\frac{\left(-1 \cdot 1\right) + {\left(e^{a}\right)}^{\left(2 \cdot \varepsilon\right)}}{e^{a \cdot \varepsilon} + 1} \cdot \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)}\\ \mathbf{elif}\;a \le 3.5459178958752838 \cdot 10^{64}:\\ \;\;\;\;\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) + \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)}\\ \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(\left(\left({\varepsilon}^{3} \cdot b\right) \cdot b\right) \cdot b\right) + \left(\frac{1}{2} \cdot \left({\varepsilon}^{2} \cdot {b}^{2}\right) + \varepsilon \cdot b\right)\right)}\\ \end{array}\]

Reproduce

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