Average Error: 15.8 → 5.6
Time: 13.5s
Precision: binary64
Cost: 7368
\[\left(x + y\right) - \frac{\left(z - t\right) \cdot y}{a - t} \]
\[\begin{array}{l} t_1 := x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)\\ \mathbf{if}\;a \leq -1 \cdot 10^{-112}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;a \leq 1.775387927039081 \cdot 10^{-67}:\\ \;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
(FPCore (x y z t a) :precision binary64 (- (+ x y) (/ (* (- z t) y) (- a t))))
(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (+ x (fma y (/ (- z t) (- t a)) y))))
   (if (<= a -1e-112)
     t_1
     (if (<= a 1.775387927039081e-67) (+ x (/ z (/ (- t a) y))) t_1))))
double code(double x, double y, double z, double t, double a) {
	return (x + y) - (((z - t) * y) / (a - t));
}
double code(double x, double y, double z, double t, double a) {
	double t_1 = x + fma(y, ((z - t) / (t - a)), y);
	double tmp;
	if (a <= -1e-112) {
		tmp = t_1;
	} else if (a <= 1.775387927039081e-67) {
		tmp = x + (z / ((t - a) / y));
	} else {
		tmp = t_1;
	}
	return tmp;
}
function code(x, y, z, t, a)
	return Float64(Float64(x + y) - Float64(Float64(Float64(z - t) * y) / Float64(a - t)))
end
function code(x, y, z, t, a)
	t_1 = Float64(x + fma(y, Float64(Float64(z - t) / Float64(t - a)), y))
	tmp = 0.0
	if (a <= -1e-112)
		tmp = t_1;
	elseif (a <= 1.775387927039081e-67)
		tmp = Float64(x + Float64(z / Float64(Float64(t - a) / y)));
	else
		tmp = t_1;
	end
	return tmp
end
code[x_, y_, z_, t_, a_] := N[(N[(x + y), $MachinePrecision] - N[(N[(N[(z - t), $MachinePrecision] * y), $MachinePrecision] / N[(a - t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(x + N[(y * N[(N[(z - t), $MachinePrecision] / N[(t - a), $MachinePrecision]), $MachinePrecision] + y), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[a, -1e-112], t$95$1, If[LessEqual[a, 1.775387927039081e-67], N[(x + N[(z / N[(N[(t - a), $MachinePrecision] / y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]
\left(x + y\right) - \frac{\left(z - t\right) \cdot y}{a - t}
\begin{array}{l}
t_1 := x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)\\
\mathbf{if}\;a \leq -1 \cdot 10^{-112}:\\
\;\;\;\;t_1\\

\mathbf{elif}\;a \leq 1.775387927039081 \cdot 10^{-67}:\\
\;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\

\mathbf{else}:\\
\;\;\;\;t_1\\


\end{array}

Error

Target

Original15.8
Target8.0
Herbie5.6
\[\begin{array}{l} \mathbf{if}\;\left(x + y\right) - \frac{\left(z - t\right) \cdot y}{a - t} < -1.3664970889390727 \cdot 10^{-7}:\\ \;\;\;\;\left(y + x\right) - \left(\left(z - t\right) \cdot \frac{1}{a - t}\right) \cdot y\\ \mathbf{elif}\;\left(x + y\right) - \frac{\left(z - t\right) \cdot y}{a - t} < 1.4754293444577233 \cdot 10^{-239}:\\ \;\;\;\;\frac{y \cdot \left(a - z\right) - x \cdot t}{a - t}\\ \mathbf{else}:\\ \;\;\;\;\left(y + x\right) - \left(\left(z - t\right) \cdot \frac{1}{a - t}\right) \cdot y\\ \end{array} \]

Derivation

  1. Split input into 2 regimes
  2. if a < -9.9999999999999995e-113 or 1.775387927039081e-67 < a

    1. Initial program 14.4

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

      \[\leadsto \color{blue}{x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)} \]
      Proof
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (-.f64 t a))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 -1 (-.f64 t a))))) y)): 9 points increase in error, 1 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (-.f64 t a)) -1))) y)): 1 points increase in error, 9 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y))): 3 points increase in error, 1 points decrease in error
      (+.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 (-.f64 z t) (-.f64 a t))))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) y))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (+.f64 (neg.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))) y)): 57 points increase in error, 7 points decrease in error
      (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 x (Rewrite<= sub-neg_binary64 (-.f64 y (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))): 14 points increase in error, 1 points decrease in error

    if -9.9999999999999995e-113 < a < 1.775387927039081e-67

    1. Initial program 18.5

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

      \[\leadsto \color{blue}{x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)} \]
      Proof
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (-.f64 t a))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 -1 (-.f64 t a))))) y)): 9 points increase in error, 1 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (-.f64 t a)) -1))) y)): 1 points increase in error, 9 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t))) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (fma.f64 y (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y))): 3 points increase in error, 1 points decrease in error
      (+.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 (-.f64 z t) (-.f64 a t))))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) y))) y)): 0 points increase in error, 0 points decrease in error
      (+.f64 x (+.f64 (neg.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))) y)): 57 points increase in error, 7 points decrease in error
      (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))))): 0 points increase in error, 0 points decrease in error
      (+.f64 x (Rewrite<= sub-neg_binary64 (-.f64 y (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))): 14 points increase in error, 1 points decrease in error
    3. Taylor expanded in z around inf 7.7

      \[\leadsto x + \color{blue}{\frac{y \cdot z}{t - a}} \]
    4. Simplified7.5

      \[\leadsto x + \color{blue}{\frac{z}{t - a} \cdot y} \]
      Proof
      (*.f64 (/.f64 z (-.f64 t a)) y): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/r/_binary64 (/.f64 z (/.f64 (-.f64 t a) y))): 42 points increase in error, 52 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 z y) (-.f64 t a))): 60 points increase in error, 34 points decrease in error
      (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y z)) (-.f64 t a)): 0 points increase in error, 0 points decrease in error
    5. Applied egg-rr6.4

      \[\leadsto x + \color{blue}{\frac{z}{\frac{t - a}{y}}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification5.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -1 \cdot 10^{-112}:\\ \;\;\;\;x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)\\ \mathbf{elif}\;a \leq 1.775387927039081 \cdot 10^{-67}:\\ \;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\ \mathbf{else}:\\ \;\;\;\;x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)\\ \end{array} \]

