Average Error: 44.8 → 0.4
Time: 5.4s
Precision: binary64
Cost: 45828
\[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
\[\begin{array}{l} \mathbf{if}\;\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \leq -0.5:\\ \;\;\;\;\mathsf{copysign}\left(-\log \left(\mathsf{hypot}\left(1, x\right) - x\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\mathsf{log1p}\left(x + \left(\mathsf{hypot}\left(1, x\right) + -1\right)\right), x\right)\\ \end{array} \]
(FPCore (x)
 :precision binary64
 (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1.0)))) x))
(FPCore (x)
 :precision binary64
 (if (<= (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1.0)))) x) -0.5)
   (copysign (- (log (- (hypot 1.0 x) x))) x)
   (copysign (log1p (+ x (+ (hypot 1.0 x) -1.0))) x)))
double code(double x) {
	return copysign(log((fabs(x) + sqrt(((x * x) + 1.0)))), x);
}
double code(double x) {
	double tmp;
	if (copysign(log((fabs(x) + sqrt(((x * x) + 1.0)))), x) <= -0.5) {
		tmp = copysign(-log((hypot(1.0, x) - x)), x);
	} else {
		tmp = copysign(log1p((x + (hypot(1.0, x) + -1.0))), 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 tmp;
	if (Math.copySign(Math.log((Math.abs(x) + Math.sqrt(((x * x) + 1.0)))), x) <= -0.5) {
		tmp = Math.copySign(-Math.log((Math.hypot(1.0, x) - x)), x);
	} else {
		tmp = Math.copySign(Math.log1p((x + (Math.hypot(1.0, x) + -1.0))), x);
	}
	return tmp;
}
def code(x):
	return math.copysign(math.log((math.fabs(x) + math.sqrt(((x * x) + 1.0)))), x)
def code(x):
	tmp = 0
	if math.copysign(math.log((math.fabs(x) + math.sqrt(((x * x) + 1.0)))), x) <= -0.5:
		tmp = math.copysign(-math.log((math.hypot(1.0, x) - x)), x)
	else:
		tmp = math.copysign(math.log1p((x + (math.hypot(1.0, x) + -1.0))), x)
	return tmp
function code(x)
	return copysign(log(Float64(abs(x) + sqrt(Float64(Float64(x * x) + 1.0)))), x)
end
function code(x)
	tmp = 0.0
	if (copysign(log(Float64(abs(x) + sqrt(Float64(Float64(x * x) + 1.0)))), x) <= -0.5)
		tmp = copysign(Float64(-log(Float64(hypot(1.0, x) - x))), x);
	else
		tmp = copysign(log1p(Float64(x + Float64(hypot(1.0, x) + -1.0))), x);
	end
	return 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_] := If[LessEqual[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], -0.5], N[With[{TMP1 = Abs[(-N[Log[N[(N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision] - x), $MachinePrecision]], $MachinePrecision])], TMP2 = Sign[x]}, TMP1 * If[TMP2 == 0, 1, TMP2]], $MachinePrecision], N[With[{TMP1 = Abs[N[Log[1 + N[(x + N[(N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision] + -1.0), $MachinePrecision]), $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}
\mathbf{if}\;\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \leq -0.5:\\
\;\;\;\;\mathsf{copysign}\left(-\log \left(\mathsf{hypot}\left(1, x\right) - x\right), x\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{copysign}\left(\mathsf{log1p}\left(x + \left(\mathsf{hypot}\left(1, x\right) + -1\right)\right), x\right)\\


\end{array}

Error

Target

Original44.8
Target0.0
Herbie0.4
\[\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 2 regimes
  2. if (copysign.f64 (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) 1)))) x) < -0.5

    1. Initial program 32.3

      \[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
    2. Applied egg-rr62.9

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

      \[\leadsto \mathsf{copysign}\left(\log \color{blue}{\left(\frac{1}{\mathsf{hypot}\left(1, x\right) - x}\right)}, x\right) \]
      Proof
      (/.f64 1 (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= metadata-eval (+.f64 1 0)) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 1 (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 x x) (*.f64 x x)))) (-.f64 (hypot.f64 1 x) x)): 24 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1 (*.f64 x x)) (*.f64 x x))) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 31 points decrease in error
      (/.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x x) 1)) (*.f64 x x)) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (-.f64 (Rewrite<= fma-udef_binary64 (fma.f64 x x 1)) (*.f64 x x)) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> sub-neg_binary64 (+.f64 (fma.f64 x x 1) (neg.f64 (*.f64 x x)))) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 (*.f64 x x)) (fma.f64 x x 1))) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (*.f64 x x))) (fma.f64 x x 1)) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (*.f64 x x) (fma.f64 x x 1)))) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1)))) (-.f64 (hypot.f64 1 x) x)): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (Rewrite=> sub-neg_binary64 (+.f64 (hypot.f64 1 x) (neg.f64 x)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 x) (hypot.f64 1 x)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 x)) (hypot.f64 1 x))): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 x (hypot.f64 1 x))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (neg.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 x (hypot.f64 1 x))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 (*.f64 x x) (fma.f64 x x 1)))) (neg.f64 (-.f64 x (hypot.f64 1 x)))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 -1 (-.f64 (*.f64 x x) (fma.f64 x x 1))) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 x (hypot.f64 1 x))))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> times-frac_binary64 (*.f64 (/.f64 -1 -1) (/.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1)) (-.f64 x (hypot.f64 1 x))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1)) (-.f64 x (hypot.f64 1 x)))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> *-lft-identity_binary64 (/.f64 (-.f64 (*.f64 x x) (fma.f64 x x 1)) (-.f64 x (hypot.f64 1 x)))): 0 points increase in error, 0 points decrease in error
      (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 x x) (-.f64 x (hypot.f64 1 x))) (/.f64 (fma.f64 x x 1) (-.f64 x (hypot.f64 1 x))))): 4 points increase in error, 1 points decrease in error
    4. Applied egg-rr0.1

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

      \[\leadsto \mathsf{copysign}\left(\color{blue}{-\log \left(\mathsf{hypot}\left(1, x\right) - x\right)}, x\right) \]
      Proof
      (neg.f64 (log.f64 (-.f64 (hypot.f64 1 x) x))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= +-lft-identity_binary64 (+.f64 0 (neg.f64 (log.f64 (-.f64 (hypot.f64 1 x) x))))): 0 points increase in error, 0 points decrease in error

    if -0.5 < (copysign.f64 (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) 1)))) x)

    1. Initial program 49.1

      \[\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \]
    2. Applied egg-rr39.3

      \[\leadsto \mathsf{copysign}\left(\color{blue}{e^{\log \log \left(x + \mathsf{hypot}\left(1, x\right)\right)}}, x\right) \]
    3. Applied egg-rr38.4

      \[\leadsto \mathsf{copysign}\left(\color{blue}{\mathsf{log1p}\left(\left(x + \mathsf{hypot}\left(1, x\right)\right) - 1\right)}, x\right) \]
    4. Simplified0.4

      \[\leadsto \mathsf{copysign}\left(\color{blue}{\mathsf{log1p}\left(x + \left(\mathsf{hypot}\left(1, x\right) - 1\right)\right)}, x\right) \]
      Proof
      (log1p.f64 (+.f64 x (-.f64 (hypot.f64 1 x) 1))): 0 points increase in error, 0 points decrease in error
      (log1p.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 x (hypot.f64 1 x)) 1))): 183 points increase in error, 1 points decrease in error
  3. Recombined 2 regimes into one program.
  4. Final simplification0.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{copysign}\left(\log \left(\left|x\right| + \sqrt{x \cdot x + 1}\right), x\right) \leq -0.5:\\ \;\;\;\;\mathsf{copysign}\left(-\log \left(\mathsf{hypot}\left(1, x\right) - x\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\mathsf{log1p}\left(x + \left(\mathsf{hypot}\left(1, x\right) + -1\right)\right), x\right)\\ \end{array} \]

Alternatives

Alternative 1
Error28.7
Cost19716
\[\begin{array}{l} \mathbf{if}\;x \leq -0.012:\\ \;\;\;\;\mathsf{copysign}\left(-\log \left(\mathsf{hypot}\left(1, x\right) - x\right), x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{copysign}\left(\log \left(x + \mathsf{hypot}\left(1, x\right)\right), x\right)\\ \end{array} \]
Alternative 2
Error44.6
Cost19520
\[\mathsf{copysign}\left(\log \left(x + \mathsf{hypot}\left(1, x\right)\right), x\right) \]

Error

Reproduce

herbie shell --seed 2022334 
(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))