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

↓

\[0.5 \cdot \mathsf{fma}\left(\frac{z + x}{y}, x - z, y\right) \]

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

↓

(FPCore (x y z) :precision binary64 (* 0.5 (fma (/ (+ z x) y) (- x z) y)))

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

↓

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

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

↓

function code(x, y, z)
	return Float64(0.5 * fma(Float64(Float64(z + x) / y), Float64(x - z), y))
end

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

↓

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

\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}

↓

0.5 \cdot \mathsf{fma}\left(\frac{z + x}{y}, x - z, y\right)

Original	28.4
Target	0.2
Herbie	0.2

Derivation

Initial program 28.4
\[\frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2} \]
Taylor expanded in x around 0 28.5
\[\leadsto \color{blue}{0.5 \cdot \frac{{y}^{2} - {z}^{2}}{y} + 0.5 \cdot \frac{{x}^{2}}{y}} \]
Simplified0.2
\[\leadsto \color{blue}{0.5 \cdot \mathsf{fma}\left(\frac{z + x}{y}, x - z, y\right)} \]
Proof
(*.f64 1/2 (fma.f64 (/.f64 (+.f64 z x) y) (-.f64 x z) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (fma.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x z)) y) (-.f64 x z) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (+.f64 x z) y) (-.f64 x z)) y))): 2 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (+.f64 x z) (-.f64 x z)) y)) y)): 78 points increase in error, 10 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 x x) (*.f64 z z))) y) y)): 2 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 x 2)) (*.f64 z z)) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 (/.f64 (-.f64 (pow.f64 x 2) (Rewrite<= unpow2_binary64 (pow.f64 z 2))) y) y)): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (Rewrite<= +-commutative_binary64 (+.f64 y (/.f64 (-.f64 (pow.f64 x 2) (pow.f64 z 2)) y)))): 0 points increase in error, 0 points decrease in error
(*.f64 1/2 (+.f64 y (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (pow.f64 x 2) y) (/.f64 (pow.f64 z 2) y))))): 0 points increase in error, 1 points decrease in error
(*.f64 1/2 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 y (/.f64 (pow.f64 x 2) y)) (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 1/2 (+.f64 y (/.f64 (pow.f64 x 2) y))) (*.f64 1/2 (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 1/2 (+.f64 y (/.f64 (pow.f64 x 2) y))) (*.f64 (neg.f64 1/2) (/.f64 (pow.f64 z 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 1/2 y) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))) (*.f64 (neg.f64 1/2) (/.f64 (pow.f64 z 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 y) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))) (*.f64 (Rewrite=> metadata-eval -1/2) (/.f64 (pow.f64 z 2) y))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+l+_binary64 (+.f64 (*.f64 1/2 y) (+.f64 (*.f64 1/2 (/.f64 (pow.f64 x 2) y)) (*.f64 -1/2 (/.f64 (pow.f64 z 2) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 y) (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= /-rgt-identity_binary64 (/.f64 y 1))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (/.f64 y (Rewrite<= *-inverses_binary64 (/.f64 y y)))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y y) y))) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 69 points increase in error, 3 points decrease in error
(+.f64 (*.f64 1/2 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 y 2)) y)) (+.f64 (*.f64 -1/2 (/.f64 (pow.f64 z 2) y)) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 -1/2 (/.f64 (pow.f64 z 2) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 (Rewrite<= metadata-eval (*.f64 1/2 -1)) (/.f64 (pow.f64 z 2) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (Rewrite<= associate-*r*_binary64 (*.f64 1/2 (*.f64 -1 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 1/2 (/.f64 (pow.f64 y 2) y)) (*.f64 1/2 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 1/2 (+.f64 (/.f64 (pow.f64 y 2) y) (neg.f64 (/.f64 (pow.f64 z 2) y))))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 (pow.f64 y 2) y) (/.f64 (pow.f64 z 2) y)))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 1/2 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (pow.f64 y 2) (pow.f64 z 2)) y))) (*.f64 1/2 (/.f64 (pow.f64 x 2) y))): 1 points increase in error, 0 points decrease in error
Final simplification0.2
\[\leadsto 0.5 \cdot \mathsf{fma}\left(\frac{z + x}{y}, x - z, y\right) \]

Alternatives

Alternative 1
Error	3.6
Cost	5072

\[\begin{array}{l} t_0 := \frac{\left(x \cdot x + y \cdot y\right) - z \cdot z}{y \cdot 2}\\ \mathbf{if}\;t_0 \leq -\infty:\\ \;\;\;\;0.5 \cdot \left(y + \frac{x}{\frac{y}{x}}\right)\\ \mathbf{elif}\;t_0 \leq -5 \cdot 10^{-145}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;t_0 \leq 0:\\ \;\;\;\;0.5 \cdot \frac{z + x}{\frac{y}{x - z}}\\ \mathbf{elif}\;t_0 \leq 10^{+292}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot \left(y - z \cdot \frac{z}{y}\right)\\ \end{array} \]

