expfmod (used to be hard to sample)

Percentage Accurate: 6.6% → 99.2%
Time: 9.9s
Alternatives: 3
Speedup: 4.1×

Specification

?
\[\begin{array}{l} \\ \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \end{array} \]
(FPCore (x) :precision binary64 (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))
double code(double x) {
	return fmod(exp(x), sqrt(cos(x))) * exp(-x);
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = mod(exp(x), sqrt(cos(x))) * exp(-x)
end function
def code(x):
	return math.fmod(math.exp(x), math.sqrt(math.cos(x))) * math.exp(-x)
function code(x)
	return Float64(rem(exp(x), sqrt(cos(x))) * exp(Float64(-x)))
end
code[x_] := N[(N[With[{TMP1 = N[Exp[x], $MachinePrecision], TMP2 = N[Sqrt[N[Cos[x], $MachinePrecision]], $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[Exp[(-x)], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}
\end{array}

Sampling outcomes in binary64 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 3 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 6.6% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \end{array} \]
(FPCore (x) :precision binary64 (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))
double code(double x) {
	return fmod(exp(x), sqrt(cos(x))) * exp(-x);
}
real(8) function code(x)
    real(8), intent (in) :: x
    code = mod(exp(x), sqrt(cos(x))) * exp(-x)
end function
def code(x):
	return math.fmod(math.exp(x), math.sqrt(math.cos(x))) * math.exp(-x)
function code(x)
	return Float64(rem(exp(x), sqrt(cos(x))) * exp(Float64(-x)))
end
code[x_] := N[(N[With[{TMP1 = N[Exp[x], $MachinePrecision], TMP2 = N[Sqrt[N[Cos[x], $MachinePrecision]], $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * N[Exp[(-x)], $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}
\end{array}

Alternative 1: 99.2% accurate, 0.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_0 := \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right)\\ t_1 := e^{-x}\\ \mathbf{if}\;x \leq -1 \cdot 10^{-309}:\\ \;\;\;\;{\left({\left(e^{x \cdot x - {t\_0}^{2}}\right)}^{\left({\left(t\_0 + x\right)}^{-1}\right)}\right)}^{-1}\\ \mathbf{elif}\;x \leq 0.2:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot t\_1\\ \mathbf{else}:\\ \;\;\;\;t\_1\\ \end{array} \end{array} \]
(FPCore (x)
 :precision binary64
 (let* ((t_0 (log (fmod (exp x) (fma (* -0.25 x) x 1.0)))) (t_1 (exp (- x))))
   (if (<= x -1e-309)
     (pow (pow (exp (- (* x x) (pow t_0 2.0))) (pow (+ t_0 x) -1.0)) -1.0)
     (if (<= x 0.2)
       (* (fmod (* (fma 0.5 x 1.0) x) (fma -0.25 (* x x) 1.0)) t_1)
       t_1))))
double code(double x) {
	double t_0 = log(fmod(exp(x), fma((-0.25 * x), x, 1.0)));
	double t_1 = exp(-x);
	double tmp;
	if (x <= -1e-309) {
		tmp = pow(pow(exp(((x * x) - pow(t_0, 2.0))), pow((t_0 + x), -1.0)), -1.0);
	} else if (x <= 0.2) {
		tmp = fmod((fma(0.5, x, 1.0) * x), fma(-0.25, (x * x), 1.0)) * t_1;
	} else {
		tmp = t_1;
	}
	return tmp;
}
function code(x)
	t_0 = log(rem(exp(x), fma(Float64(-0.25 * x), x, 1.0)))
	t_1 = exp(Float64(-x))
	tmp = 0.0
	if (x <= -1e-309)
		tmp = (exp(Float64(Float64(x * x) - (t_0 ^ 2.0))) ^ (Float64(t_0 + x) ^ -1.0)) ^ -1.0;
	elseif (x <= 0.2)
		tmp = Float64(rem(Float64(fma(0.5, x, 1.0) * x), fma(-0.25, Float64(x * x), 1.0)) * t_1);
	else
		tmp = t_1;
	end
	return tmp
end
code[x_] := Block[{t$95$0 = N[Log[N[With[{TMP1 = N[Exp[x], $MachinePrecision], TMP2 = N[(N[(-0.25 * x), $MachinePrecision] * x + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision]], $MachinePrecision]}, Block[{t$95$1 = N[Exp[(-x)], $MachinePrecision]}, If[LessEqual[x, -1e-309], N[Power[N[Power[N[Exp[N[(N[(x * x), $MachinePrecision] - N[Power[t$95$0, 2.0], $MachinePrecision]), $MachinePrecision]], $MachinePrecision], N[Power[N[(t$95$0 + x), $MachinePrecision], -1.0], $MachinePrecision]], $MachinePrecision], -1.0], $MachinePrecision], If[LessEqual[x, 0.2], N[(N[With[{TMP1 = N[(N[(0.5 * x + 1.0), $MachinePrecision] * x), $MachinePrecision], TMP2 = N[(-0.25 * N[(x * x), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * t$95$1), $MachinePrecision], t$95$1]]]]
\begin{array}{l}

\\
\begin{array}{l}
t_0 := \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right)\\
t_1 := e^{-x}\\
\mathbf{if}\;x \leq -1 \cdot 10^{-309}:\\
\;\;\;\;{\left({\left(e^{x \cdot x - {t\_0}^{2}}\right)}^{\left({\left(t\_0 + x\right)}^{-1}\right)}\right)}^{-1}\\

\mathbf{elif}\;x \leq 0.2:\\
\;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot t\_1\\

\mathbf{else}:\\
\;\;\;\;t\_1\\


\end{array}
\end{array}
Derivation
  1. Split input into 3 regimes
  2. if x < -1.000000000000002e-309

    1. Initial program 10.6%

      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}} \]
      2. lift-exp.f64N/A

        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{e^{-x}} \]
      3. lift-neg.f64N/A

        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
      4. exp-negN/A

        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
      5. lift-exp.f64N/A

        \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \frac{1}{\color{blue}{e^{x}}} \]
      6. un-div-invN/A

        \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
      7. lower-/.f6410.6

        \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
    4. Applied rewrites10.6%

      \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
    5. Taylor expanded in x around 0

      \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right)}{e^{x}} \]
    6. Step-by-step derivation
      1. +-commutativeN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right)}{e^{x}} \]
      2. metadata-evalN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      3. metadata-evalN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      4. lft-mult-inverseN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      5. distribute-rgt-neg-outN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      6. mul-1-negN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      7. associate-*l*N/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      8. mul-1-negN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      9. distribute-rgt-neg-inN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      10. *-commutativeN/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
      11. lower-fma.f64N/A

        \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right)}{e^{x}} \]
    7. Applied rewrites10.6%

      \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right)}{e^{x}} \]
    8. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}{e^{x}}} \]
      2. clear-numN/A

        \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}}} \]
      3. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}}} \]
      4. lower-/.f6410.6

        \[\leadsto \frac{1}{\color{blue}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right)}}} \]
    9. Applied rewrites10.6%

      \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, -0.25, 1\right)\right)\right)}}} \]
    10. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \frac{1}{\color{blue}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}} \]
      2. rem-exp-logN/A

        \[\leadsto \frac{1}{\frac{e^{x}}{\color{blue}{e^{\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}}} \]
      3. lift-log.f64N/A

        \[\leadsto \frac{1}{\frac{e^{x}}{e^{\color{blue}{\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}}} \]
      4. lift-exp.f64N/A

        \[\leadsto \frac{1}{\frac{\color{blue}{e^{x}}}{e^{\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}} \]
      5. exp-diffN/A

        \[\leadsto \frac{1}{\color{blue}{e^{x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}} \]
      6. flip--N/A

        \[\leadsto \frac{1}{e^{\color{blue}{\frac{x \cdot x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right) \cdot \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}{x + \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}}} \]
      7. div-invN/A

        \[\leadsto \frac{1}{e^{\color{blue}{\left(x \cdot x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right) \cdot \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)\right) \cdot \frac{1}{x + \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}}}} \]
      8. exp-prodN/A

        \[\leadsto \frac{1}{\color{blue}{{\left(e^{x \cdot x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right) \cdot \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}\right)}^{\left(\frac{1}{x + \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, \frac{-1}{4}, 1\right)\right)\right)}\right)}}} \]
    11. Applied rewrites100.0%

      \[\leadsto \frac{1}{\color{blue}{{\left(e^{x \cdot x - {\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right)}^{2}}\right)}^{\left({\left(\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right) + x\right)}^{-1}\right)}}} \]

    if -1.000000000000002e-309 < x < 0.20000000000000001

    1. Initial program 8.4%

      \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \left(\color{blue}{1} \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
    4. Step-by-step derivation
      1. Applied rewrites5.5%

        \[\leadsto \left(\color{blue}{1} \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
      2. Taylor expanded in x around 0

        \[\leadsto \left(1 \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right) \cdot e^{-x} \]
      3. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \left(1 \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right) \cdot e^{-x} \]
        2. metadata-evalN/A

          \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        3. metadata-evalN/A

          \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        4. lft-mult-inverseN/A

          \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        5. distribute-rgt-neg-outN/A

          \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        6. mul-1-negN/A

          \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        7. associate-*l*N/A

          \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        8. mul-1-negN/A

          \[\leadsto \left(1 \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        9. distribute-rgt-neg-inN/A

          \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        10. *-commutativeN/A

          \[\leadsto \left(1 \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
        11. lower-fma.f64N/A

          \[\leadsto \left(1 \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right) \cdot e^{-x} \]
      4. Applied rewrites5.5%

        \[\leadsto \left(1 \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right) \cdot e^{-x} \]
      5. Taylor expanded in x around 0

        \[\leadsto \left(\color{blue}{\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + \frac{1}{2} \cdot x\right) + 1\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
        2. *-commutativeN/A

          \[\leadsto \left(\left(\color{blue}{\left(1 + \frac{1}{2} \cdot x\right) \cdot x} + 1\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
        3. lower-fma.f64N/A

          \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(1 + \frac{1}{2} \cdot x, x, 1\right)\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
        4. +-commutativeN/A

          \[\leadsto \left(\left(\mathsf{fma}\left(\color{blue}{\frac{1}{2} \cdot x + 1}, x, 1\right)\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
        5. lower-fma.f647.7

          \[\leadsto \left(\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.5, x, 1\right)}, x, 1\right)\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
      7. Applied rewrites7.7%

        \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.5, x, 1\right), x, 1\right)\right)} \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
      8. Taylor expanded in x around inf

        \[\leadsto \left(\left({x}^{2} \cdot \color{blue}{\left(\frac{1}{2} + \frac{1}{x}\right)}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
      9. Step-by-step derivation
        1. Applied rewrites98.2%

          \[\leadsto \left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot \color{blue}{x}\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]

        if 0.20000000000000001 < x

        1. Initial program 0.0%

          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}} \]
          2. lift-exp.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{e^{-x}} \]
          3. lift-neg.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
          4. exp-negN/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
          5. lift-exp.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \frac{1}{\color{blue}{e^{x}}} \]
          6. un-div-invN/A

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
          7. lower-/.f640.0

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
        4. Applied rewrites0.0%

          \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
        5. Taylor expanded in x around 0

          \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right)}{e^{x}} \]
        6. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right)}{e^{x}} \]
          2. metadata-evalN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          3. metadata-evalN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          4. lft-mult-inverseN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          5. distribute-rgt-neg-outN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          6. mul-1-negN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          7. associate-*l*N/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          8. mul-1-negN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          10. *-commutativeN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          11. lower-fma.f64N/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right)}{e^{x}} \]
        7. Applied rewrites0.0%

          \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right)}{e^{x}} \]
        8. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}{e^{x}}} \]
          2. clear-numN/A

            \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}}} \]
          3. inv-powN/A

            \[\leadsto \color{blue}{{\left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right)}^{-1}} \]
          4. pow-to-expN/A

            \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
          5. lower-exp.f64N/A

            \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
          6. lower-*.f64N/A

            \[\leadsto e^{\color{blue}{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
        9. Applied rewrites0.0%

          \[\leadsto \color{blue}{e^{\left(x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, -0.25, 1\right)\right)\right)\right) \cdot -1}} \]
        10. Taylor expanded in x around inf

          \[\leadsto e^{\color{blue}{-1 \cdot x}} \]
        11. Step-by-step derivation
          1. neg-mul-1N/A

            \[\leadsto e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
          2. lower-neg.f64100.0

            \[\leadsto e^{\color{blue}{-x}} \]
        12. Applied rewrites100.0%

          \[\leadsto e^{\color{blue}{-x}} \]
      10. Recombined 3 regimes into one program.
      11. Final simplification99.3%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1 \cdot 10^{-309}:\\ \;\;\;\;{\left({\left(e^{x \cdot x - {\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right)}^{2}}\right)}^{\left({\left(\log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(-0.25 \cdot x, x, 1\right)\right)\right) + x\right)}^{-1}\right)}\right)}^{-1}\\ \mathbf{elif}\;x \leq 0.2:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x}\\ \mathbf{else}:\\ \;\;\;\;e^{-x}\\ \end{array} \]
      12. Add Preprocessing

      Alternative 2: 97.7% accurate, 1.7× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} t_0 := e^{-x}\\ \mathbf{if}\;x \leq -1 \cdot 10^{-309} \lor \neg \left(x \leq 0.2\right):\\ \;\;\;\;t\_0\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot t\_0\\ \end{array} \end{array} \]
      (FPCore (x)
       :precision binary64
       (let* ((t_0 (exp (- x))))
         (if (or (<= x -1e-309) (not (<= x 0.2)))
           t_0
           (* (fmod (* (fma 0.5 x 1.0) x) (fma -0.25 (* x x) 1.0)) t_0))))
      double code(double x) {
      	double t_0 = exp(-x);
      	double tmp;
      	if ((x <= -1e-309) || !(x <= 0.2)) {
      		tmp = t_0;
      	} else {
      		tmp = fmod((fma(0.5, x, 1.0) * x), fma(-0.25, (x * x), 1.0)) * t_0;
      	}
      	return tmp;
      }
      
      function code(x)
      	t_0 = exp(Float64(-x))
      	tmp = 0.0
      	if ((x <= -1e-309) || !(x <= 0.2))
      		tmp = t_0;
      	else
      		tmp = Float64(rem(Float64(fma(0.5, x, 1.0) * x), fma(-0.25, Float64(x * x), 1.0)) * t_0);
      	end
      	return tmp
      end
      
      code[x_] := Block[{t$95$0 = N[Exp[(-x)], $MachinePrecision]}, If[Or[LessEqual[x, -1e-309], N[Not[LessEqual[x, 0.2]], $MachinePrecision]], t$95$0, N[(N[With[{TMP1 = N[(N[(0.5 * x + 1.0), $MachinePrecision] * x), $MachinePrecision], TMP2 = N[(-0.25 * N[(x * x), $MachinePrecision] + 1.0), $MachinePrecision]}, Mod[Abs[TMP1], Abs[TMP2]] * Sign[TMP1]], $MachinePrecision] * t$95$0), $MachinePrecision]]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      t_0 := e^{-x}\\
      \mathbf{if}\;x \leq -1 \cdot 10^{-309} \lor \neg \left(x \leq 0.2\right):\\
      \;\;\;\;t\_0\\
      
      \mathbf{else}:\\
      \;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot t\_0\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if x < -1.000000000000002e-309 or 0.20000000000000001 < x

        1. Initial program 7.0%

          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}} \]
          2. lift-exp.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{e^{-x}} \]
          3. lift-neg.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
          4. exp-negN/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
          5. lift-exp.f64N/A

            \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \frac{1}{\color{blue}{e^{x}}} \]
          6. un-div-invN/A

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
          7. lower-/.f647.0

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
        4. Applied rewrites7.0%

          \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
        5. Taylor expanded in x around 0

          \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right)}{e^{x}} \]
        6. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right)}{e^{x}} \]
          2. metadata-evalN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          3. metadata-evalN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          4. lft-mult-inverseN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          5. distribute-rgt-neg-outN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          6. mul-1-negN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          7. associate-*l*N/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          8. mul-1-negN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          9. distribute-rgt-neg-inN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          10. *-commutativeN/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
          11. lower-fma.f64N/A

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right)}{e^{x}} \]
        7. Applied rewrites7.0%

          \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right)}{e^{x}} \]
        8. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}{e^{x}}} \]
          2. clear-numN/A

            \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}}} \]
          3. inv-powN/A

            \[\leadsto \color{blue}{{\left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right)}^{-1}} \]
          4. pow-to-expN/A

            \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
          5. lower-exp.f64N/A

            \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
          6. lower-*.f64N/A

            \[\leadsto e^{\color{blue}{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
        9. Applied rewrites7.1%

          \[\leadsto \color{blue}{e^{\left(x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, -0.25, 1\right)\right)\right)\right) \cdot -1}} \]
        10. Taylor expanded in x around inf

          \[\leadsto e^{\color{blue}{-1 \cdot x}} \]
        11. Step-by-step derivation
          1. neg-mul-1N/A

            \[\leadsto e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
          2. lower-neg.f6495.8

            \[\leadsto e^{\color{blue}{-x}} \]
        12. Applied rewrites95.8%

          \[\leadsto e^{\color{blue}{-x}} \]

        if -1.000000000000002e-309 < x < 0.20000000000000001

        1. Initial program 8.4%

          \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \left(\color{blue}{1} \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
        4. Step-by-step derivation
          1. Applied rewrites5.5%

            \[\leadsto \left(\color{blue}{1} \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
          2. Taylor expanded in x around 0

            \[\leadsto \left(1 \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right) \cdot e^{-x} \]
          3. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \left(1 \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right) \cdot e^{-x} \]
            2. metadata-evalN/A

              \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            3. metadata-evalN/A

              \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            4. lft-mult-inverseN/A

              \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            5. distribute-rgt-neg-outN/A

              \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            6. mul-1-negN/A

              \[\leadsto \left(1 \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            7. associate-*l*N/A

              \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            8. mul-1-negN/A

              \[\leadsto \left(1 \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            9. distribute-rgt-neg-inN/A

              \[\leadsto \left(1 \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            10. *-commutativeN/A

              \[\leadsto \left(1 \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right) \cdot e^{-x} \]
            11. lower-fma.f64N/A

              \[\leadsto \left(1 \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right) \cdot e^{-x} \]
          4. Applied rewrites5.5%

            \[\leadsto \left(1 \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right) \cdot e^{-x} \]
          5. Taylor expanded in x around 0

            \[\leadsto \left(\color{blue}{\left(1 + x \cdot \left(1 + \frac{1}{2} \cdot x\right)\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
          6. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \left(\color{blue}{\left(x \cdot \left(1 + \frac{1}{2} \cdot x\right) + 1\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
            2. *-commutativeN/A

              \[\leadsto \left(\left(\color{blue}{\left(1 + \frac{1}{2} \cdot x\right) \cdot x} + 1\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
            3. lower-fma.f64N/A

              \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(1 + \frac{1}{2} \cdot x, x, 1\right)\right)} \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
            4. +-commutativeN/A

              \[\leadsto \left(\left(\mathsf{fma}\left(\color{blue}{\frac{1}{2} \cdot x + 1}, x, 1\right)\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
            5. lower-fma.f647.7

              \[\leadsto \left(\left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.5, x, 1\right)}, x, 1\right)\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
          7. Applied rewrites7.7%

            \[\leadsto \left(\color{blue}{\left(\mathsf{fma}\left(\mathsf{fma}\left(0.5, x, 1\right), x, 1\right)\right)} \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
          8. Taylor expanded in x around inf

            \[\leadsto \left(\left({x}^{2} \cdot \color{blue}{\left(\frac{1}{2} + \frac{1}{x}\right)}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
          9. Step-by-step derivation
            1. Applied rewrites98.2%

              \[\leadsto \left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot \color{blue}{x}\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x} \]
          10. Recombined 2 regimes into one program.
          11. Final simplification96.7%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1 \cdot 10^{-309} \lor \neg \left(x \leq 0.2\right):\\ \;\;\;\;e^{-x}\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\mathsf{fma}\left(0.5, x, 1\right) \cdot x\right) \bmod \left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)\right) \cdot e^{-x}\\ \end{array} \]
          12. Add Preprocessing

          Alternative 3: 61.5% accurate, 4.1× speedup?

          \[\begin{array}{l} \\ e^{-x} \end{array} \]
          (FPCore (x) :precision binary64 (exp (- x)))
          double code(double x) {
          	return exp(-x);
          }
          
          real(8) function code(x)
              real(8), intent (in) :: x
              code = exp(-x)
          end function
          
          public static double code(double x) {
          	return Math.exp(-x);
          }
          
          def code(x):
          	return math.exp(-x)
          
          function code(x)
          	return exp(Float64(-x))
          end
          
          function tmp = code(x)
          	tmp = exp(-x);
          end
          
          code[x_] := N[Exp[(-x)], $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          e^{-x}
          \end{array}
          
          Derivation
          1. Initial program 7.5%

            \[\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto \color{blue}{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{-x}} \]
            2. lift-exp.f64N/A

              \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{e^{-x}} \]
            3. lift-neg.f64N/A

              \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
            4. exp-negN/A

              \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \color{blue}{\frac{1}{e^{x}}} \]
            5. lift-exp.f64N/A

              \[\leadsto \left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right) \cdot \frac{1}{\color{blue}{e^{x}}} \]
            6. un-div-invN/A

              \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
            7. lower-/.f647.5

              \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
          4. Applied rewrites7.5%

            \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\sqrt{\cos x}\right)\right)}{e^{x}}} \]
          5. Taylor expanded in x around 0

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(1 + \frac{-1}{4} \cdot {x}^{2}\right)}\right)}{e^{x}} \]
          6. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\frac{-1}{4} \cdot {x}^{2} + 1\right)}\right)}{e^{x}} \]
            2. metadata-evalN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\frac{1}{4} \cdot -1\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            3. metadata-evalN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\mathsf{neg}\left(1\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            4. lft-mult-inverseN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\mathsf{neg}\left(\color{blue}{\frac{1}{{x}^{2}} \cdot {x}^{2}}\right)\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            5. distribute-rgt-neg-outN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \color{blue}{\left(\frac{1}{{x}^{2}} \cdot \left(\mathsf{neg}\left({x}^{2}\right)\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            6. mul-1-negN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\frac{1}{4} \cdot \left(\frac{1}{{x}^{2}} \cdot \color{blue}{\left(-1 \cdot {x}^{2}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            7. associate-*l*N/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \left(-1 \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            8. mul-1-negN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot \color{blue}{\left(\mathsf{neg}\left({x}^{2}\right)\right)}\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            9. distribute-rgt-neg-inN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\color{blue}{\left(\mathsf{neg}\left(\left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) \cdot {x}^{2}\right)\right)} \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            10. *-commutativeN/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \left(\left(\mathsf{neg}\left(\color{blue}{{x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)}\right)\right) \cdot {x}^{2} + 1\right)\right)}{e^{x}} \]
            11. lower-fma.f64N/A

              \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(\mathsf{neg}\left({x}^{2} \cdot \left(\frac{1}{4} \cdot \frac{1}{{x}^{2}}\right)\right), {x}^{2}, 1\right)\right)}\right)}{e^{x}} \]
          7. Applied rewrites7.3%

            \[\leadsto \frac{\left(\left(e^{x}\right) \bmod \color{blue}{\left(\mathsf{fma}\left(-0.25, x \cdot x, 1\right)\right)}\right)}{e^{x}} \]
          8. Step-by-step derivation
            1. lift-/.f64N/A

              \[\leadsto \color{blue}{\frac{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}{e^{x}}} \]
            2. clear-numN/A

              \[\leadsto \color{blue}{\frac{1}{\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}}} \]
            3. inv-powN/A

              \[\leadsto \color{blue}{{\left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right)}^{-1}} \]
            4. pow-to-expN/A

              \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
            5. lower-exp.f64N/A

              \[\leadsto \color{blue}{e^{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
            6. lower-*.f64N/A

              \[\leadsto e^{\color{blue}{\log \left(\frac{e^{x}}{\left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(\frac{-1}{4}, x \cdot x, 1\right)\right)\right)}\right) \cdot -1}} \]
          9. Applied rewrites7.3%

            \[\leadsto \color{blue}{e^{\left(x - \log \left(\left(e^{x}\right) \bmod \left(\mathsf{fma}\left(x \cdot x, -0.25, 1\right)\right)\right)\right) \cdot -1}} \]
          10. Taylor expanded in x around inf

            \[\leadsto e^{\color{blue}{-1 \cdot x}} \]
          11. Step-by-step derivation
            1. neg-mul-1N/A

              \[\leadsto e^{\color{blue}{\mathsf{neg}\left(x\right)}} \]
            2. lower-neg.f6460.2

              \[\leadsto e^{\color{blue}{-x}} \]
          12. Applied rewrites60.2%

            \[\leadsto e^{\color{blue}{-x}} \]
          13. Add Preprocessing

          Reproduce

          ?
          herbie shell --seed 2024320 
          (FPCore (x)
            :name "expfmod (used to be hard to sample)"
            :precision binary64
            (* (fmod (exp x) (sqrt (cos x))) (exp (- x))))