Average Error: 6.3 → 2.5
Time: 32.6s
Precision: binary64
Cost: 20360
\[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]
↓
\[\begin{array}{l} t_1 := 2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), c \cdot \left(-i\right), x \cdot y\right)\right)\\ \mathbf{if}\;c \leq 2.3 \cdot 10^{+57}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;c \leq 2.8 \cdot 10^{+237}:\\ \;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
(FPCore (x y z t a b c i)
 :precision binary64
 (* 2.0 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))
↓
(FPCore (x y z t a b c i)
 :precision binary64
 (let* ((t_1 (* 2.0 (fma z t (fma (fma b c a) (* c (- i)) (* x y))))))
   (if (<= c 2.3e+57)
     t_1
     (if (<= c 2.8e+237)
       (* 2.0 (- (+ (* z t) (* x y)) (* c (* c (* b i)))))
       t_1))))
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	return 2.0 * (((x * y) + (z * t)) - (((a + (b * c)) * c) * i));
}
↓
double code(double x, double y, double z, double t, double a, double b, double c, double i) {
	double t_1 = 2.0 * fma(z, t, fma(fma(b, c, a), (c * -i), (x * y)));
	double tmp;
	if (c <= 2.3e+57) {
		tmp = t_1;
	} else if (c <= 2.8e+237) {
		tmp = 2.0 * (((z * t) + (x * y)) - (c * (c * (b * i))));
	} else {
		tmp = t_1;
	}
	return tmp;
}

function code(x, y, z, t, a, b, c, i)
	return Float64(2.0 * Float64(Float64(Float64(x * y) + Float64(z * t)) - Float64(Float64(Float64(a + Float64(b * c)) * c) * i)))
end
↓
function code(x, y, z, t, a, b, c, i)
	t_1 = Float64(2.0 * fma(z, t, fma(fma(b, c, a), Float64(c * Float64(-i)), Float64(x * y))))
	tmp = 0.0
	if (c <= 2.3e+57)
		tmp = t_1;
	elseif (c <= 2.8e+237)
		tmp = Float64(2.0 * Float64(Float64(Float64(z * t) + Float64(x * y)) - Float64(c * Float64(c * Float64(b * i)))));
	else
		tmp = t_1;
	end
	return tmp
end