Alternative 2
Error	23.9
Cost	1372

\[\begin{array}{l} t_0 := x \cdot \frac{x}{y \cdot 2}\\ \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -1.3 \cdot 10^{-108}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq -1.16 \cdot 10^{-144}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -8.5 \cdot 10^{-193}:\\ \;\;\;\;\left(z \cdot \frac{z}{y}\right) \cdot -0.5\\ \mathbf{elif}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 1.55 \cdot 10^{-145}:\\ \;\;\;\;\frac{z \cdot -0.5}{\frac{y}{z}}\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 3
Error	23.9
Cost	1372

\[\begin{array}{l} t_0 := x \cdot \frac{x}{y \cdot 2}\\ \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -1.3 \cdot 10^{-108}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq -1.16 \cdot 10^{-144}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -8.5 \cdot 10^{-193}:\\ \;\;\;\;\left(z \cdot z\right) \cdot \frac{-0.5}{y}\\ \mathbf{elif}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 1.55 \cdot 10^{-145}:\\ \;\;\;\;\frac{z \cdot -0.5}{\frac{y}{z}}\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 4
Error	23.9
Cost	1372

\[\begin{array}{l} t_0 := x \cdot \frac{x}{y \cdot 2}\\ \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -1.3 \cdot 10^{-108}:\\ \;\;\;\;\frac{x \cdot x}{y \cdot 2}\\ \mathbf{elif}\;y \leq -1.16 \cdot 10^{-144}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -8.5 \cdot 10^{-193}:\\ \;\;\;\;\left(z \cdot z\right) \cdot \frac{-0.5}{y}\\ \mathbf{elif}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 1.55 \cdot 10^{-145}:\\ \;\;\;\;\frac{z \cdot -0.5}{\frac{y}{z}}\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 5
Error	23.9
Cost	1372

\[\begin{array}{l} t_0 := 0.5 \cdot \frac{x}{\frac{y}{x}}\\ \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -1.3 \cdot 10^{-108}:\\ \;\;\;\;\frac{x \cdot x}{y \cdot 2}\\ \mathbf{elif}\;y \leq -1.16 \cdot 10^{-144}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -8.5 \cdot 10^{-193}:\\ \;\;\;\;\left(z \cdot z\right) \cdot \frac{-0.5}{y}\\ \mathbf{elif}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 2.75 \cdot 10^{-111}:\\ \;\;\;\;\frac{z \cdot -0.5}{\frac{y}{z}}\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 6
Error	23.8
Cost	1240

\[\begin{array}{l} t_0 := \frac{z \cdot -0.5}{\frac{y}{z}}\\ t_1 := x \cdot \frac{x}{y \cdot 2}\\ \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq -1.6 \cdot 10^{-110}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq -8.5 \cdot 10^{-193}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y \leq 1.55 \cdot 10^{-145}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 7
Error	0.2
Cost	1216

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

Alternative 8
Error	14.7
Cost	840

\[\begin{array}{l} t_0 := 0.5 \cdot \left(y + \frac{x}{\frac{y}{x}}\right)\\ \mathbf{if}\;y \leq -4.5 \cdot 10^{-255}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;y \leq 2.75 \cdot 10^{-111}:\\ \;\;\;\;\frac{z \cdot -0.5}{\frac{y}{z}}\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 9
Error	6.7
Cost	840

\[\begin{array}{l} t_0 := 0.5 \cdot \left(y + \frac{x}{\frac{y}{x}}\right)\\ \mathbf{if}\;x \leq -9.706732940781171 \cdot 10^{-114}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x \leq 5.795254299163547 \cdot 10^{-37}:\\ \;\;\;\;0.5 \cdot \left(y - z \cdot \frac{z}{y}\right)\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 10
Error	23.7
Cost	712

\[\begin{array}{l} \mathbf{if}\;y \leq -3.2 \cdot 10^{-22}:\\ \;\;\;\;0.5 \cdot y\\ \mathbf{elif}\;y \leq 9.6 \cdot 10^{+27}:\\ \;\;\;\;x \cdot \frac{x}{y \cdot 2}\\ \mathbf{else}:\\ \;\;\;\;0.5 \cdot y\\ \end{array} \]

Alternative 11
Error	27.1
Cost	192

\[0.5 \cdot y \]

Error

Target

Derivation

Alternatives

Error

Reproduce