Numeric.SpecFunctions:invErfc from math-functions-0.1.5.2, A

Average Error: 2.8 → 0.0

Time: 13.3s

Precision: binary64

Cost: 13376

Math

\[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]

↓

\[x + \frac{-1}{\mathsf{fma}\left(e^{z}, \frac{-1.1283791670955126}{y}, x\right)} \]

FPCore

(FPCore (x y z)
 :precision binary64
 (+ x (/ y (- (* 1.1283791670955126 (exp z)) (* x y)))))

↓

(FPCore (x y z)
 :precision binary64
 (+ x (/ -1.0 (fma (exp z) (/ -1.1283791670955126 y) x))))

C

double code(double x, double y, double z) {
	return x + (y / ((1.1283791670955126 * exp(z)) - (x * y)));
}

↓

double code(double x, double y, double z) {
	return x + (-1.0 / fma(exp(z), (-1.1283791670955126 / y), x));
}

Julia

function code(x, y, z)
	return Float64(x + Float64(y / Float64(Float64(1.1283791670955126 * exp(z)) - Float64(x * y))))
end

↓

function code(x, y, z)
	return Float64(x + Float64(-1.0 / fma(exp(z), Float64(-1.1283791670955126 / y), x)))
end

Wolfram

code[x_, y_, z_] := N[(x + N[(y / N[(N[(1.1283791670955126 * N[Exp[z], $MachinePrecision]), $MachinePrecision] - N[(x * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[x_, y_, z_] := N[(x + N[(-1.0 / N[(N[Exp[z], $MachinePrecision] * N[(-1.1283791670955126 / y), $MachinePrecision] + x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

Target

Original	2.8
Target	0.1
Herbie	0.0

\[x + \frac{1}{\frac{1.1283791670955126}{y} \cdot e^{z} - x} \]

Derivation

1. Initial program 2.8

   \[x + \frac{y}{1.1283791670955126 \cdot e^{z} - x \cdot y} \]

2. Simplified 0.0

   \[\leadsto \color{blue}{x + \frac{-1}{\mathsf{fma}\left(e^{z}, \frac{-1.1283791670955126}{y}, x\right)}} \]
   Proof
   (+.f64 x (/.f64 -1 (fma.f64 (exp.f64 z) (/.f64 -5641895835477563/5000000000000000 y) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (fma.f64 (exp.f64 z) (/.f64 (Rewrite<= metadata-eval (/.f64 5641895835477563/5000000000000000 -1)) y) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (fma.f64 (exp.f64 z) (Rewrite<= associate-/r*_binary64 (/.f64 5641895835477563/5000000000000000 (*.f64 -1 y))) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (fma.f64 (exp.f64 z) (/.f64 5641895835477563/5000000000000000 (Rewrite<= neg-mul-1_binary64 (neg.f64 y))) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (exp.f64 z) (/.f64 5641895835477563/5000000000000000 (neg.f64 y))) x)))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 5641895835477563/5000000000000000 (neg.f64 y)) (exp.f64 z))) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (*.f64 (/.f64 5641895835477563/5000000000000000 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y))) (exp.f64 z)) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (*.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 5641895835477563/5000000000000000 -1) y)) (exp.f64 z)) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (*.f64 (/.f64 (Rewrite=> metadata-eval -5641895835477563/5000000000000000) y) (exp.f64 z)) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (*.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 5641895835477563/5000000000000000)) y) (exp.f64 z)) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (neg.f64 5641895835477563/5000000000000000) (/.f64 y (exp.f64 z)))) x))): 35 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (neg.f64 5641895835477563/5000000000000000) (exp.f64 z)) y)) x))): 0 points increase in error, 35 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (/.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))) y) x))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (+.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 x)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (neg.f64 x))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite<= *-rgt-identity_binary64 (*.f64 (neg.f64 x) 1))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (neg.f64 x) (Rewrite<= *-inverses_binary64 (/.f64 (neg.f64 y) (neg.f64 y))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (neg.f64 x) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y)) (neg.f64 y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (neg.f64 x) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 y -1)) (neg.f64 y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (neg.f64 x) (Rewrite<= associate-*r/_binary64 (*.f64 y (/.f64 -1 (neg.f64 y)))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (neg.f64 x) y) (/.f64 -1 (neg.f64 y))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 x y))) (/.f64 -1 (neg.f64 y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (neg.f64 (*.f64 x y)) -1) (neg.f64 y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (/.f64 (*.f64 (neg.f64 (*.f64 x y)) -1) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y)))))): 55 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 -1 (neg.f64 (*.f64 x y)))) (*.f64 -1 y))))): 0 points increase in error, 54 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (neg.f64 (*.f64 x y)) y)))))): 0 points increase in error, 1 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (neg.f64 (*.f64 x y)) y))))): 20 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (-.f64 (/.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) y) (Rewrite=> *-lft-identity_binary64 (/.f64 (neg.f64 (*.f64 x y)) y))))): 35 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) (neg.f64 (*.f64 x y))) y)))): 0 points increase in error, 35 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (-.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 x) y))) y))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (Rewrite=> cancel-sign-sub_binary64 (+.f64 (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) (*.f64 x y))) y))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x y) (neg.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))) y))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))) y))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (Rewrite<= --rgt-identity_binary64 (-.f64 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))) 0)) y))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 -1 (/.f64 (Rewrite=> --rgt-identity_binary64 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))) y))): 3 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 y) (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))))): 0 points increase in error, 3 points decrease in error
   (+.f64 x (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 y (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (*.f64 (Rewrite<= metadata-eval (/.f64 1 -1)) (/.f64 y (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (*.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) -1) (/.f64 y (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))))): 55 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (neg.f64 -1) y) (*.f64 -1 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))))): 0 points increase in error, 35 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))))): 0 points increase in error, 20 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 (*.f64 x y) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 (*.f64 x y)) (*.f64 5641895835477563/5000000000000000 (exp.f64 z)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (*.f64 x y))) (*.f64 5641895835477563/5000000000000000 (exp.f64 z))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (neg.f64 (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (/.f64 (*.f64 (neg.f64 -1) y) (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= associate-*r/_binary64 (*.f64 (neg.f64 -1) (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (*.f64 (neg.f64 -1) (Rewrite<= +-lft-identity_binary64 (+.f64 0 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 -1 (+.f64 0 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (neg.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (+.f64 0 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (neg.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (+.f64 0 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))))))): 0 points increase in error, 0 points decrease in error
   (+.f64 x (neg.f64 (-.f64 0 (Rewrite=> +-lft-identity_binary64 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y))))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= sub-neg_binary64 (-.f64 x (-.f64 0 (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 x 0) (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y))))): 0 points increase in error, 0 points decrease in error
   (+.f64 (Rewrite=> --rgt-identity_binary64 x) (/.f64 y (-.f64 (*.f64 5641895835477563/5000000000000000 (exp.f64 z)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error

3. Final simplification 0.0

   \[\leadsto x + \frac{-1}{\mathsf{fma}\left(e^{z}, \frac{-1.1283791670955126}{y}, x\right)} \]

Alternatives

Alternative 1
Error	0.1
Cost	20168

\[\begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;x - \frac{1}{x}\\ \mathbf{elif}\;e^{z} \leq 2:\\ \;\;\;\;x + \frac{y}{e^{z} \cdot 1.1283791670955126 - x \cdot y}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 2
Error	0.2
Cost	14152

\[\begin{array}{l} \mathbf{if}\;e^{z} \leq 0:\\ \;\;\;\;x - \frac{1}{x}\\ \mathbf{elif}\;e^{z} \leq 2:\\ \;\;\;\;x + \frac{-1}{\left(x + -1.1283791670955126 \cdot \frac{z}{y}\right) + -1.1283791670955126 \cdot \frac{1}{y}}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 3
Error	8.6
Cost	1104

\[\begin{array}{l} t_0 := x - \frac{1}{x}\\ t_1 := x + 0.8862269254527579 \cdot \left(y - z \cdot y\right)\\ \mathbf{if}\;z \leq -0.0245:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 1.34 \cdot 10^{-154}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq 3.2 \cdot 10^{-86}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 0.195:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 4
Error	8.6
Cost	1104

\[\begin{array}{l} t_0 := x - \frac{1}{x}\\ \mathbf{if}\;z \leq -0.0025:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 2 \cdot 10^{-154}:\\ \;\;\;\;x + 0.8862269254527579 \cdot \left(y - z \cdot y\right)\\ \mathbf{elif}\;z \leq 4 \cdot 10^{-78}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 0.18:\\ \;\;\;\;x + y \cdot \left(0.8862269254527579 \cdot \left(1 - z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 5
Error	0.3
Cost	1096

\[\begin{array}{l} \mathbf{if}\;z \leq -280000000000:\\ \;\;\;\;x - \frac{1}{x}\\ \mathbf{elif}\;z \leq 25:\\ \;\;\;\;x + \frac{y}{\left(1.1283791670955126 + z \cdot 1.1283791670955126\right) - x \cdot y}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 6
Error	8.7
Cost	848

\[\begin{array}{l} t_0 := x - \frac{1}{x}\\ t_1 := x + y \cdot 0.8862269254527579\\ \mathbf{if}\;z \leq -0.0061:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 7.2 \cdot 10^{-155}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \leq 1.2 \cdot 10^{-81}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;z \leq 0.18:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 7
Error	0.4
Cost	840

\[\begin{array}{l} \mathbf{if}\;z \leq -280000000000:\\ \;\;\;\;x - \frac{1}{x}\\ \mathbf{elif}\;z \leq 25:\\ \;\;\;\;x + \frac{y}{1.1283791670955126 - x \cdot y}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 8
Error	0.4
Cost	840

\[\begin{array}{l} \mathbf{if}\;z \leq -280000000000:\\ \;\;\;\;x - \frac{1}{x}\\ \mathbf{elif}\;z \leq 25:\\ \;\;\;\;x + \frac{-1}{x + \frac{-1.1283791670955126}{y}}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 9
Error	15.8
Cost	584

\[\begin{array}{l} \mathbf{if}\;z \leq -0.005:\\ \;\;\;\;x\\ \mathbf{elif}\;z \leq 0.19:\\ \;\;\;\;x + \frac{y}{1.1283791670955126}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 10
Error	15.8
Cost	584

\[\begin{array}{l} \mathbf{if}\;z \leq -1.85:\\ \;\;\;\;x\\ \mathbf{elif}\;z \leq 0.225:\\ \;\;\;\;x + y \cdot 0.8862269254527579\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 11
Error	18.7
Cost	456

\[\begin{array}{l} \mathbf{if}\;x \leq -3.2 \cdot 10^{-149}:\\ \;\;\;\;x\\ \mathbf{elif}\;x \leq 7.5 \cdot 10^{-255}:\\ \;\;\;\;y \cdot 0.8862269254527579\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

Alternative 12
Error	19.9
Cost	64

\[x \]

Reproduce

herbie shell --seed 2022343 
(FPCore (x y z)
  :name "Numeric.SpecFunctions:invErfc from math-functions-0.1.5.2, A"
  :precision binary64

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

  (+ x (/ y (- (* 1.1283791670955126 (exp z)) (* x y)))))