?

Average Accuracy: 29.4% → 98.8%
Time: 5.2s
Precision: binary64
Cost: 72328

?

\[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
\[\begin{array}{l} t_0 := \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right)\\ \mathbf{if}\;t_0 \leq -10:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 + \frac{-0.5}{x}}\right), x\right)\\ \mathbf{elif}\;t_0 \leq 5 \cdot 10^{-6}:\\ \;\;\;\;\mathsf{copysign}\left(-0.16666666666666666 \cdot {x}^{3} + \left(x + 0.075 \cdot {x}^{5}\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]
(FPCore (x)
 :precision binary64
 (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1.0)))) x))
(FPCore (x)
 :precision binary64
 (let* ((t_0 (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1.0)))) x)))
   (if (<= t_0 -10.0)
     (copysign (log (/ 1.0 (+ (* x -2.0) (/ -0.5 x)))) x)
     (if (<= t_0 5e-6)
       (copysign
        (+ (* -0.16666666666666666 (pow x 3.0)) (+ x (* 0.075 (pow x 5.0))))
        x)
       (copysign (log (+ x x)) x)))))
double code(double x) {
	return copysign(log((fabs(x) + sqrt(((x * x) + 1.0)))), x);
}
double code(double x) {
	double t_0 = copysign(log((fabs(x) + sqrt(((x * x) + 1.0)))), x);
	double tmp;
	if (t_0 <= -10.0) {
		tmp = copysign(log((1.0 / ((x * -2.0) + (-0.5 / x)))), x);
	} else if (t_0 <= 5e-6) {
		tmp = copysign(((-0.16666666666666666 * pow(x, 3.0)) + (x + (0.075 * pow(x, 5.0)))), x);
	} else {
		tmp = copysign(log((x + x)), x);
	}
	return tmp;
}
public static double code(double x) {
	return Math.copySign(Math.log((Math.abs(x) + Math.sqrt(((x * x) + 1.0)))), x);
}
public static double code(double x) {
	double t_0 = Math.copySign(Math.log((Math.abs(x) + Math.sqrt(((x * x) + 1.0)))), x);
	double tmp;
	if (t_0 <= -10.0) {
		tmp = Math.copySign(Math.log((1.0 / ((x * -2.0) + (-0.5 / x)))), x);
	} else if (t_0 <= 5e-6) {
		tmp = Math.copySign(((-0.16666666666666666 * Math.pow(x, 3.0)) + (x + (0.075 * Math.pow(x, 5.0)))), x);
	} else {
		tmp = Math.copySign(Math.log((x + x)), x);
	}
	return tmp;
}
def code(x):
	return math.copysign(math.log((math.fabs(x) + math.sqrt(((x * x) + 1.0)))), x)
def code(x):
	t_0 = math.copysign(math.log((math.fabs(x) + math.sqrt(((x * x) + 1.0)))), x)
	tmp = 0
	if t_0 <= -10.0:
		tmp = math.copysign(math.log((1.0 / ((x * -2.0) + (-0.5 / x)))), x)
	elif t_0 <= 5e-6:
		tmp = math.copysign(((-0.16666666666666666 * math.pow(x, 3.0)) + (x + (0.075 * math.pow(x, 5.0)))), x)
	else:
		tmp = math.copysign(math.log((x + x)), x)
	return tmp
function code(x)
	return copysign(log(Float64(abs(x) + sqrt(Float64(Float64(x * x) + 1.0)))), x)
end
function code(x)
	t_0 = copysign(log(Float64(abs(x) + sqrt(Float64(Float64(x * x) + 1.0)))), x)
	tmp = 0.0
	if (t_0 <= -10.0)
		tmp = copysign(log(Float64(1.0 / Float64(Float64(x * -2.0) + Float64(-0.5 / x)))), x);
	elseif (t_0 <= 5e-6)
		tmp = copysign(Float64(Float64(-0.16666666666666666 * (x ^ 3.0)) + Float64(x + Float64(0.075 * (x ^ 5.0)))), x);
	else
		tmp = copysign(log(Float64(x + x)), x);
	end
	return tmp
