expq3 (problem 3.4.2)

Average Error: 58.4 → 52.6

Time: 38.5s

Precision: 64

• could not determine a ground truth for program body

  1. a = 2.6476780725355068e+101
  2. b = -6.203135907666058e-146
  3. eps = 3.346115000419954e-91

\[-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}\;b \le -1.3823046687346545 \cdot 10^{+106}:\\ \;\;\;\;\frac{\sqrt[3]{\left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right) \cdot \left(\left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right) \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)\right)} \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot a + \left(\left(\left(a \cdot a\right) \cdot a\right) \cdot \left(\varepsilon \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot \varepsilon\right)\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(a \cdot a\right) \cdot \frac{1}{2}\right)\right)\right)}\\ \mathbf{elif}\;b \le 1.981037746615871 \cdot 10^{+71}:\\ \;\;\;\;\frac{\varepsilon \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)}{\frac{\left(e^{\varepsilon \cdot a + \varepsilon \cdot a} \cdot e^{\varepsilon \cdot a} - 1\right) \cdot \left(\left(\frac{1}{2} \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(b \cdot b\right)\right) + \left(\left(b \cdot \left(b \cdot b\right)\right) \cdot \frac{1}{6}\right) \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \varepsilon\right)\right)\right) + \varepsilon \cdot b\right)}{e^{\varepsilon \cdot a} \cdot e^{\varepsilon \cdot a} + \left(e^{\varepsilon \cdot a} + 1\right)}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt[3]{\left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right) \cdot \left(\left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right) \cdot \left(e^{\varepsilon \cdot \left(b + a\right)} - 1\right)\right)} \cdot \varepsilon}{\left(e^{\varepsilon \cdot b} - 1\right) \cdot \left(\varepsilon \cdot a + \left(\left(\left(a \cdot a\right) \cdot a\right) \cdot \left(\varepsilon \cdot \left(\frac{1}{6} \cdot \left(\varepsilon \cdot \varepsilon\right)\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(a \cdot a\right) \cdot \frac{1}{2}\right)\right)\right)}\\ \end{array}\]

C

double f(double a, double b, double eps) {
        double r1463322 = eps;
        double r1463323 = a;
        double r1463324 = b;
        double r1463325 = r1463323 + r1463324;
        double r1463326 = r1463325 * r1463322;
        double r1463327 = exp(r1463326);
        double r1463328 = 1.0;
        double r1463329 = r1463327 - r1463328;
        double r1463330 = r1463322 * r1463329;
        double r1463331 = r1463323 * r1463322;
        double r1463332 = exp(r1463331);
        double r1463333 = r1463332 - r1463328;
        double r1463334 = r1463324 * r1463322;
        double r1463335 = exp(r1463334);
        double r1463336 = r1463335 - r1463328;
        double r1463337 = r1463333 * r1463336;
        double r1463338 = r1463330 / r1463337;
        return r1463338;
}

↓

double f(double a, double b, double eps) {
        double r1463339 = b;
        double r1463340 = -1.3823046687346545e+106;
        bool r1463341 = r1463339 <= r1463340;
        double r1463342 = eps;
        double r1463343 = a;
        double r1463344 = r1463339 + r1463343;
        double r1463345 = r1463342 * r1463344;
        double r1463346 = exp(r1463345);
        double r1463347 = 1.0;
        double r1463348 = r1463346 - r1463347;
        double r1463349 = r1463348 * r1463348;
        double r1463350 = r1463348 * r1463349;
        double r1463351 = cbrt(r1463350);
        double r1463352 = r1463351 * r1463342;
        double r1463353 = r1463342 * r1463339;
        double r1463354 = exp(r1463353);
        double r1463355 = r1463354 - r1463347;
        double r1463356 = r1463342 * r1463343;
        double r1463357 = r1463343 * r1463343;
        double r1463358 = r1463357 * r1463343;
        double r1463359 = 0.16666666666666666;
        double r1463360 = r1463342 * r1463342;
        double r1463361 = r1463359 * r1463360;
        double r1463362 = r1463342 * r1463361;
        double r1463363 = r1463358 * r1463362;
        double r1463364 = 0.5;
        double r1463365 = r1463357 * r1463364;
        double r1463366 = r1463360 * r1463365;
        double r1463367 = r1463363 + r1463366;
        double r1463368 = r1463356 + r1463367;
        double r1463369 = r1463355 * r1463368;
        double r1463370 = r1463352 / r1463369;
        double r1463371 = 1.981037746615871e+71;
        bool r1463372 = r1463339 <= r1463371;
        double r1463373 = r1463342 * r1463348;
        double r1463374 = r1463356 + r1463356;
        double r1463375 = exp(r1463374);
        double r1463376 = exp(r1463356);
        double r1463377 = r1463375 * r1463376;
        double r1463378 = r1463377 - r1463347;
        double r1463379 = r1463339 * r1463339;
        double r1463380 = r1463360 * r1463379;
        double r1463381 = r1463364 * r1463380;
        double r1463382 = r1463339 * r1463379;
        double r1463383 = r1463382 * r1463359;
        double r1463384 = r1463342 * r1463360;
        double r1463385 = r1463383 * r1463384;
        double r1463386 = r1463381 + r1463385;
        double r1463387 = r1463386 + r1463353;
        double r1463388 = r1463378 * r1463387;
        double r1463389 = r1463376 * r1463376;
        double r1463390 = r1463376 + r1463347;
        double r1463391 = r1463389 + r1463390;
        double r1463392 = r1463388 / r1463391;
        double r1463393 = r1463373 / r1463392;
        double r1463394 = r1463372 ? r1463393 : r1463370;
        double r1463395 = r1463341 ? r1463370 : r1463394;
        return r1463395;
}

Error

Bits error versus a

Bits error versus b

Bits error versus eps

Target

Original	58.4
Target	14.2
Herbie	52.6

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

Derivation

1. Split input into 2 regimes

2. if b < -1.3823046687346545e+106 or 1.981037746615871e+71 < b

   1. Initial program 51.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 46.8

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

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

   5. Applied add-cbrt-cube 46.8

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

   if -1.3823046687346545e+106 < b < 1.981037746615871e+71

   1. Initial program 61.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 55.0

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

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

   5. Applied flip3-- 55.2

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

   6. Applied associate-*l/ 55.2

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

   7. Simplified 55.3

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

4. Final simplification 52.6

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

Reproduce

herbie shell --seed 2019128 
(FPCore (a b eps)
  :name "expq3 (problem 3.4.2)"
  :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))))