code[x_, y_, z_, t_, a_, b_, c_, i_] := N[(2.0 * N[(N[(N[(x * y), $MachinePrecision] + N[(z * t), $MachinePrecision]), $MachinePrecision] - N[(N[(N[(a + N[(b * c), $MachinePrecision]), $MachinePrecision] * c), $MachinePrecision] * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
↓
code[x_, y_, z_, t_, a_, b_, c_, i_] := Block[{t$95$1 = N[(2.0 * N[(z * t + N[(N[(b * c + a), $MachinePrecision] * N[(c * (-i)), $MachinePrecision] + N[(x * y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[c, 2.3e+57], t$95$1, If[LessEqual[c, 2.8e+237], N[(2.0 * N[(N[(N[(z * t), $MachinePrecision] + N[(x * y), $MachinePrecision]), $MachinePrecision] - N[(c * N[(c * N[(b * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], t$95$1]]]

2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)
↓
\begin{array}{l}
t_1 := 2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), c \cdot \left(-i\right), x \cdot y\right)\right)\\
\mathbf{if}\;c \leq 2.3 \cdot 10^{+57}:\\
\;\;\;\;t_1\\

\mathbf{elif}\;c \leq 2.8 \cdot 10^{+237}:\\
\;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\

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


\end{array}

Error

Target

Original6.3
Target1.8
Herbie2.5
\[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(a + b \cdot c\right) \cdot \left(c \cdot i\right)\right) \]

Derivation

  1. Split input into 2 regimes

  2. if c < 2.2999999999999999e57 or 2.79999999999999983e237 < c

    1. Initial program 4.5

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]

    2. Simplified1.3

      \[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), i \cdot \left(-c\right), x \cdot y\right)\right)} \]
      Proof
      (*.f64 2 (fma.f64 z t (fma.f64 (fma.f64 b c a) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 b c) a)) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 1 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (*.f64 b c))) (*.f64 i (neg.f64 c)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (fma.f64 (+.f64 a (*.f64 b c)) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 i c))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (fma.f64 (+.f64 a (*.f64 b c)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 c i))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 a (*.f64 b c)) (neg.f64 (*.f64 c i))) (*.f64 x y))))): 1 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (+.f64 a (*.f64 b c)) (*.f64 c i)))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (+.f64 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))) (*.f64 x y)))): 35 points increase in error, 9 points decrease in error
      (*.f64 2 (fma.f64 z t (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (Rewrite=> associate-+l-_binary64 (-.f64 0 (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (fma.f64 z t (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y)))))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 z t) (-.f64 (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i) (*.f64 x y))))): 3 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 (*.f64 z t) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)) (*.f64 x y)))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x y) (-.f64 (*.f64 z t) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i))))): 0 points increase in error, 0 points decrease in error
      (*.f64 2 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (*.f64 x y) (*.f64 z t)) (*.f64 (*.f64 (+.f64 a (*.f64 b c)) c) i)))): 0 points increase in error, 0 points decrease in error

    if 2.2999999999999999e57 < c < 2.79999999999999983e237

    1. Initial program 23.7

      \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right) \]

    2. Taylor expanded in a around 0 29.9

      \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{{c}^{2} \cdot \left(i \cdot b\right)}\right) \]

    3. Simplified14.1

      \[\leadsto 2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \color{blue}{c \cdot \left(c \cdot \left(i \cdot b\right)\right)}\right) \]
      Proof
      (*.f64 c (*.f64 c (*.f64 i b))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 c c) (*.f64 i b))): 60 points increase in error, 15 points decrease in error
      (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 i b)): 0 points increase in error, 0 points decrease in error
  3. Recombined 2 regimes into one program.

  4. Final simplification2.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;c \leq 2.3 \cdot 10^{+57}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), c \cdot \left(-i\right), x \cdot y\right)\right)\\ \mathbf{elif}\;c \leq 2.8 \cdot 10^{+237}:\\ \;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(z, t, \mathsf{fma}\left(\mathsf{fma}\left(b, c, a\right), c \cdot \left(-i\right), x \cdot y\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Error7.3
Cost3664
\[\begin{array}{l} t_1 := z \cdot t + x \cdot y\\ t_2 := 2 \cdot \left(t_1 - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ t_3 := i \cdot \left(c \cdot \left(a + c \cdot b\right)\right)\\ \mathbf{if}\;t_3 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_3 \leq -2 \cdot 10^{+121}:\\ \;\;\;\;2 \cdot \left(z \cdot t - t_3\right)\\ \mathbf{elif}\;t_3 \leq 4 \cdot 10^{+76}:\\ \;\;\;\;2 \cdot \left(t_1 - c \cdot \left(a \cdot i\right)\right)\\ \mathbf{elif}\;t_3 \leq 10^{+301}:\\ \;\;\;\;2 \cdot \left(x \cdot y - t_3\right)\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]
Alternative 2
Error7.7
Cost3536
\[\begin{array}{l} t_1 := 2 \cdot \left(x \cdot y - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ t_2 := i \cdot \left(c \cdot \left(a + c \cdot b\right)\right)\\ t_3 := 2 \cdot \left(x \cdot y - t_2\right)\\ \mathbf{if}\;t_2 \leq -\infty:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_2 \leq -4 \cdot 10^{+99}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;t_2 \leq 4 \cdot 10^{+76}:\\ \;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(a \cdot i\right)\right)\\ \mathbf{elif}\;t_2 \leq 10^{+301}:\\ \;\;\;\;t_3\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 3
Error8.0
Cost3536
\[\begin{array}{l} t_1 := 2 \cdot \left(x \cdot y - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ t_2 := i \cdot \left(c \cdot \left(a + c \cdot b\right)\right)\\ \mathbf{if}\;t_2 \leq -\infty:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t_2 \leq -2 \cdot 10^{+121}:\\ \;\;\;\;2 \cdot \left(z \cdot t - t_2\right)\\ \mathbf{elif}\;t_2 \leq 4 \cdot 10^{+76}:\\ \;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(a \cdot i\right)\right)\\ \mathbf{elif}\;t_2 \leq 10^{+301}:\\ \;\;\;\;2 \cdot \left(x \cdot y - t_2\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 4
Error2.5
Cost2376
\[\begin{array}{l} t_1 := z \cdot t + x \cdot y\\ t_2 := 2 \cdot \left(t_1 - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ t_3 := c \cdot \left(a + c \cdot b\right)\\ \mathbf{if}\;t_3 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_3 \leq 5 \cdot 10^{+263}:\\ \;\;\;\;2 \cdot \left(t_1 - i \cdot \left(c \cdot \left(c \cdot b\right) + c \cdot a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]
Alternative 5
Error2.5
Cost2248
\[\begin{array}{l} t_1 := z \cdot t + x \cdot y\\ t_2 := 2 \cdot \left(t_1 - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ t_3 := c \cdot \left(a + c \cdot b\right)\\ \mathbf{if}\;t_3 \leq -\infty:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t_3 \leq 5 \cdot 10^{+263}:\\ \;\;\;\;2 \cdot \left(t_1 - i \cdot t_3\right)\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]
Alternative 6
Error18.8
Cost1612
\[\begin{array}{l} t_1 := 2 \cdot \left(z \cdot t + x \cdot y\right)\\ \mathbf{if}\;z \cdot t \leq -1 \cdot 10^{-31}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \cdot t \leq 2 \cdot 10^{-287}:\\ \;\;\;\;2 \cdot \left(x \cdot y - i \cdot \left(c \cdot a\right)\right)\\ \mathbf{elif}\;z \cdot t \leq 10^{-72}:\\ \;\;\;\;2 \cdot \left(x \cdot y - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 7
Error17.9
Cost1224
\[\begin{array}{l} t_1 := 2 \cdot \left(z \cdot t + x \cdot y\right)\\ \mathbf{if}\;z \cdot t \leq -1 \cdot 10^{-31}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;z \cdot t \leq 2 \cdot 10^{-80}:\\ \;\;\;\;2 \cdot \left(x \cdot y - i \cdot \left(c \cdot a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 8
Error14.8
Cost1092
\[\begin{array}{l} \mathbf{if}\;c \leq 3.4 \cdot 10^{+17}:\\ \;\;\;\;2 \cdot \left(\left(z \cdot t + x \cdot y\right) - c \cdot \left(a \cdot i\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \left(z \cdot t - c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right)\\ \end{array} \]
Alternative 9
Error23.5
Cost972
\[\begin{array}{l} t_1 := \left(c \cdot \left(c \cdot \left(b \cdot i\right)\right)\right) \cdot -2\\ t_2 := 2 \cdot \left(z \cdot t + x \cdot y\right)\\ \mathbf{if}\;c \leq -1.6 \cdot 10^{+153}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;c \leq -3.4 \cdot 10^{+91}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;c \leq 1.12 \cdot 10^{+30}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 10
Error37.7
Cost848
\[\begin{array}{l} t_1 := 2 \cdot \left(x \cdot y\right)\\ t_2 := 2 \cdot \left(z \cdot t\right)\\ \mathbf{if}\;t \leq -2.6045011846734606 \cdot 10^{-166}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq 4.7 \cdot 10^{+95}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 10^{+215}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq 4.5 \cdot 10^{+227}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array} \]
Alternative 11
Error23.2
Cost708
\[\begin{array}{l} \mathbf{if}\;c \leq 1.12 \cdot 10^{+30}:\\ \;\;\;\;2 \cdot \left(z \cdot t + x \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;-2 \cdot \left(c \cdot \left(b \cdot \left(c \cdot i\right)\right)\right)\\ \end{array} \]
Alternative 12
Error23.0
Cost576
\[2 \cdot \left(z \cdot t + x \cdot y\right) \]
Alternative 13
Error43.1
Cost320
\[2 \cdot \left(x \cdot y\right) \]

Error

Reproduce

herbie shell --seed 2022318 
(FPCore (x y z t a b c i)
  :name "Diagrams.ThreeD.Shapes:frustum from diagrams-lib-1.3.0.3, A"
  :precision binary64

  :herbie-target
  (* 2.0 (- (+ (* x y) (* z t)) (* (+ a (* b c)) (* c i))))

  (* 2.0 (- (+ (* x y) (* z t)) (* (* (+ a (* b c)) c) i))))