end
function tmp = code(x)
	tmp = sign(x) * abs(log((abs(x) + sqrt(((x * x) + 1.0)))));
end
function tmp_2 = code(x)
	t_0 = sign(x) * abs(log((abs(x) + sqrt(((x * x) + 1.0)))));
	tmp = 0.0;
	if (t_0 <= -10.0)
		tmp = sign(x) * abs(log((1.0 / ((x * -2.0) + (-0.5 / x)))));
	elseif (t_0 <= 5e-6)
		tmp = sign(x) * abs(((-0.16666666666666666 * (x ^ 3.0)) + (x + (0.075 * (x ^ 5.0)))));
	else
		tmp = sign(x) * abs(log((x + x)));
	end
	tmp_2 = tmp;
end
code[x_] := N[With[{TMP1 = Abs[N[Log[N[(N[Abs[x], $MachinePrecision] + N[Sqrt[N[(N[(x * x), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]
code[x_] := Block[{t$95$0 = N[With[{TMP1 = Abs[N[Log[N[(N[Abs[x], $MachinePrecision] + N[Sqrt[N[(N[(x * x), $MachinePrecision] + 1.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]}, If[LessEqual[t$95$0, -10.0], N[With[{TMP1 = Abs[N[Log[N[(1.0 / N[(N[(x * -2.0), $MachinePrecision] + N[(-0.5 / x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision], If[LessEqual[t$95$0, 5e-6], N[With[{TMP1 = Abs[N[(N[(-0.16666666666666666 * N[Power[x, 3.0], $MachinePrecision]), $MachinePrecision] + N[(x + N[(0.075 * N[Power[x, 5.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision], N[With[{TMP1 = Abs[N[Log[N[(x + x), $MachinePrecision]], $MachinePrecision]], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision]]]]
\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right)
\begin{array}{l}
t_0 := \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right)\\
\mathbf{if}\;t_0 \leq -10:\\
\;\;\;\;\mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 + \frac{-0.5}{x}}\right), x\right)\\

\mathbf{elif}\;t_0 \leq 5 \cdot 10^{-6}:\\
\;\;\;\;\mathsf{copysign}\left(-0.16666666666666666 \cdot {x}^{3} + \left(x + 0.075 \cdot {x}^{5}\right), x\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\


\end{array}

Error?

Target

Original29.4%
Target99.9%
Herbie98.8%
\[\mathsf{copysign}\left(\mathsf{log1p}\left(\left|x\right| + \frac{\left|x\right|}{\mathsf{hypot}\left(1, \frac{1}{\left|x\right|}\right) + \frac{1}{\left|x\right|}}\right), x\right) \]

Derivation?

  1. Split input into 3 regimes
  2. if (copysign.f64 (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) 1)))) x) < -10

    1. Initial program 48.1%

      \[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
    2. Simplified99.9%

      \[\leadsto \color{blue}{\mathsf{copysign}\left(\log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right)} \]
      Proof

      [Start]48.1

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]

      +-commutative [=>]48.1

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{\color{blue}{1 + x \cdot x}}\right), x\right) \]

      hypot-1-def [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \color{blue}{\mathsf{hypot}\left(1, x\right)}\right), x\right) \]
    3. Applied egg-rr0.6%

      \[\leadsto \mathsf{copysign}\left(\log \color{blue}{\left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{1 + x \cdot x}{x - \mathsf{hypot}\left(1, x\right)}\right)}, x\right) \]
      Proof

      [Start]99.9

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      flip-+ [=>]0.6

      \[ \mathsf{copysign}\left(\log \color{blue}{\left(\frac{\left|x\right| \cdot \left|x\right| - \mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right)}, x\right) \]

      div-sub [=>]0.5

      \[ \mathsf{copysign}\left(\log \color{blue}{\left(\frac{\left|x\right| \cdot \left|x\right|}{\left|x\right| - \mathsf{hypot}\left(1, x\right)} - \frac{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right)}, x\right) \]

      sqr-abs [=>]0.5

      \[ \mathsf{copysign}\left(\log \left(\frac{\color{blue}{x \cdot x}}{\left|x\right| - \mathsf{hypot}\left(1, x\right)} - \frac{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      add-sqr-sqrt [=>]0.0

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{\left|\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right| - \mathsf{hypot}\left(1, x\right)} - \frac{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      fabs-sqr [=>]0.0

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{\color{blue}{\sqrt{x} \cdot \sqrt{x}} - \mathsf{hypot}\left(1, x\right)} - \frac{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      add-sqr-sqrt [<=]0.2

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{\color{blue}{x} - \mathsf{hypot}\left(1, x\right)} - \frac{\mathsf{hypot}\left(1, x\right) \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      hypot-udef [=>]0.2

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{\color{blue}{\sqrt{1 \cdot 1 + x \cdot x}} \cdot \mathsf{hypot}\left(1, x\right)}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      hypot-udef [=>]0.2

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{\sqrt{1 \cdot 1 + x \cdot x} \cdot \color{blue}{\sqrt{1 \cdot 1 + x \cdot x}}}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      add-sqr-sqrt [<=]0.2

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{\color{blue}{1 \cdot 1 + x \cdot x}}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      metadata-eval [=>]0.2

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{\color{blue}{1} + x \cdot x}{\left|x\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      add-sqr-sqrt [=>]0.0

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{1 + x \cdot x}{\left|\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right| - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      fabs-sqr [=>]0.0

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{1 + x \cdot x}{\color{blue}{\sqrt{x} \cdot \sqrt{x}} - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      add-sqr-sqrt [<=]0.6

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{1 + x \cdot x}{\color{blue}{x} - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]
    4. Simplified99.9%

      \[\leadsto \mathsf{copysign}\left(\log \color{blue}{\left(\frac{1}{\mathsf{hypot}\left(1, x\right) - x}\right)}, x\right) \]
      Proof

      [Start]0.6

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x}{x - \mathsf{hypot}\left(1, x\right)} - \frac{1 + x \cdot x}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      div-sub [<=]1.3

      \[ \mathsf{copysign}\left(\log \color{blue}{\left(\frac{x \cdot x - \left(1 + x \cdot x\right)}{x - \mathsf{hypot}\left(1, x\right)}\right)}, x\right) \]

      +-commutative [=>]1.3

      \[ \mathsf{copysign}\left(\log \left(\frac{x \cdot x - \color{blue}{\left(x \cdot x + 1\right)}}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      associate--r+ [=>]48.1

      \[ \mathsf{copysign}\left(\log \left(\frac{\color{blue}{\left(x \cdot x - x \cdot x\right) - 1}}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      +-inverses [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{\color{blue}{0} - 1}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      metadata-eval [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{\color{blue}{-1}}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      metadata-eval [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{\color{blue}{\frac{1}{-1}}}{x - \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      associate-/r* [<=]99.9

      \[ \mathsf{copysign}\left(\log \color{blue}{\left(\frac{1}{-1 \cdot \left(x - \mathsf{hypot}\left(1, x\right)\right)}\right)}, x\right) \]

      neg-mul-1 [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{-\left(x - \mathsf{hypot}\left(1, x\right)\right)}}\right), x\right) \]

      neg-sub0 [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{0 - \left(x - \mathsf{hypot}\left(1, x\right)\right)}}\right), x\right) \]

      associate--r- [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{\left(0 - x\right) + \mathsf{hypot}\left(1, x\right)}}\right), x\right) \]

      neg-sub0 [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{\left(-x\right)} + \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      mul-1-neg [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{-1 \cdot x} + \mathsf{hypot}\left(1, x\right)}\right), x\right) \]

      +-commutative [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{\mathsf{hypot}\left(1, x\right) + -1 \cdot x}}\right), x\right) \]

      mul-1-neg [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\mathsf{hypot}\left(1, x\right) + \color{blue}{\left(-x\right)}}\right), x\right) \]

      sub-neg [<=]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{\mathsf{hypot}\left(1, x\right) - x}}\right), x\right) \]
    5. Taylor expanded in x around -inf 99.9%

      \[\leadsto \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{-2 \cdot x - 0.5 \cdot \frac{1}{x}}}\right), x\right) \]
    6. Simplified99.9%

      \[\leadsto \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{x \cdot -2 - \frac{0.5}{x}}}\right), x\right) \]
      Proof

      [Start]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{-2 \cdot x - 0.5 \cdot \frac{1}{x}}\right), x\right) \]

      *-commutative [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{\color{blue}{x \cdot -2} - 0.5 \cdot \frac{1}{x}}\right), x\right) \]

      associate-*r/ [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 - \color{blue}{\frac{0.5 \cdot 1}{x}}}\right), x\right) \]

      metadata-eval [=>]99.9

      \[ \mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 - \frac{\color{blue}{0.5}}{x}}\right), x\right) \]

    if -10 < (copysign.f64 (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) 1)))) x) < 5.00000000000000041e-6

    1. Initial program 8.8%

      \[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
    2. Simplified8.8%

      \[\leadsto \color{blue}{\mathsf{copysign}\left(\log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right)} \]
      Proof

      [Start]8.8

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]

      +-commutative [=>]8.8

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{\color{blue}{1 + x \cdot x}}\right), x\right) \]

      hypot-1-def [=>]8.8

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \color{blue}{\mathsf{hypot}\left(1, x\right)}\right), x\right) \]
    3. Applied egg-rr8.7%

      \[\leadsto \mathsf{copysign}\left(\color{blue}{0 + \log \left(x + \mathsf{hypot}\left(1, x\right)\right)}, x\right) \]
      Proof

      [Start]8.8

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      *-un-lft-identity [=>]8.8

      \[ \mathsf{copysign}\left(\log \color{blue}{\left(1 \cdot \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right)\right)}, x\right) \]

      log-prod [=>]8.8

      \[ \mathsf{copysign}\left(\color{blue}{\log 1 + \log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right)}, x\right) \]

      metadata-eval [=>]8.8

      \[ \mathsf{copysign}\left(\color{blue}{0} + \log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      add-sqr-sqrt [=>]3.4

      \[ \mathsf{copysign}\left(0 + \log \left(\left|\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right| + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      fabs-sqr [=>]3.4

      \[ \mathsf{copysign}\left(0 + \log \left(\color{blue}{\sqrt{x} \cdot \sqrt{x}} + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      add-sqr-sqrt [<=]8.7

      \[ \mathsf{copysign}\left(0 + \log \left(\color{blue}{x} + \mathsf{hypot}\left(1, x\right)\right), x\right) \]
    4. Simplified8.7%

      \[\leadsto \mathsf{copysign}\left(\color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}, x\right) \]
      Proof

      [Start]8.7

      \[ \mathsf{copysign}\left(0 + \log \left(x + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

      +-lft-identity [=>]8.7

      \[ \mathsf{copysign}\left(\color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}, x\right) \]
    5. Taylor expanded in x around 0 99.1%

      \[\leadsto \mathsf{copysign}\left(\color{blue}{-0.16666666666666666 \cdot {x}^{3} + \left(0.075 \cdot {x}^{5} + x\right)}, x\right) \]

    if 5.00000000000000041e-6 < (copysign.f64 (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) 1)))) x)

    1. Initial program 52.1%

      \[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
    2. Simplified99.5%

      \[\leadsto \color{blue}{\mathsf{copysign}\left(\log \left(\left|x\right| + \mathsf{hypot}\left(1, x\right)\right), x\right)} \]
      Proof

      [Start]52.1

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]

      +-commutative [=>]52.1

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{\color{blue}{1 + x \cdot x}}\right), x\right) \]

      hypot-1-def [=>]99.5

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + \color{blue}{\mathsf{hypot}\left(1, x\right)}\right), x\right) \]
    3. Taylor expanded in x around inf 97.1%

      \[\leadsto \mathsf{copysign}\left(\log \color{blue}{\left(\left|x\right| + x\right)}, x\right) \]
    4. Simplified97.1%

      \[\leadsto \mathsf{copysign}\left(\log \color{blue}{\left(x + x\right)}, x\right) \]
      Proof

      [Start]97.1

      \[ \mathsf{copysign}\left(\log \left(\left|x\right| + x\right), x\right) \]

      rem-square-sqrt [<=]97.1

      \[ \mathsf{copysign}\left(\log \left(\left|\color{blue}{\sqrt{x} \cdot \sqrt{x}}\right| + x\right), x\right) \]

      fabs-sqr [=>]97.1

      \[ \mathsf{copysign}\left(\log \left(\color{blue}{\sqrt{x} \cdot \sqrt{x}} + x\right), x\right) \]

      rem-square-sqrt [=>]97.1

      \[ \mathsf{copysign}\left(\log \left(\color{blue}{x} + x\right), x\right) \]
  3. Recombined 3 regimes into one program.
  4. Final simplification98.8%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \leq -10:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 + \frac{-0.5}{x}}\right), x\right)\\ \mathbf{elif}\;\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \leq 5 \cdot 10^{-6}:\\ \;\;\;\;\mathsf{copysign}\left(-0.16666666666666666 \cdot {x}^{3} + \left(x + 0.075 \cdot {x}^{5}\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy99.3%
Cost13572
\[\begin{array}{l} \mathbf{if}\;x \leq -0.95:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(\frac{1}{x \cdot -2 + \frac{-0.5}{x}}\right), x\right)\\ \mathbf{elif}\;x \leq 1.25:\\ \;\;\;\;\mathsf{copysign}\left(x + -0.16666666666666666 \cdot {x}^{3}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]
Alternative 2
Accuracy99.2%
Cost13512
\[\begin{array}{l} \mathbf{if}\;x \leq -1.25:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(\frac{-0.5}{x}\right), x\right)\\ \mathbf{elif}\;x \leq 1.25:\\ \;\;\;\;\mathsf{copysign}\left(x + -0.16666666666666666 \cdot {x}^{3}, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]
Alternative 3
Accuracy81.8%
Cost13320
\[\begin{array}{l} \mathbf{if}\;x \leq -3.2:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(-x\right), x\right)\\ \mathbf{elif}\;x \leq 1.25:\\ \;\;\;\;\mathsf{copysign}\left(x, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]
Alternative 4
Accuracy98.9%
Cost13320
\[\begin{array}{l} \mathbf{if}\;x \leq -1.25:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(\frac{-0.5}{x}\right), x\right)\\ \mathbf{elif}\;x \leq 1.25:\\ \;\;\;\;\mathsf{copysign}\left(x, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + x\right), x\right)\\ \end{array} \]
Alternative 5
Accuracy64.6%
Cost13124
\[\begin{array}{l} \mathbf{if}\;x \leq -1:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(-x\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\mathsf{log1p}\left(x\right), x\right)\\ \end{array} \]
Alternative 6
Accuracy58.6%
Cost13060
\[\begin{array}{l} \mathbf{if}\;x \leq 1.6:\\ \;\;\;\;\mathsf{copysign}\left(x, x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\mathsf{log1p}\left(x\right), x\right)\\ \end{array} \]
Alternative 7
Accuracy52.3%
Cost6528
\[\mathsf{copysign}\left(x, x\right) \]

Error

Reproduce?

herbie shell --seed 2023130 
(FPCore (x)
  :name "Rust f64::asinh"
  :precision binary64

  :herbie-target
  (copysign (log1p (+ (fabs x) (/ (fabs x) (+ (hypot 1.0 (/ 1.0 (fabs x))) (/ 1.0 (fabs x)))))) x)

  (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1.0)))) x))