Average Error: 24.1 → 8.5
Time: 6.3s
Precision: 64
\[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\]
\[\begin{array}{l} \mathbf{if}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\ \mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le -2.83283552082506149 \cdot 10^{-308}:\\ \;\;\;\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\\ \mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le 0.0:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{x}{z} - \frac{t}{z}, t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\ \end{array}\]
x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}
\begin{array}{l}
\mathbf{if}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} = -\infty:\\
\;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\

\mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le -2.83283552082506149 \cdot 10^{-308}:\\
\;\;\;\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\\

\mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le 0.0:\\
\;\;\;\;\mathsf{fma}\left(y, \frac{x}{z} - \frac{t}{z}, t\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r632023 = x;
        double r632024 = y;
        double r632025 = z;
        double r632026 = r632024 - r632025;
        double r632027 = t;
        double r632028 = r632027 - r632023;
        double r632029 = r632026 * r632028;
        double r632030 = a;
        double r632031 = r632030 - r632025;
        double r632032 = r632029 / r632031;
        double r632033 = r632023 + r632032;
        return r632033;
}

double f(double x, double y, double z, double t, double a) {
        double r632034 = x;
        double r632035 = y;
        double r632036 = z;
        double r632037 = r632035 - r632036;
        double r632038 = t;
        double r632039 = r632038 - r632034;
        double r632040 = r632037 * r632039;
        double r632041 = a;
        double r632042 = r632041 - r632036;
        double r632043 = r632040 / r632042;
        double r632044 = r632034 + r632043;
        double r632045 = -inf.0;
        bool r632046 = r632044 <= r632045;
        double r632047 = 1.0;
        double r632048 = r632047 / r632042;
        double r632049 = r632035 * r632048;
        double r632050 = r632036 / r632042;
        double r632051 = r632049 - r632050;
        double r632052 = fma(r632051, r632039, r632034);
        double r632053 = -2.8328355208250615e-308;
        bool r632054 = r632044 <= r632053;
        double r632055 = 0.0;
        bool r632056 = r632044 <= r632055;
        double r632057 = r632034 / r632036;
        double r632058 = r632038 / r632036;
        double r632059 = r632057 - r632058;
        double r632060 = fma(r632035, r632059, r632038);
        double r632061 = r632056 ? r632060 : r632052;
        double r632062 = r632054 ? r632044 : r632061;
        double r632063 = r632046 ? r632052 : r632062;
        return r632063;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original24.1
Target11.9
Herbie8.5
\[\begin{array}{l} \mathbf{if}\;z \lt -1.25361310560950359 \cdot 10^{188}:\\ \;\;\;\;t - \frac{y}{z} \cdot \left(t - x\right)\\ \mathbf{elif}\;z \lt 4.44670236911381103 \cdot 10^{64}:\\ \;\;\;\;x + \frac{y - z}{\frac{a - z}{t - x}}\\ \mathbf{else}:\\ \;\;\;\;t - \frac{y}{z} \cdot \left(t - x\right)\\ \end{array}\]

Derivation

  1. Split input into 3 regimes
  2. if (+ x (/ (* (- y z) (- t x)) (- a z))) < -inf.0 or 0.0 < (+ x (/ (* (- y z) (- t x)) (- a z)))

    1. Initial program 31.2

      \[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\]
    2. Simplified10.2

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y - z}{a - z}, t - x, x\right)}\]
    3. Using strategy rm
    4. Applied div-sub10.2

      \[\leadsto \mathsf{fma}\left(\color{blue}{\frac{y}{a - z} - \frac{z}{a - z}}, t - x, x\right)\]
    5. Using strategy rm
    6. Applied div-inv10.2

      \[\leadsto \mathsf{fma}\left(\color{blue}{y \cdot \frac{1}{a - z}} - \frac{z}{a - z}, t - x, x\right)\]

    if -inf.0 < (+ x (/ (* (- y z) (- t x)) (- a z))) < -2.8328355208250615e-308

    1. Initial program 1.9

      \[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\]

    if -2.8328355208250615e-308 < (+ x (/ (* (- y z) (- t x)) (- a z))) < 0.0

    1. Initial program 61.3

      \[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\]
    2. Simplified61.3

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{y - z}{a - z}, t - x, x\right)}\]
    3. Taylor expanded around inf 20.0

      \[\leadsto \color{blue}{\left(\frac{x \cdot y}{z} + t\right) - \frac{t \cdot y}{z}}\]
    4. Simplified22.9

      \[\leadsto \color{blue}{\mathsf{fma}\left(y, \frac{x}{z} - \frac{t}{z}, t\right)}\]
  3. Recombined 3 regimes into one program.
  4. Final simplification8.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} = -\infty:\\ \;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\ \mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le -2.83283552082506149 \cdot 10^{-308}:\\ \;\;\;\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}\\ \mathbf{elif}\;x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z} \le 0.0:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{x}{z} - \frac{t}{z}, t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y \cdot \frac{1}{a - z} - \frac{z}{a - z}, t - x, x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020062 +o rules:numerics
(FPCore (x y z t a)
  :name "Graphics.Rendering.Chart.Axis.Types:invLinMap from Chart-1.5.3"
  :precision binary64

  :herbie-target
  (if (< z -1.2536131056095036e+188) (- t (* (/ y z) (- t x))) (if (< z 4.446702369113811e+64) (+ x (/ (- y z) (/ (- a z) (- t x)))) (- t (* (/ y z) (- t x)))))

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