Average Error: 7.3 → 3.7
Time: 19.2s
Precision: 64
\[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
\[\begin{array}{l} \mathbf{if}\;z \le -5.0213726882368712246896067821148316655 \cdot 10^{81} \lor \neg \left(z \le 2.653747744881045351380565842467581880116 \cdot 10^{131}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}{x + 1}\\ \end{array}\]
\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\begin{array}{l}
\mathbf{if}\;z \le -5.0213726882368712246896067821148316655 \cdot 10^{81} \lor \neg \left(z \le 2.653747744881045351380565842467581880116 \cdot 10^{131}\right):\\
\;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\

\mathbf{else}:\\
\;\;\;\;\frac{x + \left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}{x + 1}\\

\end{array}
double f(double x, double y, double z, double t) {
        double r453365 = x;
        double r453366 = y;
        double r453367 = z;
        double r453368 = r453366 * r453367;
        double r453369 = r453368 - r453365;
        double r453370 = t;
        double r453371 = r453370 * r453367;
        double r453372 = r453371 - r453365;
        double r453373 = r453369 / r453372;
        double r453374 = r453365 + r453373;
        double r453375 = 1.0;
        double r453376 = r453365 + r453375;
        double r453377 = r453374 / r453376;
        return r453377;
}

double f(double x, double y, double z, double t) {
        double r453378 = z;
        double r453379 = -5.021372688236871e+81;
        bool r453380 = r453378 <= r453379;
        double r453381 = 2.6537477448810454e+131;
        bool r453382 = r453378 <= r453381;
        double r453383 = !r453382;
        bool r453384 = r453380 || r453383;
        double r453385 = x;
        double r453386 = y;
        double r453387 = t;
        double r453388 = r453386 / r453387;
        double r453389 = r453385 + r453388;
        double r453390 = 1.0;
        double r453391 = r453385 + r453390;
        double r453392 = r453389 / r453391;
        double r453393 = r453386 * r453378;
        double r453394 = r453393 - r453385;
        double r453395 = 1.0;
        double r453396 = r453387 * r453378;
        double r453397 = r453396 - r453385;
        double r453398 = r453395 / r453397;
        double r453399 = r453394 * r453398;
        double r453400 = r453385 + r453399;
        double r453401 = r453400 / r453391;
        double r453402 = r453384 ? r453392 : r453401;
        return r453402;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original7.3
Target0.4
Herbie3.7
\[\frac{x + \left(\frac{y}{t - \frac{x}{z}} - \frac{x}{t \cdot z - x}\right)}{x + 1}\]

Derivation

  1. Split input into 2 regimes
  2. if z < -5.021372688236871e+81 or 2.6537477448810454e+131 < z

    1. Initial program 19.7

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
    2. Taylor expanded around inf 8.1

      \[\leadsto \frac{x + \color{blue}{\frac{y}{t}}}{x + 1}\]

    if -5.021372688236871e+81 < z < 2.6537477448810454e+131

    1. Initial program 1.6

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
    2. Using strategy rm
    3. Applied div-inv1.7

      \[\leadsto \frac{x + \color{blue}{\left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}}{x + 1}\]
  3. Recombined 2 regimes into one program.
  4. Final simplification3.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -5.0213726882368712246896067821148316655 \cdot 10^{81} \lor \neg \left(z \le 2.653747744881045351380565842467581880116 \cdot 10^{131}\right):\\ \;\;\;\;\frac{x + \frac{y}{t}}{x + 1}\\ \mathbf{else}:\\ \;\;\;\;\frac{x + \left(y \cdot z - x\right) \cdot \frac{1}{t \cdot z - x}}{x + 1}\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 
(FPCore (x y z t)
  :name "Diagrams.Trail:splitAtParam  from diagrams-lib-1.3.0.3, A"

  :herbie-target
  (/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1.0))

  (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)))