Alternatives

Alternative 1
Error5.6
Cost1096
\[\begin{array}{l} t_1 := x + \left(y + \frac{y}{\frac{t - a}{z - t}}\right)\\ \mathbf{if}\;a \leq -1 \cdot 10^{-112}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;a \leq 1.775387927039081 \cdot 10^{-67}:\\ \;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 2
Error13.1
Cost840
\[\begin{array}{l} \mathbf{if}\;a \leq -0.0033007227874441427:\\ \;\;\;\;x + y\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + \frac{z - a}{\frac{t}{y}}\\ \mathbf{else}:\\ \;\;\;\;x + y\\ \end{array} \]
Alternative 3
Error10.9
Cost840
\[\begin{array}{l} t_1 := \left(x + y\right) - z \cdot \frac{y}{a}\\ \mathbf{if}\;a \leq -0.0033007227874441427:\\ \;\;\;\;t_1\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + \frac{z - a}{\frac{t}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 4
Error8.8
Cost840
\[\begin{array}{l} t_1 := \left(x + y\right) - z \cdot \frac{y}{a}\\ \mathbf{if}\;a \leq -6.185221678103034 \cdot 10^{+63}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 5
Error8.5
Cost840
\[\begin{array}{l} t_1 := \left(x + y\right) - y \cdot \frac{z}{a}\\ \mathbf{if}\;a \leq -6.185221678103034 \cdot 10^{+63}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + \frac{z}{\frac{t - a}{y}}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 6
Error14.1
Cost712
\[\begin{array}{l} \mathbf{if}\;a \leq -9.795506314085126 \cdot 10^{-28}:\\ \;\;\;\;x + y\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + y \cdot \frac{z}{t}\\ \mathbf{else}:\\ \;\;\;\;x + y\\ \end{array} \]
Alternative 7
Error14.1
Cost712
\[\begin{array}{l} \mathbf{if}\;a \leq -9.795506314085126 \cdot 10^{-28}:\\ \;\;\;\;x + y\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x + z \cdot \frac{y}{t}\\ \mathbf{else}:\\ \;\;\;\;x + y\\ \end{array} \]
Alternative 8
Error27.6
Cost592
\[\begin{array}{l} \mathbf{if}\;y \leq -1.9 \cdot 10^{+129}:\\ \;\;\;\;y\\ \mathbf{elif}\;y \leq 1.9297028493595222 \cdot 10^{+63}:\\ \;\;\;\;x\\ \mathbf{elif}\;y \leq 2.6 \cdot 10^{+249}:\\ \;\;\;\;y\\ \mathbf{elif}\;y \leq 3.5 \cdot 10^{+291}:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;y\\ \end{array} \]
Alternative 9
Error19.9
Cost456
\[\begin{array}{l} \mathbf{if}\;a \leq -3.6626450995537563 \cdot 10^{-20}:\\ \;\;\;\;x + y\\ \mathbf{elif}\;a \leq 3.399079661379045 \cdot 10^{+31}:\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;x + y\\ \end{array} \]
Alternative 10
Error51.0
Cost64
\[y \]

Error

Reproduce

herbie shell --seed 2022308 
(FPCore (x y z t a)
  :name "Graphics.Rendering.Plot.Render.Plot.Axis:renderAxisTick from plot-0.2.3.4, B"
  :precision binary64

  :herbie-target
  (if (< (- (+ x y) (/ (* (- z t) y) (- a t))) -1.3664970889390727e-7) (- (+ y x) (* (* (- z t) (/ 1.0 (- a t))) y)) (if (< (- (+ x y) (/ (* (- z t) y) (- a t))) 1.4754293444577233e-239) (/ (- (* y (- a z)) (* x t)) (- a t)) (- (+ y x) (* (* (- z t) (/ 1.0 (- a t))) y))))

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