symmetry log of sum of exp

Percentage Accurate: 53.3% → 100.0%
Time: 10.7s
Alternatives: 12
Speedup: 2.8×

Specification

?
\[\begin{array}{l} \\ \log \left(e^{a} + e^{b}\right) \end{array} \]
(FPCore (a b) :precision binary64 (log (+ (exp a) (exp b))))
double code(double a, double b) {
	return log((exp(a) + exp(b)));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = log((exp(a) + exp(b)))
end function
public static double code(double a, double b) {
	return Math.log((Math.exp(a) + Math.exp(b)));
}
def code(a, b):
	return math.log((math.exp(a) + math.exp(b)))
function code(a, b)
	return log(Float64(exp(a) + exp(b)))
end
function tmp = code(a, b)
	tmp = log((exp(a) + exp(b)));
end
code[a_, b_] := N[Log[N[(N[Exp[a], $MachinePrecision] + N[Exp[b], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\log \left(e^{a} + e^{b}\right)
\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 12 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: 53.3% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \log \left(e^{a} + e^{b}\right) \end{array} \]
(FPCore (a b) :precision binary64 (log (+ (exp a) (exp b))))
double code(double a, double b) {
	return log((exp(a) + exp(b)));
}
real(8) function code(a, b)
    real(8), intent (in) :: a
    real(8), intent (in) :: b
    code = log((exp(a) + exp(b)))
end function
public static double code(double a, double b) {
	return Math.log((Math.exp(a) + Math.exp(b)));
}
def code(a, b):
	return math.log((math.exp(a) + math.exp(b)))
function code(a, b)
	return log(Float64(exp(a) + exp(b)))
end
function tmp = code(a, b)
	tmp = log((exp(a) + exp(b)));
end
code[a_, b_] := N[Log[N[(N[Exp[a], $MachinePrecision] + N[Exp[b], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]
\begin{array}{l}

\\
\log \left(e^{a} + e^{b}\right)
\end{array}

Alternative 1: 100.0% accurate, 1.5× speedup?

\[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \mathsf{log1p}\left(e^{a - b}\right) + b \end{array} \]
NOTE: a and b should be sorted in increasing order before calling this function.
(FPCore (a b) :precision binary64 (+ (log1p (exp (- a b))) b))
assert(a < b);
double code(double a, double b) {
	return log1p(exp((a - b))) + b;
}
assert a < b;
public static double code(double a, double b) {
	return Math.log1p(Math.exp((a - b))) + b;
}
[a, b] = sort([a, b])
def code(a, b):
	return math.log1p(math.exp((a - b))) + b
a, b = sort([a, b])
function code(a, b)
	return Float64(log1p(exp(Float64(a - b))) + b)
end
NOTE: a and b should be sorted in increasing order before calling this function.
code[a_, b_] := N[(N[Log[1 + N[Exp[N[(a - b), $MachinePrecision]], $MachinePrecision]], $MachinePrecision] + b), $MachinePrecision]
\begin{array}{l}
[a, b] = \mathsf{sort}([a, b])\\
\\
\mathsf{log1p}\left(e^{a - b}\right) + b
\end{array}
Derivation
  1. Initial program 53.4%

    \[\log \left(e^{a} + e^{b}\right) \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-+.f64N/A

      \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
    2. lift-exp.f64N/A

      \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
    3. sinh-+-cosh-revN/A

      \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
    4. flip-+N/A

      \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
    5. sinh-coshN/A

      \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
    6. sinh-coshN/A

      \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
    7. sinh---cosh-revN/A

      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
    8. lift-exp.f64N/A

      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
    9. sinh-+-cosh-revN/A

      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
    10. flip-+N/A

      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
    11. sinh---cosh-revN/A

      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
    12. frac-addN/A

      \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
    13. lower-/.f64N/A

      \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
  4. Applied rewrites48.9%

    \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
  5. Step-by-step derivation
    1. lift-log.f64N/A

      \[\leadsto \color{blue}{\log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
    2. lift-/.f64N/A

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

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

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\color{blue}{\left(-a\right) + \left(-b\right)}}}\right) \]
    5. exp-sumN/A

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

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\color{blue}{e^{-a}} \cdot e^{-b}}\right) \]
    7. *-rgt-identityN/A

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\color{blue}{\left(e^{-a} \cdot 1\right)} \cdot e^{-b}}\right) \]
    8. lift-*.f64N/A

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

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\left(e^{-a} \cdot 1\right) \cdot \color{blue}{e^{-b}}}\right) \]
    10. *-lft-identityN/A

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\left(e^{-a} \cdot 1\right) \cdot \color{blue}{\left(1 \cdot e^{-b}\right)}}\right) \]
    11. associate-/r*N/A

      \[\leadsto \log \color{blue}{\left(\frac{\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}}{1 \cdot e^{-b}}\right)} \]
    12. log-divN/A

      \[\leadsto \color{blue}{\log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}\right) - \log \left(1 \cdot e^{-b}\right)} \]
    13. *-lft-identityN/A

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

      \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}\right) - \log \color{blue}{\left(e^{-b}\right)} \]
  6. Applied rewrites72.3%

    \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{\left(-b\right) - \left(-a\right)}\right) - \left(-b\right)} \]
  7. Taylor expanded in a around inf

    \[\leadsto \color{blue}{b + \log \left(1 + e^{a - b}\right)} \]
  8. Step-by-step derivation
    1. +-commutativeN/A

      \[\leadsto \color{blue}{\log \left(1 + e^{a - b}\right) + b} \]
    2. lower-+.f64N/A

      \[\leadsto \color{blue}{\log \left(1 + e^{a - b}\right) + b} \]
    3. lower-log1p.f64N/A

      \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a - b}\right)} + b \]
    4. lower-exp.f64N/A

      \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a - b}}\right) + b \]
    5. lower--.f6472.3

      \[\leadsto \mathsf{log1p}\left(e^{\color{blue}{a - b}}\right) + b \]
  9. Applied rewrites72.3%

    \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a - b}\right) + b} \]
  10. Add Preprocessing

Alternative 2: 58.2% accurate, 1.4× speedup?

\[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -160:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(e^{-b}\right) + b\\ \end{array} \end{array} \]
NOTE: a and b should be sorted in increasing order before calling this function.
(FPCore (a b)
 :precision binary64
 (if (<= a -160.0) (* 0.5 b) (+ (log1p (exp (- b))) b)))
assert(a < b);
double code(double a, double b) {
	double tmp;
	if (a <= -160.0) {
		tmp = 0.5 * b;
	} else {
		tmp = log1p(exp(-b)) + b;
	}
	return tmp;
}
assert a < b;
public static double code(double a, double b) {
	double tmp;
	if (a <= -160.0) {
		tmp = 0.5 * b;
	} else {
		tmp = Math.log1p(Math.exp(-b)) + b;
	}
	return tmp;
}
[a, b] = sort([a, b])
def code(a, b):
	tmp = 0
	if a <= -160.0:
		tmp = 0.5 * b
	else:
		tmp = math.log1p(math.exp(-b)) + b
	return tmp
a, b = sort([a, b])
function code(a, b)
	tmp = 0.0
	if (a <= -160.0)
		tmp = Float64(0.5 * b);
	else
		tmp = Float64(log1p(exp(Float64(-b))) + b);
	end
	return tmp
end
NOTE: a and b should be sorted in increasing order before calling this function.
code[a_, b_] := If[LessEqual[a, -160.0], N[(0.5 * b), $MachinePrecision], N[(N[Log[1 + N[Exp[(-b)], $MachinePrecision]], $MachinePrecision] + b), $MachinePrecision]]
\begin{array}{l}
[a, b] = \mathsf{sort}([a, b])\\
\\
\begin{array}{l}
\mathbf{if}\;a \leq -160:\\
\;\;\;\;0.5 \cdot b\\

