| Alternative 1 | |
|---|---|
| Accuracy | 99.7% |
| Cost | 2372 |

(FPCore (x.re x.im) :precision binary64 (- (* (- (* x.re x.re) (* x.im x.im)) x.re) (* (+ (* x.re x.im) (* x.im x.re)) x.im)))
(FPCore (x.re x.im)
:precision binary64
(let* ((t_0 (* (+ x.re x.im) (* x.re (- x.re x.im)))))
(if (<=
(-
(* x.re (- (* x.re x.re) (* x.im x.im)))
(* x.im (+ (* x.re x.im) (* x.re x.im))))
INFINITY)
(- t_0 (* x.im (* x.im (+ x.re x.re))))
t_0)))double code(double x_46_re, double x_46_im) {
return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
double code(double x_46_re, double x_46_im) {
double t_0 = (x_46_re + x_46_im) * (x_46_re * (x_46_re - x_46_im));
double tmp;
if (((x_46_re * ((x_46_re * x_46_re) - (x_46_im * x_46_im))) - (x_46_im * ((x_46_re * x_46_im) + (x_46_re * x_46_im)))) <= ((double) INFINITY)) {
tmp = t_0 - (x_46_im * (x_46_im * (x_46_re + x_46_re)));
} else {
tmp = t_0;
}
return tmp;
}
public static double code(double x_46_re, double x_46_im) {
return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im);
}
public static double code(double x_46_re, double x_46_im) {
double t_0 = (x_46_re + x_46_im) * (x_46_re * (x_46_re - x_46_im));
double tmp;
if (((x_46_re * ((x_46_re * x_46_re) - (x_46_im * x_46_im))) - (x_46_im * ((x_46_re * x_46_im) + (x_46_re * x_46_im)))) <= Double.POSITIVE_INFINITY) {
tmp = t_0 - (x_46_im * (x_46_im * (x_46_re + x_46_re)));
} else {
tmp = t_0;
}
return tmp;
}
def code(x_46_re, x_46_im): return (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im)
def code(x_46_re, x_46_im): t_0 = (x_46_re + x_46_im) * (x_46_re * (x_46_re - x_46_im)) tmp = 0 if ((x_46_re * ((x_46_re * x_46_re) - (x_46_im * x_46_im))) - (x_46_im * ((x_46_re * x_46_im) + (x_46_re * x_46_im)))) <= math.inf: tmp = t_0 - (x_46_im * (x_46_im * (x_46_re + x_46_re))) else: tmp = t_0 return tmp
function code(x_46_re, x_46_im) return Float64(Float64(Float64(Float64(x_46_re * x_46_re) - Float64(x_46_im * x_46_im)) * x_46_re) - Float64(Float64(Float64(x_46_re * x_46_im) + Float64(x_46_im * x_46_re)) * x_46_im)) end
function code(x_46_re, x_46_im) t_0 = Float64(Float64(x_46_re + x_46_im) * Float64(x_46_re * Float64(x_46_re - x_46_im))) tmp = 0.0 if (Float64(Float64(x_46_re * Float64(Float64(x_46_re * x_46_re) - Float64(x_46_im * x_46_im))) - Float64(x_46_im * Float64(Float64(x_46_re * x_46_im) + Float64(x_46_re * x_46_im)))) <= Inf) tmp = Float64(t_0 - Float64(x_46_im * Float64(x_46_im * Float64(x_46_re + x_46_re)))); else tmp = t_0; end return tmp end
function tmp = code(x_46_re, x_46_im) tmp = (((x_46_re * x_46_re) - (x_46_im * x_46_im)) * x_46_re) - (((x_46_re * x_46_im) + (x_46_im * x_46_re)) * x_46_im); end
function tmp_2 = code(x_46_re, x_46_im) t_0 = (x_46_re + x_46_im) * (x_46_re * (x_46_re - x_46_im)); tmp = 0.0; if (((x_46_re * ((x_46_re * x_46_re) - (x_46_im * x_46_im))) - (x_46_im * ((x_46_re * x_46_im) + (x_46_re * x_46_im)))) <= Inf) tmp = t_0 - (x_46_im * (x_46_im * (x_46_re + x_46_re))); else tmp = t_0; end tmp_2 = tmp; end
code[x$46$re_, x$46$im_] := N[(N[(N[(N[(x$46$re * x$46$re), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision] * x$46$re), $MachinePrecision] - N[(N[(N[(x$46$re * x$46$im), $MachinePrecision] + N[(x$46$im * x$46$re), $MachinePrecision]), $MachinePrecision] * x$46$im), $MachinePrecision]), $MachinePrecision]
code[x$46$re_, x$46$im_] := Block[{t$95$0 = N[(N[(x$46$re + x$46$im), $MachinePrecision] * N[(x$46$re * N[(x$46$re - x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[N[(N[(x$46$re * N[(N[(x$46$re * x$46$re), $MachinePrecision] - N[(x$46$im * x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(x$46$im * N[(N[(x$46$re * x$46$im), $MachinePrecision] + N[(x$46$re * x$46$im), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], Infinity], N[(t$95$0 - N[(x$46$im * N[(x$46$im * N[(x$46$re + x$46$re), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$0]]
\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im
\begin{array}{l}
t_0 := \left(x.re + x.im\right) \cdot \left(x.re \cdot \left(x.re - x.im\right)\right)\\
\mathbf{if}\;x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \left(x.re \cdot x.im + x.re \cdot x.im\right) \leq \infty:\\
\;\;\;\;t_0 - x.im \cdot \left(x.im \cdot \left(x.re + x.re\right)\right)\\
\mathbf{else}:\\
\;\;\;\;t_0\\
\end{array}
Herbie found 5 alternatives:
| Alternative | Accuracy | Speedup |
|---|
Results
| Original | 82.3% |
|---|---|
| Target | 86.8% |
| Herbie | 99.7% |
if (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) < +inf.0Initial program 91.8%
Simplified91.8%
[Start]91.8% | \[ \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im
\] |
|---|---|
*-commutative [=>]91.8% | \[ \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im
\] |
*-commutative [=>]91.8% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - \color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}
\] |
*-commutative [<=]91.8% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)
\] |
distribute-lft-out [=>]91.8% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right)}
\] |
Applied egg-rr99.7%
[Start]91.8% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)
\] |
|---|---|
sub-neg [=>]91.8% | \[ \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)}
\] |
*-commutative [=>]91.8% | \[ \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
difference-of-squares [=>]91.8% | \[ \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)} \cdot x.re + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
associate-*l* [=>]99.7% | \[ \color{blue}{\left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right)} + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
*-commutative [=>]99.7% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(-\color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot x.im}\right)
\] |
distribute-rgt-neg-in [=>]99.7% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \left(-x.im\right)}
\] |
distribute-rgt-in [=>]99.7% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(-x.im\right)
\] |
distribute-lft-out [=>]99.7% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(-x.im\right)
\] |
if +inf.0 < (-.f64 (*.f64 (-.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) x.re) (*.f64 (+.f64 (*.f64 x.re x.im) (*.f64 x.im x.re)) x.im)) Initial program 0.0%
Simplified0.0%
[Start]0.0% | \[ \left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im
\] |
|---|---|
*-commutative [=>]0.0% | \[ \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right)} - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im
\] |
*-commutative [=>]0.0% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - \color{blue}{x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)}
\] |
*-commutative [<=]0.0% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \left(x.re \cdot x.im + \color{blue}{x.re \cdot x.im}\right)
\] |
distribute-lft-out [=>]0.0% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right)}
\] |
Applied egg-rr23.8%
[Start]0.0% | \[ x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) - x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)
\] |
|---|---|
sub-neg [=>]0.0% | \[ \color{blue}{x.re \cdot \left(x.re \cdot x.re - x.im \cdot x.im\right) + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)}
\] |
*-commutative [=>]0.0% | \[ \color{blue}{\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re} + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
difference-of-squares [=>]23.8% | \[ \color{blue}{\left(\left(x.re + x.im\right) \cdot \left(x.re - x.im\right)\right)} \cdot x.re + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
associate-*l* [=>]23.8% | \[ \color{blue}{\left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right)} + \left(-x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)\right)
\] |
*-commutative [=>]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(-\color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot x.im}\right)
\] |
distribute-rgt-neg-in [=>]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \left(-x.im\right)}
\] |
distribute-rgt-in [=>]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(-x.im\right)
\] |
distribute-lft-out [=>]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.im \cdot \left(x.re + x.re\right)\right)} \cdot \left(-x.im\right)
\] |
Applied egg-rr100.0%
[Start]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.im \cdot \left(x.re + x.re\right)\right) \cdot \left(-x.im\right)
\] |
|---|---|
distribute-lft-in [=>]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.im \cdot x.re + x.im \cdot x.re\right)} \cdot \left(-x.im\right)
\] |
distribute-rgt-in [<=]23.8% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\left(x.re \cdot \left(x.im + x.im\right)\right)} \cdot \left(-x.im\right)
\] |
add-sqr-sqrt [=>]0.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \color{blue}{\left(\sqrt{-x.im} \cdot \sqrt{-x.im}\right)}
\] |
sqrt-unprod [=>]52.4% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \color{blue}{\sqrt{\left(-x.im\right) \cdot \left(-x.im\right)}}
\] |
sqr-neg [=>]52.4% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \sqrt{\color{blue}{x.im \cdot x.im}}
\] |
sqrt-prod [=>]52.4% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \color{blue}{\left(\sqrt{x.im} \cdot \sqrt{x.im}\right)}
\] |
add-sqr-sqrt [<=]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \color{blue}{x.im}
\] |
*-commutative [<=]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)}
\] |
add-log-exp [=>]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{\log \left(e^{x.im \cdot \left(x.re \cdot \left(x.im + x.im\right)\right)}\right)}
\] |
associate-*r* [=>]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left(e^{\color{blue}{\left(x.im \cdot x.re\right) \cdot \left(x.im + x.im\right)}}\right)
\] |
*-commutative [<=]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left(e^{\color{blue}{\left(x.re \cdot x.im\right)} \cdot \left(x.im + x.im\right)}\right)
\] |
exp-prod [=>]76.2% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \color{blue}{\left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + x.im\right)}\right)}
\] |
add-sqr-sqrt [=>]52.4% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + \color{blue}{\sqrt{x.im} \cdot \sqrt{x.im}}\right)}\right)
\] |
sqrt-prod [<=]61.9% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + \color{blue}{\sqrt{x.im \cdot x.im}}\right)}\right)
\] |
sqr-neg [<=]61.9% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + \sqrt{\color{blue}{\left(-x.im\right) \cdot \left(-x.im\right)}}\right)}\right)
\] |
sqrt-unprod [<=]14.3% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + \color{blue}{\sqrt{-x.im} \cdot \sqrt{-x.im}}\right)}\right)
\] |
add-sqr-sqrt [<=]100.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\left(x.im + \color{blue}{\left(-x.im\right)}\right)}\right)
\] |
sub-neg [<=]100.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\color{blue}{\left(x.im - x.im\right)}}\right)
\] |
+-inverses [=>]100.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \left({\left(e^{x.re \cdot x.im}\right)}^{\color{blue}{0}}\right)
\] |
metadata-eval [=>]100.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \log \color{blue}{1}
\] |
metadata-eval [=>]100.0% | \[ \left(x.re + x.im\right) \cdot \left(\left(x.re - x.im\right) \cdot x.re\right) + \color{blue}{0}
\] |
Final simplification99.7%
| Alternative 1 | |
|---|---|
| Accuracy | 99.7% |
| Cost | 2372 |
| Alternative 2 | |
|---|---|
| Accuracy | 96.3% |
| Cost | 969 |
| Alternative 3 | |
|---|---|
| Accuracy | 82.4% |
| Cost | 713 |
| Alternative 4 | |
|---|---|
| Accuracy | 82.4% |
| Cost | 713 |
| Alternative 5 | |
|---|---|
| Accuracy | 58.4% |
| Cost | 320 |
herbie shell --seed 2023165
(FPCore (x.re x.im)
:name "math.cube on complex, real part"
:precision binary64
:herbie-target
(+ (* (* x.re x.re) (- x.re x.im)) (* (* x.re x.im) (- x.re (* 3.0 x.im))))
(- (* (- (* x.re x.re) (* x.im x.im)) x.re) (* (+ (* x.re x.im) (* x.im x.re)) x.im)))