\mathbf{else}:\\
\;\;\;\;\mathsf{log1p}\left(e^{-b}\right) + b\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if a < -160

    1. Initial program 5.9%

      \[\log \left(e^{a} + e^{b}\right) \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
      2. lift-exp.f64N/A

        \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
      3. sinh-+-cosh-revN/A

        \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
      4. flip-+N/A

        \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
      5. sinh-coshN/A

        \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
      6. sinh-coshN/A

        \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
      7. sinh---cosh-revN/A

        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
      8. lift-exp.f64N/A

        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
      9. sinh-+-cosh-revN/A

        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
      10. flip-+N/A

        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
      11. sinh---cosh-revN/A

        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
      12. frac-addN/A

        \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
      13. lower-/.f64N/A

        \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
    4. Applied rewrites0.1%

      \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
    5. Taylor expanded in a around 0

      \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
    6. Step-by-step derivation
      1. div-addN/A

        \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
      2. *-inversesN/A

        \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
      3. +-commutativeN/A

        \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
      4. lower-log1p.f64N/A

        \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
      5. exp-negN/A

        \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
      6. remove-double-divN/A

        \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
      7. lower-exp.f643.8

        \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
    7. Applied rewrites3.8%

      \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
    8. Taylor expanded in b around 0

      \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
    9. Step-by-step derivation
      1. Applied rewrites3.8%

        \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
      2. Taylor expanded in b around inf

        \[\leadsto \frac{1}{2} \cdot b \]
      3. Step-by-step derivation
        1. Applied rewrites18.8%

          \[\leadsto 0.5 \cdot b \]

        if -160 < a

        1. Initial program 67.0%

          \[\log \left(e^{a} + e^{b}\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
          2. lift-exp.f64N/A

            \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
          3. sinh-+-cosh-revN/A

            \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
          4. flip-+N/A

            \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
          5. sinh-coshN/A

            \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
          6. sinh-coshN/A

            \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
          7. sinh---cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
          8. lift-exp.f64N/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
          9. sinh-+-cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
          10. flip-+N/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
          11. sinh---cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
          12. frac-addN/A

            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
          13. lower-/.f64N/A

            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
        4. Applied rewrites62.8%

          \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
        5. Step-by-step derivation
          1. lift-log.f64N/A

            \[\leadsto \color{blue}{\log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
          2. lift-/.f64N/A

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

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

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\color{blue}{\left(-a\right) + \left(-b\right)}}}\right) \]
          5. exp-sumN/A

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

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\color{blue}{e^{-a}} \cdot e^{-b}}\right) \]
          7. *-rgt-identityN/A

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\color{blue}{\left(e^{-a} \cdot 1\right)} \cdot e^{-b}}\right) \]
          8. lift-*.f64N/A

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

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\left(e^{-a} \cdot 1\right) \cdot \color{blue}{e^{-b}}}\right) \]
          10. *-lft-identityN/A

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{\left(e^{-a} \cdot 1\right) \cdot \color{blue}{\left(1 \cdot e^{-b}\right)}}\right) \]
          11. associate-/r*N/A

            \[\leadsto \log \color{blue}{\left(\frac{\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}}{1 \cdot e^{-b}}\right)} \]
          12. log-divN/A

            \[\leadsto \color{blue}{\log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}\right) - \log \left(1 \cdot e^{-b}\right)} \]
          13. *-lft-identityN/A

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

            \[\leadsto \log \left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{-a} \cdot 1}\right) - \log \color{blue}{\left(e^{-b}\right)} \]
        6. Applied rewrites64.4%

          \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{\left(-b\right) - \left(-a\right)}\right) - \left(-b\right)} \]
        7. Taylor expanded in a around 0

          \[\leadsto \color{blue}{b + \log \left(1 + e^{\mathsf{neg}\left(b\right)}\right)} \]
        8. Step-by-step derivation
          1. +-commutativeN/A

            \[\leadsto \color{blue}{\log \left(1 + e^{\mathsf{neg}\left(b\right)}\right) + b} \]
          2. lower-+.f64N/A

            \[\leadsto \color{blue}{\log \left(1 + e^{\mathsf{neg}\left(b\right)}\right) + b} \]
          3. lower-log1p.f64N/A

            \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{\mathsf{neg}\left(b\right)}\right)} + b \]
          4. lower-exp.f64N/A

            \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{\mathsf{neg}\left(b\right)}}\right) + b \]
          5. lower-neg.f6462.6

            \[\leadsto \mathsf{log1p}\left(e^{\color{blue}{-b}}\right) + b \]
        9. Applied rewrites62.6%

          \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{-b}\right) + b} \]
      4. Recombined 2 regimes into one program.
      5. Add Preprocessing

      Alternative 3: 57.0% accurate, 1.5× speedup?

      \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -360:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(e^{a}\right)\\ \end{array} \end{array} \]
      NOTE: a and b should be sorted in increasing order before calling this function.
      (FPCore (a b) :precision binary64 (if (<= a -360.0) (* 0.5 b) (log1p (exp a))))
      assert(a < b);
      double code(double a, double b) {
      	double tmp;
      	if (a <= -360.0) {
      		tmp = 0.5 * b;
      	} else {
      		tmp = log1p(exp(a));
      	}
      	return tmp;
      }
      
      assert a < b;
      public static double code(double a, double b) {
      	double tmp;
      	if (a <= -360.0) {
      		tmp = 0.5 * b;
      	} else {
      		tmp = Math.log1p(Math.exp(a));
      	}
      	return tmp;
      }
      
      [a, b] = sort([a, b])
      def code(a, b):
      	tmp = 0
      	if a <= -360.0:
      		tmp = 0.5 * b
      	else:
      		tmp = math.log1p(math.exp(a))
      	return tmp
      
      a, b = sort([a, b])
      function code(a, b)
      	tmp = 0.0
      	if (a <= -360.0)
      		tmp = Float64(0.5 * b);
      	else
      		tmp = log1p(exp(a));
      	end
      	return tmp
      end
      
      NOTE: a and b should be sorted in increasing order before calling this function.
      code[a_, b_] := If[LessEqual[a, -360.0], N[(0.5 * b), $MachinePrecision], N[Log[1 + N[Exp[a], $MachinePrecision]], $MachinePrecision]]
      
      \begin{array}{l}
      [a, b] = \mathsf{sort}([a, b])\\
      \\
      \begin{array}{l}
      \mathbf{if}\;a \leq -360:\\
      \;\;\;\;0.5 \cdot b\\
      
      \mathbf{else}:\\
      \;\;\;\;\mathsf{log1p}\left(e^{a}\right)\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if a < -360

        1. Initial program 5.9%

          \[\log \left(e^{a} + e^{b}\right) \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
          2. lift-exp.f64N/A

            \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
          3. sinh-+-cosh-revN/A

            \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
          4. flip-+N/A

            \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
          5. sinh-coshN/A

            \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
          6. sinh-coshN/A

            \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
          7. sinh---cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
          8. lift-exp.f64N/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
          9. sinh-+-cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
          10. flip-+N/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
          11. sinh---cosh-revN/A

            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
          12. frac-addN/A

            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
          13. lower-/.f64N/A

            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
        4. Applied rewrites0.1%

          \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
        5. Taylor expanded in a around 0

          \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
        6. Step-by-step derivation
          1. div-addN/A

            \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
          2. *-inversesN/A

            \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
          3. +-commutativeN/A

            \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
          4. lower-log1p.f64N/A

            \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
          5. exp-negN/A

            \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
          6. remove-double-divN/A

            \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
          7. lower-exp.f643.8

            \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
        7. Applied rewrites3.8%

          \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
        8. Taylor expanded in b around 0

          \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
        9. Step-by-step derivation
          1. Applied rewrites3.8%

            \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
          2. Taylor expanded in b around inf

            \[\leadsto \frac{1}{2} \cdot b \]
          3. Step-by-step derivation
            1. Applied rewrites18.8%

              \[\leadsto 0.5 \cdot b \]

            if -360 < a

            1. Initial program 67.0%

              \[\log \left(e^{a} + e^{b}\right) \]
            2. Add Preprocessing
            3. Taylor expanded in b around 0

              \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
            4. Step-by-step derivation
              1. lower-log1p.f64N/A

                \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
              2. lower-exp.f6463.8

                \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
            5. Applied rewrites63.8%

              \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
          4. Recombined 2 regimes into one program.
          5. Final simplification53.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -360:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(e^{a}\right)\\ \end{array} \]
          6. Add Preprocessing

          Alternative 4: 57.2% accurate, 2.3× speedup?

          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right), a, \mathsf{fma}\left(0.5, b, \log 2\right)\right)\\ \end{array} \end{array} \]
          NOTE: a and b should be sorted in increasing order before calling this function.
          (FPCore (a b)
           :precision binary64
           (if (<= a -132.0)
             (* 0.5 b)
             (fma (fma 0.125 a (fma -0.25 b 0.5)) a (fma 0.5 b (log 2.0)))))
          assert(a < b);
          double code(double a, double b) {
          	double tmp;
          	if (a <= -132.0) {
          		tmp = 0.5 * b;
          	} else {
          		tmp = fma(fma(0.125, a, fma(-0.25, b, 0.5)), a, fma(0.5, b, log(2.0)));
          	}
          	return tmp;
          }
          
          a, b = sort([a, b])
          function code(a, b)
          	tmp = 0.0
          	if (a <= -132.0)
          		tmp = Float64(0.5 * b);
          	else
          		tmp = fma(fma(0.125, a, fma(-0.25, b, 0.5)), a, fma(0.5, b, log(2.0)));
          	end
          	return tmp
          end
          
          NOTE: a and b should be sorted in increasing order before calling this function.
          code[a_, b_] := If[LessEqual[a, -132.0], N[(0.5 * b), $MachinePrecision], N[(N[(0.125 * a + N[(-0.25 * b + 0.5), $MachinePrecision]), $MachinePrecision] * a + N[(0.5 * b + N[Log[2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
          
          \begin{array}{l}
          [a, b] = \mathsf{sort}([a, b])\\
          \\
          \begin{array}{l}
          \mathbf{if}\;a \leq -132:\\
          \;\;\;\;0.5 \cdot b\\
          
          \mathbf{else}:\\
          \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right), a, \mathsf{fma}\left(0.5, b, \log 2\right)\right)\\
          
          
          \end{array}
          \end{array}
          
          Derivation
          1. Split input into 2 regimes
          2. if a < -132

            1. Initial program 5.9%

              \[\log \left(e^{a} + e^{b}\right) \]
            2. Add Preprocessing
            3. Step-by-step derivation
              1. lift-+.f64N/A

                \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
              2. lift-exp.f64N/A

                \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
              3. sinh-+-cosh-revN/A

                \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
              4. flip-+N/A

                \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
              5. sinh-coshN/A

                \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
              6. sinh-coshN/A

                \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
              7. sinh---cosh-revN/A

                \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
              8. lift-exp.f64N/A

                \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
              9. sinh-+-cosh-revN/A

                \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
              10. flip-+N/A

                \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
              11. sinh---cosh-revN/A

                \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
              12. frac-addN/A

                \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
              13. lower-/.f64N/A

                \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
            4. Applied rewrites0.1%

              \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
            5. Taylor expanded in a around 0

              \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
            6. Step-by-step derivation
              1. div-addN/A

                \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
              2. *-inversesN/A

                \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
              3. +-commutativeN/A

                \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
              4. lower-log1p.f64N/A

                \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
              5. exp-negN/A

                \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
              6. remove-double-divN/A

                \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
              7. lower-exp.f643.8

                \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
            7. Applied rewrites3.8%

              \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
            8. Taylor expanded in b around 0

              \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
            9. Step-by-step derivation
              1. Applied rewrites3.8%

                \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
              2. Taylor expanded in b around inf

                \[\leadsto \frac{1}{2} \cdot b \]
              3. Step-by-step derivation
                1. Applied rewrites18.8%

                  \[\leadsto 0.5 \cdot b \]

                if -132 < a

                1. Initial program 67.0%

                  \[\log \left(e^{a} + e^{b}\right) \]
                2. Add Preprocessing
                3. Taylor expanded in b around 0

                  \[\leadsto \color{blue}{\log \left(1 + e^{a}\right) + \frac{b}{1 + e^{a}}} \]
                4. Step-by-step derivation
                  1. *-rgt-identityN/A

                    \[\leadsto \log \left(1 + e^{a}\right) + \frac{\color{blue}{b \cdot 1}}{1 + e^{a}} \]
                  2. associate-*r/N/A

                    \[\leadsto \log \left(1 + e^{a}\right) + \color{blue}{b \cdot \frac{1}{1 + e^{a}}} \]
                  3. +-commutativeN/A

                    \[\leadsto \color{blue}{b \cdot \frac{1}{1 + e^{a}} + \log \left(1 + e^{a}\right)} \]
                  4. lower-+.f64N/A

                    \[\leadsto \color{blue}{b \cdot \frac{1}{1 + e^{a}} + \log \left(1 + e^{a}\right)} \]
                  5. associate-*r/N/A

                    \[\leadsto \color{blue}{\frac{b \cdot 1}{1 + e^{a}}} + \log \left(1 + e^{a}\right) \]
                  6. *-rgt-identityN/A

                    \[\leadsto \frac{\color{blue}{b}}{1 + e^{a}} + \log \left(1 + e^{a}\right) \]
                  7. lower-/.f64N/A

                    \[\leadsto \color{blue}{\frac{b}{1 + e^{a}}} + \log \left(1 + e^{a}\right) \]
                  8. +-commutativeN/A

                    \[\leadsto \frac{b}{\color{blue}{e^{a} + 1}} + \log \left(1 + e^{a}\right) \]
                  9. lower-+.f64N/A

                    \[\leadsto \frac{b}{\color{blue}{e^{a} + 1}} + \log \left(1 + e^{a}\right) \]
                  10. lower-exp.f64N/A

                    \[\leadsto \frac{b}{\color{blue}{e^{a}} + 1} + \log \left(1 + e^{a}\right) \]
                  11. lower-log1p.f64N/A

                    \[\leadsto \frac{b}{e^{a} + 1} + \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                  12. lower-exp.f6463.7

                    \[\leadsto \frac{b}{e^{a} + 1} + \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                5. Applied rewrites63.7%

                  \[\leadsto \color{blue}{\frac{b}{e^{a} + 1} + \mathsf{log1p}\left(e^{a}\right)} \]
                6. Taylor expanded in a around 0

                  \[\leadsto \log 2 + \color{blue}{\left(\frac{1}{2} \cdot b + a \cdot \left(\left(\frac{1}{2} + a \cdot \left(\frac{1}{8} - \left(\frac{-1}{8} \cdot b + \frac{1}{8} \cdot b\right)\right)\right) - \frac{1}{4} \cdot b\right)\right)} \]
                7. Step-by-step derivation
                  1. Applied rewrites63.1%

                    \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(0.125, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right), \color{blue}{a}, \mathsf{fma}\left(0.5, b, \log 2\right)\right) \]
                8. Recombined 2 regimes into one program.
                9. Final simplification53.2%

                  \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, \mathsf{fma}\left(-0.25, b, 0.5\right)\right), a, \mathsf{fma}\left(0.5, b, \log 2\right)\right)\\ \end{array} \]
                10. Add Preprocessing

                Alternative 5: 56.6% accurate, 2.3× speedup?

                \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -2.6:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, -0.005208333333333333, 0.125\right), a, 0.5\right), a, \log 2\right)\\ \end{array} \end{array} \]
                NOTE: a and b should be sorted in increasing order before calling this function.
                (FPCore (a b)
                 :precision binary64
                 (if (<= a -2.6)
                   (* 0.5 b)
                   (fma (fma (fma (* a a) -0.005208333333333333 0.125) a 0.5) a (log 2.0))))
                assert(a < b);
                double code(double a, double b) {
                	double tmp;
                	if (a <= -2.6) {
                		tmp = 0.5 * b;
                	} else {
                		tmp = fma(fma(fma((a * a), -0.005208333333333333, 0.125), a, 0.5), a, log(2.0));
                	}
                	return tmp;
                }
                
                a, b = sort([a, b])
                function code(a, b)
                	tmp = 0.0
                	if (a <= -2.6)
                		tmp = Float64(0.5 * b);
                	else
                		tmp = fma(fma(fma(Float64(a * a), -0.005208333333333333, 0.125), a, 0.5), a, log(2.0));
                	end
                	return tmp
                end
                
                NOTE: a and b should be sorted in increasing order before calling this function.
                code[a_, b_] := If[LessEqual[a, -2.6], N[(0.5 * b), $MachinePrecision], N[(N[(N[(N[(a * a), $MachinePrecision] * -0.005208333333333333 + 0.125), $MachinePrecision] * a + 0.5), $MachinePrecision] * a + N[Log[2.0], $MachinePrecision]), $MachinePrecision]]
                
                \begin{array}{l}
                [a, b] = \mathsf{sort}([a, b])\\
                \\
                \begin{array}{l}
                \mathbf{if}\;a \leq -2.6:\\
                \;\;\;\;0.5 \cdot b\\
                
                \mathbf{else}:\\
                \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, -0.005208333333333333, 0.125\right), a, 0.5\right), a, \log 2\right)\\
                
                
                \end{array}
                \end{array}
                
                Derivation
                1. Split input into 2 regimes
                2. if a < -2.60000000000000009

                  1. Initial program 5.9%

                    \[\log \left(e^{a} + e^{b}\right) \]
                  2. Add Preprocessing
                  3. Step-by-step derivation
                    1. lift-+.f64N/A

                      \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                    2. lift-exp.f64N/A

                      \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                    3. sinh-+-cosh-revN/A

                      \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                    4. flip-+N/A

                      \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                    5. sinh-coshN/A

                      \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                    6. sinh-coshN/A

                      \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                    7. sinh---cosh-revN/A

                      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                    8. lift-exp.f64N/A

                      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                    9. sinh-+-cosh-revN/A

                      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                    10. flip-+N/A

                      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                    11. sinh---cosh-revN/A

                      \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                    12. frac-addN/A

                      \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                    13. lower-/.f64N/A

                      \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                  4. Applied rewrites0.1%

                    \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                  5. Taylor expanded in a around 0

                    \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                  6. Step-by-step derivation
                    1. div-addN/A

                      \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                    2. *-inversesN/A

                      \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                    3. +-commutativeN/A

                      \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                    4. lower-log1p.f64N/A

                      \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                    5. exp-negN/A

                      \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                    6. remove-double-divN/A

                      \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                    7. lower-exp.f643.8

                      \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                  7. Applied rewrites3.8%

                    \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                  8. Taylor expanded in b around 0

                    \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                  9. Step-by-step derivation
                    1. Applied rewrites3.8%

                      \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                    2. Taylor expanded in b around inf

                      \[\leadsto \frac{1}{2} \cdot b \]
                    3. Step-by-step derivation
                      1. Applied rewrites18.8%

                        \[\leadsto 0.5 \cdot b \]

                      if -2.60000000000000009 < a

                      1. Initial program 67.0%

                        \[\log \left(e^{a} + e^{b}\right) \]
                      2. Add Preprocessing
                      3. Taylor expanded in b around 0

                        \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
                      4. Step-by-step derivation
                        1. lower-log1p.f64N/A

                          \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                        2. lower-exp.f6463.8

                          \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                      5. Applied rewrites63.8%

                        \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                      6. Taylor expanded in a around 0

                        \[\leadsto \log 2 + \color{blue}{a \cdot \left(\frac{1}{2} + a \cdot \left(\frac{1}{8} + \frac{-1}{192} \cdot {a}^{2}\right)\right)} \]
                      7. Step-by-step derivation
                        1. Applied rewrites63.2%

                          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, -0.005208333333333333, 0.125\right), a, 0.5\right), \color{blue}{a}, \log 2\right) \]
                      8. Recombined 2 regimes into one program.
                      9. Final simplification53.3%

                        \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -2.6:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(a \cdot a, -0.005208333333333333, 0.125\right), a, 0.5\right), a, \log 2\right)\\ \end{array} \]
                      10. Add Preprocessing

                      Alternative 6: 57.0% accurate, 2.4× speedup?

                      \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\mathsf{fma}\left(0.5, a, 1\right), a, 1\right) + \left(1 + b\right)\right)\\ \end{array} \end{array} \]
                      NOTE: a and b should be sorted in increasing order before calling this function.
                      (FPCore (a b)
                       :precision binary64
                       (if (<= a -132.0) (* 0.5 b) (log (+ (fma (fma 0.5 a 1.0) a 1.0) (+ 1.0 b)))))
                      assert(a < b);
                      double code(double a, double b) {
                      	double tmp;
                      	if (a <= -132.0) {
                      		tmp = 0.5 * b;
                      	} else {
                      		tmp = log((fma(fma(0.5, a, 1.0), a, 1.0) + (1.0 + b)));
                      	}
                      	return tmp;
                      }
                      
                      a, b = sort([a, b])
                      function code(a, b)
                      	tmp = 0.0
                      	if (a <= -132.0)
                      		tmp = Float64(0.5 * b);
                      	else
                      		tmp = log(Float64(fma(fma(0.5, a, 1.0), a, 1.0) + Float64(1.0 + b)));
                      	end
                      	return tmp
                      end
                      
                      NOTE: a and b should be sorted in increasing order before calling this function.
                      code[a_, b_] := If[LessEqual[a, -132.0], N[(0.5 * b), $MachinePrecision], N[Log[N[(N[(N[(0.5 * a + 1.0), $MachinePrecision] * a + 1.0), $MachinePrecision] + N[(1.0 + b), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]
                      
                      \begin{array}{l}
                      [a, b] = \mathsf{sort}([a, b])\\
                      \\
                      \begin{array}{l}
                      \mathbf{if}\;a \leq -132:\\
                      \;\;\;\;0.5 \cdot b\\
                      
                      \mathbf{else}:\\
                      \;\;\;\;\log \left(\mathsf{fma}\left(\mathsf{fma}\left(0.5, a, 1\right), a, 1\right) + \left(1 + b\right)\right)\\
                      
                      
                      \end{array}
                      \end{array}
                      
                      Derivation
                      1. Split input into 2 regimes
                      2. if a < -132

                        1. Initial program 5.9%

                          \[\log \left(e^{a} + e^{b}\right) \]
                        2. Add Preprocessing
                        3. Step-by-step derivation
                          1. lift-+.f64N/A

                            \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                          2. lift-exp.f64N/A

                            \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                          3. sinh-+-cosh-revN/A

                            \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                          4. flip-+N/A

                            \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                          5. sinh-coshN/A

                            \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                          6. sinh-coshN/A

                            \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                          7. sinh---cosh-revN/A

                            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                          8. lift-exp.f64N/A

                            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                          9. sinh-+-cosh-revN/A

                            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                          10. flip-+N/A

                            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                          11. sinh---cosh-revN/A

                            \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                          12. frac-addN/A

                            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                          13. lower-/.f64N/A

                            \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                        4. Applied rewrites0.1%

                          \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                        5. Taylor expanded in a around 0

                          \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                        6. Step-by-step derivation
                          1. div-addN/A

                            \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                          2. *-inversesN/A

                            \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                          3. +-commutativeN/A

                            \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                          4. lower-log1p.f64N/A

                            \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                          5. exp-negN/A

                            \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                          6. remove-double-divN/A

                            \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                          7. lower-exp.f643.8

                            \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                        7. Applied rewrites3.8%

                          \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                        8. Taylor expanded in b around 0

                          \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                        9. Step-by-step derivation
                          1. Applied rewrites3.8%

                            \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                          2. Taylor expanded in b around inf

                            \[\leadsto \frac{1}{2} \cdot b \]
                          3. Step-by-step derivation
                            1. Applied rewrites18.8%

                              \[\leadsto 0.5 \cdot b \]

                            if -132 < a

                            1. Initial program 67.0%

                              \[\log \left(e^{a} + e^{b}\right) \]
                            2. Add Preprocessing
                            3. Taylor expanded in a around 0

                              \[\leadsto \log \left(\color{blue}{1} + e^{b}\right) \]
                            4. Step-by-step derivation
                              1. Applied rewrites62.8%

                                \[\leadsto \log \left(\color{blue}{1} + e^{b}\right) \]
                              2. Taylor expanded in b around 0

                                \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                              3. Step-by-step derivation
                                1. lower-+.f6460.9

                                  \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                              4. Applied rewrites60.9%

                                \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                              5. Taylor expanded in a around 0

                                \[\leadsto \log \left(\color{blue}{\left(1 + a \cdot \left(1 + \frac{1}{2} \cdot a\right)\right)} + \left(1 + b\right)\right) \]
                              6. Step-by-step derivation
                                1. +-commutativeN/A

                                  \[\leadsto \log \left(\color{blue}{\left(a \cdot \left(1 + \frac{1}{2} \cdot a\right) + 1\right)} + \left(1 + b\right)\right) \]
                                2. *-commutativeN/A

                                  \[\leadsto \log \left(\left(\color{blue}{\left(1 + \frac{1}{2} \cdot a\right) \cdot a} + 1\right) + \left(1 + b\right)\right) \]
                                3. lower-fma.f64N/A

                                  \[\leadsto \log \left(\color{blue}{\mathsf{fma}\left(1 + \frac{1}{2} \cdot a, a, 1\right)} + \left(1 + b\right)\right) \]
                                4. +-commutativeN/A

                                  \[\leadsto \log \left(\mathsf{fma}\left(\color{blue}{\frac{1}{2} \cdot a + 1}, a, 1\right) + \left(1 + b\right)\right) \]
                                5. lower-fma.f6461.9

                                  \[\leadsto \log \left(\mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(0.5, a, 1\right)}, a, 1\right) + \left(1 + b\right)\right) \]
                              7. Applied rewrites61.9%

                                \[\leadsto \log \left(\color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(0.5, a, 1\right), a, 1\right)} + \left(1 + b\right)\right) \]
                            5. Recombined 2 regimes into one program.
                            6. Add Preprocessing

                            Alternative 7: 56.5% accurate, 2.6× speedup?

                            \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, 0.5\right), a, \log 2\right)\\ \end{array} \end{array} \]
                            NOTE: a and b should be sorted in increasing order before calling this function.
                            (FPCore (a b)
                             :precision binary64
                             (if (<= a -132.0) (* 0.5 b) (fma (fma 0.125 a 0.5) a (log 2.0))))
                            assert(a < b);
                            double code(double a, double b) {
                            	double tmp;
                            	if (a <= -132.0) {
                            		tmp = 0.5 * b;
                            	} else {
                            		tmp = fma(fma(0.125, a, 0.5), a, log(2.0));
                            	}
                            	return tmp;
                            }
                            
                            a, b = sort([a, b])
                            function code(a, b)
                            	tmp = 0.0
                            	if (a <= -132.0)
                            		tmp = Float64(0.5 * b);
                            	else
                            		tmp = fma(fma(0.125, a, 0.5), a, log(2.0));
                            	end
                            	return tmp
                            end
                            
                            NOTE: a and b should be sorted in increasing order before calling this function.
                            code[a_, b_] := If[LessEqual[a, -132.0], N[(0.5 * b), $MachinePrecision], N[(N[(0.125 * a + 0.5), $MachinePrecision] * a + N[Log[2.0], $MachinePrecision]), $MachinePrecision]]
                            
                            \begin{array}{l}
                            [a, b] = \mathsf{sort}([a, b])\\
                            \\
                            \begin{array}{l}
                            \mathbf{if}\;a \leq -132:\\
                            \;\;\;\;0.5 \cdot b\\
                            
                            \mathbf{else}:\\
                            \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, 0.5\right), a, \log 2\right)\\
                            
                            
                            \end{array}
                            \end{array}
                            
                            Derivation
                            1. Split input into 2 regimes
                            2. if a < -132

                              1. Initial program 5.9%

                                \[\log \left(e^{a} + e^{b}\right) \]
                              2. Add Preprocessing
                              3. Step-by-step derivation
                                1. lift-+.f64N/A

                                  \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                2. lift-exp.f64N/A

                                  \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                3. sinh-+-cosh-revN/A

                                  \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                4. flip-+N/A

                                  \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                5. sinh-coshN/A

                                  \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                6. sinh-coshN/A

                                  \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                7. sinh---cosh-revN/A

                                  \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                8. lift-exp.f64N/A

                                  \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                9. sinh-+-cosh-revN/A

                                  \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                10. flip-+N/A

                                  \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                11. sinh---cosh-revN/A

                                  \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                12. frac-addN/A

                                  \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                13. lower-/.f64N/A

                                  \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                              4. Applied rewrites0.1%

                                \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                              5. Taylor expanded in a around 0

                                \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                              6. Step-by-step derivation
                                1. div-addN/A

                                  \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                2. *-inversesN/A

                                  \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                3. +-commutativeN/A

                                  \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                4. lower-log1p.f64N/A

                                  \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                5. exp-negN/A

                                  \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                6. remove-double-divN/A

                                  \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                7. lower-exp.f643.8

                                  \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                              7. Applied rewrites3.8%

                                \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                              8. Taylor expanded in b around 0

                                \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                              9. Step-by-step derivation
                                1. Applied rewrites3.8%

                                  \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                2. Taylor expanded in b around inf

                                  \[\leadsto \frac{1}{2} \cdot b \]
                                3. Step-by-step derivation
                                  1. Applied rewrites18.8%

                                    \[\leadsto 0.5 \cdot b \]

                                  if -132 < a

                                  1. Initial program 67.0%

                                    \[\log \left(e^{a} + e^{b}\right) \]
                                  2. Add Preprocessing
                                  3. Taylor expanded in b around 0

                                    \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
                                  4. Step-by-step derivation
                                    1. lower-log1p.f64N/A

                                      \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                    2. lower-exp.f6463.8

                                      \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                                  5. Applied rewrites63.8%

                                    \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                  6. Taylor expanded in a around 0

                                    \[\leadsto \log 2 + \color{blue}{a \cdot \left(\frac{1}{2} + \frac{1}{8} \cdot a\right)} \]
                                  7. Step-by-step derivation
                                    1. Applied rewrites63.2%

                                      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(0.125, a, 0.5\right), \color{blue}{a}, \log 2\right) \]
                                  8. Recombined 2 regimes into one program.
                                  9. Final simplification53.3%

                                    \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(0.125, a, 0.5\right), a, \log 2\right)\\ \end{array} \]
                                  10. Add Preprocessing

                                  Alternative 8: 56.8% accurate, 2.6× speedup?

                                  \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -1:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\log \left(\left(1 + a\right) + \left(1 + b\right)\right)\\ \end{array} \end{array} \]
                                  NOTE: a and b should be sorted in increasing order before calling this function.
                                  (FPCore (a b)
                                   :precision binary64
                                   (if (<= a -1.0) (* 0.5 b) (log (+ (+ 1.0 a) (+ 1.0 b)))))
                                  assert(a < b);
                                  double code(double a, double b) {
                                  	double tmp;
                                  	if (a <= -1.0) {
                                  		tmp = 0.5 * b;
                                  	} else {
                                  		tmp = log(((1.0 + a) + (1.0 + b)));
                                  	}
                                  	return tmp;
                                  }
                                  
                                  NOTE: a and b should be sorted in increasing order before calling this function.
                                  real(8) function code(a, b)
                                      real(8), intent (in) :: a
                                      real(8), intent (in) :: b
                                      real(8) :: tmp
                                      if (a <= (-1.0d0)) then
                                          tmp = 0.5d0 * b
                                      else
                                          tmp = log(((1.0d0 + a) + (1.0d0 + b)))
                                      end if
                                      code = tmp
                                  end function
                                  
                                  assert a < b;
                                  public static double code(double a, double b) {
                                  	double tmp;
                                  	if (a <= -1.0) {
                                  		tmp = 0.5 * b;
                                  	} else {
                                  		tmp = Math.log(((1.0 + a) + (1.0 + b)));
                                  	}
                                  	return tmp;
                                  }
                                  
                                  [a, b] = sort([a, b])
                                  def code(a, b):
                                  	tmp = 0
                                  	if a <= -1.0:
                                  		tmp = 0.5 * b
                                  	else:
                                  		tmp = math.log(((1.0 + a) + (1.0 + b)))
                                  	return tmp
                                  
                                  a, b = sort([a, b])
                                  function code(a, b)
                                  	tmp = 0.0
                                  	if (a <= -1.0)
                                  		tmp = Float64(0.5 * b);
                                  	else
                                  		tmp = log(Float64(Float64(1.0 + a) + Float64(1.0 + b)));
                                  	end
                                  	return tmp
                                  end
                                  
                                  a, b = num2cell(sort([a, b])){:}
                                  function tmp_2 = code(a, b)
                                  	tmp = 0.0;
                                  	if (a <= -1.0)
                                  		tmp = 0.5 * b;
                                  	else
                                  		tmp = log(((1.0 + a) + (1.0 + b)));
                                  	end
                                  	tmp_2 = tmp;
                                  end
                                  
                                  NOTE: a and b should be sorted in increasing order before calling this function.
                                  code[a_, b_] := If[LessEqual[a, -1.0], N[(0.5 * b), $MachinePrecision], N[Log[N[(N[(1.0 + a), $MachinePrecision] + N[(1.0 + b), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]]
                                  
                                  \begin{array}{l}
                                  [a, b] = \mathsf{sort}([a, b])\\
                                  \\
                                  \begin{array}{l}
                                  \mathbf{if}\;a \leq -1:\\
                                  \;\;\;\;0.5 \cdot b\\
                                  
                                  \mathbf{else}:\\
                                  \;\;\;\;\log \left(\left(1 + a\right) + \left(1 + b\right)\right)\\
                                  
                                  
                                  \end{array}
                                  \end{array}
                                  
                                  Derivation
                                  1. Split input into 2 regimes
                                  2. if a < -1

                                    1. Initial program 5.9%

                                      \[\log \left(e^{a} + e^{b}\right) \]
                                    2. Add Preprocessing
                                    3. Step-by-step derivation
                                      1. lift-+.f64N/A

                                        \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                      2. lift-exp.f64N/A

                                        \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                      3. sinh-+-cosh-revN/A

                                        \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                      4. flip-+N/A

                                        \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                      5. sinh-coshN/A

                                        \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                      6. sinh-coshN/A

                                        \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                      7. sinh---cosh-revN/A

                                        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                      8. lift-exp.f64N/A

                                        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                      9. sinh-+-cosh-revN/A

                                        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                      10. flip-+N/A

                                        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                      11. sinh---cosh-revN/A

                                        \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                      12. frac-addN/A

                                        \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                      13. lower-/.f64N/A

                                        \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                    4. Applied rewrites0.1%

                                      \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                                    5. Taylor expanded in a around 0

                                      \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                    6. Step-by-step derivation
                                      1. div-addN/A

                                        \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                      2. *-inversesN/A

                                        \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                      3. +-commutativeN/A

                                        \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                      4. lower-log1p.f64N/A

                                        \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                      5. exp-negN/A

                                        \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                      6. remove-double-divN/A

                                        \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                      7. lower-exp.f643.8

                                        \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                    7. Applied rewrites3.8%

                                      \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                                    8. Taylor expanded in b around 0

                                      \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                                    9. Step-by-step derivation
                                      1. Applied rewrites3.8%

                                        \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                      2. Taylor expanded in b around inf

                                        \[\leadsto \frac{1}{2} \cdot b \]
                                      3. Step-by-step derivation
                                        1. Applied rewrites18.8%

                                          \[\leadsto 0.5 \cdot b \]

                                        if -1 < a

                                        1. Initial program 67.0%

                                          \[\log \left(e^{a} + e^{b}\right) \]
                                        2. Add Preprocessing
                                        3. Taylor expanded in a around 0

                                          \[\leadsto \log \left(\color{blue}{1} + e^{b}\right) \]
                                        4. Step-by-step derivation
                                          1. Applied rewrites62.8%

                                            \[\leadsto \log \left(\color{blue}{1} + e^{b}\right) \]
                                          2. Taylor expanded in b around 0

                                            \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                                          3. Step-by-step derivation
                                            1. lower-+.f6460.9

                                              \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                                          4. Applied rewrites60.9%

                                            \[\leadsto \log \left(1 + \color{blue}{\left(1 + b\right)}\right) \]
                                          5. Taylor expanded in a around 0

                                            \[\leadsto \log \left(\color{blue}{\left(1 + a\right)} + \left(1 + b\right)\right) \]
                                          6. Step-by-step derivation
                                            1. lower-+.f6461.5

                                              \[\leadsto \log \left(\color{blue}{\left(1 + a\right)} + \left(1 + b\right)\right) \]
                                          7. Applied rewrites61.5%

                                            \[\leadsto \log \left(\color{blue}{\left(1 + a\right)} + \left(1 + b\right)\right) \]
                                        5. Recombined 2 regimes into one program.
                                        6. Add Preprocessing

                                        Alternative 9: 56.2% accurate, 2.7× speedup?

                                        \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -1.36:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(0.5, a, \log 2\right)\\ \end{array} \end{array} \]
                                        NOTE: a and b should be sorted in increasing order before calling this function.
                                        (FPCore (a b)
                                         :precision binary64
                                         (if (<= a -1.36) (* 0.5 b) (fma 0.5 a (log 2.0))))
                                        assert(a < b);
                                        double code(double a, double b) {
                                        	double tmp;
                                        	if (a <= -1.36) {
                                        		tmp = 0.5 * b;
                                        	} else {
                                        		tmp = fma(0.5, a, log(2.0));
                                        	}
                                        	return tmp;
                                        }
                                        
                                        a, b = sort([a, b])
                                        function code(a, b)
                                        	tmp = 0.0
                                        	if (a <= -1.36)
                                        		tmp = Float64(0.5 * b);
                                        	else
                                        		tmp = fma(0.5, a, log(2.0));
                                        	end
                                        	return tmp
                                        end
                                        
                                        NOTE: a and b should be sorted in increasing order before calling this function.
                                        code[a_, b_] := If[LessEqual[a, -1.36], N[(0.5 * b), $MachinePrecision], N[(0.5 * a + N[Log[2.0], $MachinePrecision]), $MachinePrecision]]
                                        
                                        \begin{array}{l}
                                        [a, b] = \mathsf{sort}([a, b])\\
                                        \\
                                        \begin{array}{l}
                                        \mathbf{if}\;a \leq -1.36:\\
                                        \;\;\;\;0.5 \cdot b\\
                                        
                                        \mathbf{else}:\\
                                        \;\;\;\;\mathsf{fma}\left(0.5, a, \log 2\right)\\
                                        
                                        
                                        \end{array}
                                        \end{array}
                                        
                                        Derivation
                                        1. Split input into 2 regimes
                                        2. if a < -1.3600000000000001

                                          1. Initial program 5.9%

                                            \[\log \left(e^{a} + e^{b}\right) \]
                                          2. Add Preprocessing
                                          3. Step-by-step derivation
                                            1. lift-+.f64N/A

                                              \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                            2. lift-exp.f64N/A

                                              \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                            3. sinh-+-cosh-revN/A

                                              \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                            4. flip-+N/A

                                              \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                            5. sinh-coshN/A

                                              \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                            6. sinh-coshN/A

                                              \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                            7. sinh---cosh-revN/A

                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                            8. lift-exp.f64N/A

                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                            9. sinh-+-cosh-revN/A

                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                            10. flip-+N/A

                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                            11. sinh---cosh-revN/A

                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                            12. frac-addN/A

                                              \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                            13. lower-/.f64N/A

                                              \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                          4. Applied rewrites0.1%

                                            \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                                          5. Taylor expanded in a around 0

                                            \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                          6. Step-by-step derivation
                                            1. div-addN/A

                                              \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                            2. *-inversesN/A

                                              \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                            3. +-commutativeN/A

                                              \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                            4. lower-log1p.f64N/A

                                              \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                            5. exp-negN/A

                                              \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                            6. remove-double-divN/A

                                              \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                            7. lower-exp.f643.8

                                              \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                          7. Applied rewrites3.8%

                                            \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                                          8. Taylor expanded in b around 0

                                            \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                                          9. Step-by-step derivation
                                            1. Applied rewrites3.8%

                                              \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                            2. Taylor expanded in b around inf

                                              \[\leadsto \frac{1}{2} \cdot b \]
                                            3. Step-by-step derivation
                                              1. Applied rewrites18.8%

                                                \[\leadsto 0.5 \cdot b \]

                                              if -1.3600000000000001 < a

                                              1. Initial program 67.0%

                                                \[\log \left(e^{a} + e^{b}\right) \]
                                              2. Add Preprocessing
                                              3. Taylor expanded in b around 0

                                                \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
                                              4. Step-by-step derivation
                                                1. lower-log1p.f64N/A

                                                  \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                                2. lower-exp.f6463.8

                                                  \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                                              5. Applied rewrites63.8%

                                                \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                              6. Taylor expanded in a around 0

                                                \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot a} \]
                                              7. Step-by-step derivation
                                                1. Applied rewrites62.8%

                                                  \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{a}, \log 2\right) \]
                                              8. Recombined 2 regimes into one program.
                                              9. Final simplification53.0%

                                                \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -1.36:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(0.5, a, \log 2\right)\\ \end{array} \]
                                              10. Add Preprocessing

                                              Alternative 10: 56.2% accurate, 2.8× speedup?

                                              \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -1:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(1 + a\right)\\ \end{array} \end{array} \]
                                              NOTE: a and b should be sorted in increasing order before calling this function.
                                              (FPCore (a b) :precision binary64 (if (<= a -1.0) (* 0.5 b) (log1p (+ 1.0 a))))
                                              assert(a < b);
                                              double code(double a, double b) {
                                              	double tmp;
                                              	if (a <= -1.0) {
                                              		tmp = 0.5 * b;
                                              	} else {
                                              		tmp = log1p((1.0 + a));
                                              	}
                                              	return tmp;
                                              }
                                              
                                              assert a < b;
                                              public static double code(double a, double b) {
                                              	double tmp;
                                              	if (a <= -1.0) {
                                              		tmp = 0.5 * b;
                                              	} else {
                                              		tmp = Math.log1p((1.0 + a));
                                              	}
                                              	return tmp;
                                              }
                                              
                                              [a, b] = sort([a, b])
                                              def code(a, b):
                                              	tmp = 0
                                              	if a <= -1.0:
                                              		tmp = 0.5 * b
                                              	else:
                                              		tmp = math.log1p((1.0 + a))
                                              	return tmp
                                              
                                              a, b = sort([a, b])
                                              function code(a, b)
                                              	tmp = 0.0
                                              	if (a <= -1.0)
                                              		tmp = Float64(0.5 * b);
                                              	else
                                              		tmp = log1p(Float64(1.0 + a));
                                              	end
                                              	return tmp
                                              end
                                              
                                              NOTE: a and b should be sorted in increasing order before calling this function.
                                              code[a_, b_] := If[LessEqual[a, -1.0], N[(0.5 * b), $MachinePrecision], N[Log[1 + N[(1.0 + a), $MachinePrecision]], $MachinePrecision]]
                                              
                                              \begin{array}{l}
                                              [a, b] = \mathsf{sort}([a, b])\\
                                              \\
                                              \begin{array}{l}
                                              \mathbf{if}\;a \leq -1:\\
                                              \;\;\;\;0.5 \cdot b\\
                                              
                                              \mathbf{else}:\\
                                              \;\;\;\;\mathsf{log1p}\left(1 + a\right)\\
                                              
                                              
                                              \end{array}
                                              \end{array}
                                              
                                              Derivation
                                              1. Split input into 2 regimes
                                              2. if a < -1

                                                1. Initial program 5.9%

                                                  \[\log \left(e^{a} + e^{b}\right) \]
                                                2. Add Preprocessing
                                                3. Step-by-step derivation
                                                  1. lift-+.f64N/A

                                                    \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                                  2. lift-exp.f64N/A

                                                    \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                                  3. sinh-+-cosh-revN/A

                                                    \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                                  4. flip-+N/A

                                                    \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                                  5. sinh-coshN/A

                                                    \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                  6. sinh-coshN/A

                                                    \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                  7. sinh---cosh-revN/A

                                                    \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                                  8. lift-exp.f64N/A

                                                    \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                                  9. sinh-+-cosh-revN/A

                                                    \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                                  10. flip-+N/A

                                                    \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                                  11. sinh---cosh-revN/A

                                                    \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                                  12. frac-addN/A

                                                    \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                  13. lower-/.f64N/A

                                                    \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                4. Applied rewrites0.1%

                                                  \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                                                5. Taylor expanded in a around 0

                                                  \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                6. Step-by-step derivation
                                                  1. div-addN/A

                                                    \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                  2. *-inversesN/A

                                                    \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                                  3. +-commutativeN/A

                                                    \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                  4. lower-log1p.f64N/A

                                                    \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                  5. exp-negN/A

                                                    \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                                  6. remove-double-divN/A

                                                    \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                  7. lower-exp.f643.8

                                                    \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                7. Applied rewrites3.8%

                                                  \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                                                8. Taylor expanded in b around 0

                                                  \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                                                9. Step-by-step derivation
                                                  1. Applied rewrites3.8%

                                                    \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                                  2. Taylor expanded in b around inf

                                                    \[\leadsto \frac{1}{2} \cdot b \]
                                                  3. Step-by-step derivation
                                                    1. Applied rewrites18.8%

                                                      \[\leadsto 0.5 \cdot b \]

                                                    if -1 < a

                                                    1. Initial program 67.0%

                                                      \[\log \left(e^{a} + e^{b}\right) \]
                                                    2. Add Preprocessing
                                                    3. Taylor expanded in b around 0

                                                      \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
                                                    4. Step-by-step derivation
                                                      1. lower-log1p.f64N/A

                                                        \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                                      2. lower-exp.f6463.8

                                                        \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                                                    5. Applied rewrites63.8%

                                                      \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                                    6. Taylor expanded in a around 0

                                                      \[\leadsto \mathsf{log1p}\left(1 + a\right) \]
                                                    7. Step-by-step derivation
                                                      1. Applied rewrites62.7%

                                                        \[\leadsto \mathsf{log1p}\left(1 + a\right) \]
                                                    8. Recombined 2 regimes into one program.
                                                    9. Final simplification52.9%

                                                      \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -1:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(1 + a\right)\\ \end{array} \]
                                                    10. Add Preprocessing

                                                    Alternative 11: 55.7% accurate, 2.8× speedup?

                                                    \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(1\right)\\ \end{array} \end{array} \]
                                                    NOTE: a and b should be sorted in increasing order before calling this function.
                                                    (FPCore (a b) :precision binary64 (if (<= a -132.0) (* 0.5 b) (log1p 1.0)))
                                                    assert(a < b);
                                                    double code(double a, double b) {
                                                    	double tmp;
                                                    	if (a <= -132.0) {
                                                    		tmp = 0.5 * b;
                                                    	} else {
                                                    		tmp = log1p(1.0);
                                                    	}
                                                    	return tmp;
                                                    }
                                                    
                                                    assert a < b;
                                                    public static double code(double a, double b) {
                                                    	double tmp;
                                                    	if (a <= -132.0) {
                                                    		tmp = 0.5 * b;
                                                    	} else {
                                                    		tmp = Math.log1p(1.0);
                                                    	}
                                                    	return tmp;
                                                    }
                                                    
                                                    [a, b] = sort([a, b])
                                                    def code(a, b):
                                                    	tmp = 0
                                                    	if a <= -132.0:
                                                    		tmp = 0.5 * b
                                                    	else:
                                                    		tmp = math.log1p(1.0)
                                                    	return tmp
                                                    
                                                    a, b = sort([a, b])
                                                    function code(a, b)
                                                    	tmp = 0.0
                                                    	if (a <= -132.0)
                                                    		tmp = Float64(0.5 * b);
                                                    	else
                                                    		tmp = log1p(1.0);
                                                    	end
                                                    	return tmp
                                                    end
                                                    
                                                    NOTE: a and b should be sorted in increasing order before calling this function.
                                                    code[a_, b_] := If[LessEqual[a, -132.0], N[(0.5 * b), $MachinePrecision], N[Log[1 + 1.0], $MachinePrecision]]
                                                    
                                                    \begin{array}{l}
                                                    [a, b] = \mathsf{sort}([a, b])\\
                                                    \\
                                                    \begin{array}{l}
                                                    \mathbf{if}\;a \leq -132:\\
                                                    \;\;\;\;0.5 \cdot b\\
                                                    
                                                    \mathbf{else}:\\
                                                    \;\;\;\;\mathsf{log1p}\left(1\right)\\
                                                    
                                                    
                                                    \end{array}
                                                    \end{array}
                                                    
                                                    Derivation
                                                    1. Split input into 2 regimes
                                                    2. if a < -132

                                                      1. Initial program 5.9%

                                                        \[\log \left(e^{a} + e^{b}\right) \]
                                                      2. Add Preprocessing
                                                      3. Step-by-step derivation
                                                        1. lift-+.f64N/A

                                                          \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                                        2. lift-exp.f64N/A

                                                          \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                                        3. sinh-+-cosh-revN/A

                                                          \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                                        4. flip-+N/A

                                                          \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                                        5. sinh-coshN/A

                                                          \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                        6. sinh-coshN/A

                                                          \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                        7. sinh---cosh-revN/A

                                                          \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                                        8. lift-exp.f64N/A

                                                          \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                                        9. sinh-+-cosh-revN/A

                                                          \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                                        10. flip-+N/A

                                                          \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                                        11. sinh---cosh-revN/A

                                                          \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                                        12. frac-addN/A

                                                          \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                        13. lower-/.f64N/A

                                                          \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                      4. Applied rewrites0.1%

                                                        \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                                                      5. Taylor expanded in a around 0

                                                        \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                      6. Step-by-step derivation
                                                        1. div-addN/A

                                                          \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                        2. *-inversesN/A

                                                          \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                                        3. +-commutativeN/A

                                                          \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                        4. lower-log1p.f64N/A

                                                          \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                        5. exp-negN/A

                                                          \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                                        6. remove-double-divN/A

                                                          \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                        7. lower-exp.f643.8

                                                          \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                      7. Applied rewrites3.8%

                                                        \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                                                      8. Taylor expanded in b around 0

                                                        \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                                                      9. Step-by-step derivation
                                                        1. Applied rewrites3.8%

                                                          \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                                        2. Taylor expanded in b around inf

                                                          \[\leadsto \frac{1}{2} \cdot b \]
                                                        3. Step-by-step derivation
                                                          1. Applied rewrites18.8%

                                                            \[\leadsto 0.5 \cdot b \]

                                                          if -132 < a

                                                          1. Initial program 67.0%

                                                            \[\log \left(e^{a} + e^{b}\right) \]
                                                          2. Add Preprocessing
                                                          3. Taylor expanded in b around 0

                                                            \[\leadsto \color{blue}{\log \left(1 + e^{a}\right)} \]
                                                          4. Step-by-step derivation
                                                            1. lower-log1p.f64N/A

                                                              \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                                            2. lower-exp.f6463.8

                                                              \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{a}}\right) \]
                                                          5. Applied rewrites63.8%

                                                            \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{a}\right)} \]
                                                          6. Taylor expanded in a around 0

                                                            \[\leadsto \mathsf{log1p}\left(1\right) \]
                                                          7. Step-by-step derivation
                                                            1. Applied rewrites62.2%

                                                              \[\leadsto \mathsf{log1p}\left(1\right) \]
                                                          8. Recombined 2 regimes into one program.
                                                          9. Final simplification52.5%

                                                            \[\leadsto \begin{array}{l} \mathbf{if}\;a \leq -132:\\ \;\;\;\;0.5 \cdot b\\ \mathbf{else}:\\ \;\;\;\;\mathsf{log1p}\left(1\right)\\ \end{array} \]
                                                          10. Add Preprocessing

                                                          Alternative 12: 12.0% accurate, 50.7× speedup?

                                                          \[\begin{array}{l} [a, b] = \mathsf{sort}([a, b])\\ \\ 0.5 \cdot b \end{array} \]
                                                          NOTE: a and b should be sorted in increasing order before calling this function.
                                                          (FPCore (a b) :precision binary64 (* 0.5 b))
                                                          assert(a < b);
                                                          double code(double a, double b) {
                                                          	return 0.5 * b;
                                                          }
                                                          
                                                          NOTE: a and b should be sorted in increasing order before calling this function.
                                                          real(8) function code(a, b)
                                                              real(8), intent (in) :: a
                                                              real(8), intent (in) :: b
                                                              code = 0.5d0 * b
                                                          end function
                                                          
                                                          assert a < b;
                                                          public static double code(double a, double b) {
                                                          	return 0.5 * b;
                                                          }
                                                          
                                                          [a, b] = sort([a, b])
                                                          def code(a, b):
                                                          	return 0.5 * b
                                                          
                                                          a, b = sort([a, b])
                                                          function code(a, b)
                                                          	return Float64(0.5 * b)
                                                          end
                                                          
                                                          a, b = num2cell(sort([a, b])){:}
                                                          function tmp = code(a, b)
                                                          	tmp = 0.5 * b;
                                                          end
                                                          
                                                          NOTE: a and b should be sorted in increasing order before calling this function.
                                                          code[a_, b_] := N[(0.5 * b), $MachinePrecision]
                                                          
                                                          \begin{array}{l}
                                                          [a, b] = \mathsf{sort}([a, b])\\
                                                          \\
                                                          0.5 \cdot b
                                                          \end{array}
                                                          
                                                          Derivation
                                                          1. Initial program 53.4%

                                                            \[\log \left(e^{a} + e^{b}\right) \]
                                                          2. Add Preprocessing
                                                          3. Step-by-step derivation
                                                            1. lift-+.f64N/A

                                                              \[\leadsto \log \color{blue}{\left(e^{a} + e^{b}\right)} \]
                                                            2. lift-exp.f64N/A

                                                              \[\leadsto \log \left(\color{blue}{e^{a}} + e^{b}\right) \]
                                                            3. sinh-+-cosh-revN/A

                                                              \[\leadsto \log \left(\color{blue}{\left(\cosh a + \sinh a\right)} + e^{b}\right) \]
                                                            4. flip-+N/A

                                                              \[\leadsto \log \left(\color{blue}{\frac{\cosh a \cdot \cosh a - \sinh a \cdot \sinh a}{\cosh a - \sinh a}} + e^{b}\right) \]
                                                            5. sinh-coshN/A

                                                              \[\leadsto \log \left(\frac{\color{blue}{1}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                            6. sinh-coshN/A

                                                              \[\leadsto \log \left(\frac{\color{blue}{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}}{\cosh a - \sinh a} + e^{b}\right) \]
                                                            7. sinh---cosh-revN/A

                                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(a\right)}}} + e^{b}\right) \]
                                                            8. lift-exp.f64N/A

                                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{e^{b}}\right) \]
                                                            9. sinh-+-cosh-revN/A

                                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\left(\cosh b + \sinh b\right)}\right) \]
                                                            10. flip-+N/A

                                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \color{blue}{\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\cosh b - \sinh b}}\right) \]
                                                            11. sinh---cosh-revN/A

                                                              \[\leadsto \log \left(\frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{e^{\mathsf{neg}\left(a\right)}} + \frac{\cosh b \cdot \cosh b - \sinh b \cdot \sinh b}{\color{blue}{e^{\mathsf{neg}\left(b\right)}}}\right) \]
                                                            12. frac-addN/A

                                                              \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                            13. lower-/.f64N/A

                                                              \[\leadsto \log \color{blue}{\left(\frac{\left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right) \cdot e^{\mathsf{neg}\left(b\right)} + e^{\mathsf{neg}\left(a\right)} \cdot \left(\cosh b \cdot \cosh b - \sinh b \cdot \sinh b\right)}{e^{\mathsf{neg}\left(a\right)} \cdot e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                          4. Applied rewrites48.9%

                                                            \[\leadsto \log \color{blue}{\left(\frac{\mathsf{fma}\left(1, e^{-b}, e^{-a} \cdot 1\right)}{e^{\left(-a\right) + \left(-b\right)}}\right)} \]
                                                          5. Taylor expanded in a around 0

                                                            \[\leadsto \color{blue}{\log \left(\frac{1 + e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                          6. Step-by-step derivation
                                                            1. div-addN/A

                                                              \[\leadsto \log \color{blue}{\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \frac{e^{\mathsf{neg}\left(b\right)}}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                            2. *-inversesN/A

                                                              \[\leadsto \log \left(\frac{1}{e^{\mathsf{neg}\left(b\right)}} + \color{blue}{1}\right) \]
                                                            3. +-commutativeN/A

                                                              \[\leadsto \log \color{blue}{\left(1 + \frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                            4. lower-log1p.f64N/A

                                                              \[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{e^{\mathsf{neg}\left(b\right)}}\right)} \]
                                                            5. exp-negN/A

                                                              \[\leadsto \mathsf{log1p}\left(\frac{1}{\color{blue}{\frac{1}{e^{b}}}}\right) \]
                                                            6. remove-double-divN/A

                                                              \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                            7. lower-exp.f6450.1

                                                              \[\leadsto \mathsf{log1p}\left(\color{blue}{e^{b}}\right) \]
                                                          7. Applied rewrites50.1%

                                                            \[\leadsto \color{blue}{\mathsf{log1p}\left(e^{b}\right)} \]
                                                          8. Taylor expanded in b around 0

                                                            \[\leadsto \log 2 + \color{blue}{\frac{1}{2} \cdot b} \]
                                                          9. Step-by-step derivation
                                                            1. Applied rewrites48.9%

                                                              \[\leadsto \mathsf{fma}\left(0.5, \color{blue}{b}, \log 2\right) \]
                                                            2. Taylor expanded in b around inf

                                                              \[\leadsto \frac{1}{2} \cdot b \]
                                                            3. Step-by-step derivation
                                                              1. Applied rewrites6.8%

                                                                \[\leadsto 0.5 \cdot b \]
                                                              2. Add Preprocessing

                                                              Reproduce

                                                              ?
                                                              herbie shell --seed 2024343 
                                                              (FPCore (a b)
                                                                :name "symmetry log of sum of exp"
                                                                :precision binary64
                                                                (log (+ (exp a) (exp b))))