Rust f32::atanh

Percentage Accurate: 49.1% → 99.5%

Time: 1.8s

Alternatives: 5

Speedup: 3.4×

• Could not converge on a ground truth

  1. x = 7.089199490037004e+21

Specification

Math

\[\tanh^{-1} x \]

FPCore

(FPCore (x)
  :precision binary32
  (atanh x))

C

float code(float x) {
	return atanhf(x);
}

Julia

function code(x)
	return atanh(x)
end

MATLAB

function tmp = code(x)
	tmp = atanh(x);
end

Initial Program: 49.1% accurate, 1.0× speedup

Math

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

FPCore

(FPCore (x)
  :precision binary32
  (* 0.5 (log1p (/ (* 2.0 x) (- 1.0 x)))))

C

float code(float x) {
	return 0.5f * log1pf(((2.0f * x) / (1.0f - x)));
}

Julia

function code(x)
	return Float32(Float32(0.5) * log1p(Float32(Float32(Float32(2.0) * x) / Float32(Float32(1.0) - x))))
end

Alternative 1: 99.5% accurate, 0.6× speedup

Math

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

FPCore

(FPCore (x)
  :precision binary32
  (*
 (copysign 1.0 x)
 (if (<= (fabs x) 1.0)
   (* 0.5 (log1p (/ (+ (fabs x) (fabs x)) (- 1.0 (fabs x)))))
   (* 0.0 (* 2.0 (fabs x))))))

C

float code(float x) {
	float tmp;
	if (fabsf(x) <= 1.0f) {
		tmp = 0.5f * log1pf(((fabsf(x) + fabsf(x)) / (1.0f - fabsf(x))));
	} else {
		tmp = 0.0f * (2.0f * fabsf(x));
	}
	return copysignf(1.0f, x) * tmp;
}

Julia

function code(x)
	tmp = Float32(0.0)
	if (abs(x) <= Float32(1.0))
		tmp = Float32(Float32(0.5) * log1p(Float32(Float32(abs(x) + abs(x)) / Float32(Float32(1.0) - abs(x)))));
	else
		tmp = Float32(Float32(0.0) * Float32(Float32(2.0) * abs(x)));
	end
	return Float32(copysign(Float32(1.0), x) * tmp)
end

Derivation

1. Split input into 2 regimes

2. if x < 1

   1. Initial program 49.1%

      \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
   2. Step-by-step derivation

      1. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

      2. flip-- N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      3. remove-sound-/ N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      4. lower-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      5. metadata-eval N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

      6. lower--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

      7. lower-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

      8. +-commutative N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

      9. add-flip N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

      10. metadata-eval N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

      11. lower--.f32 74.1%

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

   3. Applied rewrites 74.1%

      \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
   4. Step-by-step derivation

      1. lift-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{\color{blue}{2 \cdot x}}{\frac{1 - x \cdot x}{x - -1}}\right) \]

      2. count-2-rev N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{\color{blue}{x + x}}{\frac{1 - x \cdot x}{x - -1}}\right) \]

      3. lower-+.f32 74.1%

         \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{\color{blue}{x + x}}{\frac{1 - x \cdot x}{x - -1}}\right) \]

      4. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

      5. remove-sound-/ N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

      6. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{\color{blue}{1 - x \cdot x}}{x - -1}}\right) \]

      7. metadata-eval N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{\color{blue}{1 \cdot 1} - x \cdot x}{x - -1}}\right) \]

      8. lift-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{1 \cdot 1 - \color{blue}{x \cdot x}}{x - -1}}\right) \]

      9. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{1 \cdot 1 - x \cdot x}{\color{blue}{x - -1}}}\right) \]

      10. sub-flip N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{1 \cdot 1 - x \cdot x}{\color{blue}{x + \left(\mathsf{neg}\left(-1\right)\right)}}}\right) \]

      11. metadata-eval N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{1 \cdot 1 - x \cdot x}{x + \color{blue}{1}}}\right) \]

      12. +-commutative N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\frac{1 \cdot 1 - x \cdot x}{\color{blue}{1 + x}}}\right) \]

      13. flip-- N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{x + x}{\color{blue}{1 - x}}\right) \]

      14. lower--.f32 49.1%

          \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{x + x}{\color{blue}{1 - x}}\right) \]

   5. Applied rewrites 49.1%

      \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\color{blue}{\frac{x + x}{1 - x}}\right) \]

   if 1 < x

   1. Initial program 49.1%

      \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
   2. Step-by-step derivation

      1. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

      2. flip-- N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      3. remove-sound-/ N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      4. lower-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      5. metadata-eval N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

      6. lower--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

      7. lower-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

      8. +-commutative N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

      9. add-flip N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

      10. metadata-eval N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

      11. lower--.f32 74.1%

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

   3. Applied rewrites 74.1%

      \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
   4. Step-by-step derivation

      1. lift-log1p.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      2. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

      3. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      4. log-div N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\left(\log \left(\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|\right) - \log \left(\left|\frac{1 - x \cdot x}{x - -1}\right|\right)\right)} \]

      5. diff-log N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\frac{\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|}{\left|\frac{1 - x \cdot x}{x - -1}\right|}\right)} \]

      6. fabs-div N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      7. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|\color{blue}{1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      8. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      9. lower-log.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      10. lower-fabs.f32 N/A

          \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   5. Applied rewrites 53.2%

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

   6. Taylor expanded in undef-var around zero

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]
   7. Step-by-step derivation

   8. Applied rewrites 56.1%

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]

   9. Taylor expanded in x around 0

      \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
   10. Step-by-step derivation

       1. lower-*.f32 55.7%

          \[\leadsto 0 \cdot \left(2 \cdot \color{blue}{x}\right) \]

   11. Applied rewrites 55.7%

       \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 2: 98.9% accurate, 0.9× speedup

Math

\[\mathsf{copysign}\left(1, x\right) \cdot \begin{array}{l} \mathbf{if}\;\left|x\right| \leq 1:\\ \;\;\;\;\mathsf{fma}\left(\left(\left|x\right| \cdot \left|x\right|\right) \cdot \left|x\right|, 0.3333333333333333, \left|x\right|\right)\\ \mathbf{else}:\\ \;\;\;\;0 \cdot \left(2 \cdot \left|x\right|\right)\\ \end{array} \]

FPCore

(FPCore (x)
  :precision binary32
  (*
 (copysign 1.0 x)
 (if (<= (fabs x) 1.0)
   (fma
    (* (* (fabs x) (fabs x)) (fabs x))
    0.3333333333333333
    (fabs x))
   (* 0.0 (* 2.0 (fabs x))))))

C

float code(float x) {
	float tmp;
	if (fabsf(x) <= 1.0f) {
		tmp = fmaf(((fabsf(x) * fabsf(x)) * fabsf(x)), 0.3333333333333333f, fabsf(x));
	} else {
		tmp = 0.0f * (2.0f * fabsf(x));
	}
	return copysignf(1.0f, x) * tmp;
}

Julia

function code(x)
	tmp = Float32(0.0)
	if (abs(x) <= Float32(1.0))
		tmp = fma(Float32(Float32(abs(x) * abs(x)) * abs(x)), Float32(0.3333333333333333), abs(x));
	else
		tmp = Float32(Float32(0.0) * Float32(Float32(2.0) * abs(x)));
	end
	return Float32(copysign(Float32(1.0), x) * tmp)
end

Derivation

1. Split input into 2 regimes

2. if x < 1

   1. Initial program 49.1%

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

   2. Taylor expanded in x around 0

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

      1. lower-*.f32 N/A

         \[\leadsto x \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {x}^{2}\right)} \]

      2. lower-+.f32 N/A

         \[\leadsto x \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {x}^{2}}\right) \]

      3. lower-*.f32 N/A

         \[\leadsto x \cdot \left(1 + \frac{1}{3} \cdot \color{blue}{{x}^{2}}\right) \]

      4. lower-pow.f32 50.3%

         \[\leadsto x \cdot \left(1 + 0.3333333333333333 \cdot {x}^{\color{blue}{2}}\right) \]

   4. Applied rewrites 50.3%

      \[\leadsto \color{blue}{x \cdot \left(1 + 0.3333333333333333 \cdot {x}^{2}\right)} \]
   5. Step-by-step derivation

      1. lift-*.f32 N/A

         \[\leadsto x \cdot \color{blue}{\left(1 + \frac{1}{3} \cdot {x}^{2}\right)} \]

      2. lift-+.f32 N/A

         \[\leadsto x \cdot \left(1 + \color{blue}{\frac{1}{3} \cdot {x}^{2}}\right) \]

      3. +-commutative N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot {x}^{2} + \color{blue}{1}\right) \]

      4. distribute-lft-in N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot {x}^{2}\right) + \color{blue}{x \cdot 1} \]

      5. lift-*.f32 N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot {x}^{2}\right) + x \cdot 1 \]

      6. lift-pow.f32 N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot {x}^{2}\right) + x \cdot 1 \]

      7. pow2 N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot \left(x \cdot x\right)\right) + x \cdot 1 \]

      8. lift-*.f32 N/A

         \[\leadsto x \cdot \left(\frac{1}{3} \cdot \left(x \cdot x\right)\right) + x \cdot 1 \]

      9. *-commutative N/A

         \[\leadsto x \cdot \left(\left(x \cdot x\right) \cdot \frac{1}{3}\right) + x \cdot 1 \]

      10. associate-*r* N/A

          \[\leadsto \left(x \cdot \left(x \cdot x\right)\right) \cdot \frac{1}{3} + \color{blue}{x} \cdot 1 \]

      11. lift-*.f32 N/A

          \[\leadsto \left(x \cdot \left(x \cdot x\right)\right) \cdot \frac{1}{3} + x \cdot 1 \]

      12. cube-mult N/A

          \[\leadsto {x}^{3} \cdot \frac{1}{3} + x \cdot 1 \]

      13. *-rgt-identity N/A

          \[\leadsto {x}^{3} \cdot \frac{1}{3} + x \]

      14. lower-fma.f32 N/A

          \[\leadsto \mathsf{fma}\left({x}^{3}, \color{blue}{\frac{1}{3}}, x\right) \]

      15. unpow3 N/A

          \[\leadsto \mathsf{fma}\left(\left(x \cdot x\right) \cdot x, \frac{1}{3}, x\right) \]

      16. lift-*.f32 N/A

          \[\leadsto \mathsf{fma}\left(\left(x \cdot x\right) \cdot x, \frac{1}{3}, x\right) \]

      17. lower-*.f32 50.4%

          \[\leadsto \mathsf{fma}\left(\left(x \cdot x\right) \cdot x, 0.3333333333333333, x\right) \]

   6. Applied rewrites 50.4%

      \[\leadsto \mathsf{fma}\left(\left(x \cdot x\right) \cdot x, \color{blue}{0.3333333333333333}, x\right) \]

   if 1 < x

   1. Initial program 49.1%

      \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
   2. Step-by-step derivation

      1. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

      2. flip-- N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      3. remove-sound-/ N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      4. lower-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      5. metadata-eval N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

      6. lower--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

      7. lower-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

      8. +-commutative N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

      9. add-flip N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

      10. metadata-eval N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

      11. lower--.f32 74.1%

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

   3. Applied rewrites 74.1%

      \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
   4. Step-by-step derivation

      1. lift-log1p.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      2. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

      3. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      4. log-div N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\left(\log \left(\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|\right) - \log \left(\left|\frac{1 - x \cdot x}{x - -1}\right|\right)\right)} \]

      5. diff-log N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\frac{\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|}{\left|\frac{1 - x \cdot x}{x - -1}\right|}\right)} \]

      6. fabs-div N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      7. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|\color{blue}{1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      8. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      9. lower-log.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      10. lower-fabs.f32 N/A

          \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   5. Applied rewrites 53.2%

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

   6. Taylor expanded in undef-var around zero

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]
   7. Step-by-step derivation

   8. Applied rewrites 56.1%

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]

   9. Taylor expanded in x around 0

      \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
   10. Step-by-step derivation

       1. lower-*.f32 55.7%

          \[\leadsto 0 \cdot \left(2 \cdot \color{blue}{x}\right) \]

   11. Applied rewrites 55.7%

       \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 3: 59.4% accurate, 1.1× speedup

Math

\[\mathsf{copysign}\left(1, x\right) \cdot \begin{array}{l} \mathbf{if}\;\left|x\right| \leq 1:\\ \;\;\;\;\log \left(1 + \left|x\right|\right)\\ \mathbf{else}:\\ \;\;\;\;0 \cdot \left(2 \cdot \left|x\right|\right)\\ \end{array} \]

FPCore

(FPCore (x)
  :precision binary32
  (*
 (copysign 1.0 x)
 (if (<= (fabs x) 1.0)
   (log (+ 1.0 (fabs x)))
   (* 0.0 (* 2.0 (fabs x))))))

C

float code(float x) {
	float tmp;
	if (fabsf(x) <= 1.0f) {
		tmp = logf((1.0f + fabsf(x)));
	} else {
		tmp = 0.0f * (2.0f * fabsf(x));
	}
	return copysignf(1.0f, x) * tmp;
}

Julia

function code(x)
	tmp = Float32(0.0)
	if (abs(x) <= Float32(1.0))
		tmp = log(Float32(Float32(1.0) + abs(x)));
	else
		tmp = Float32(Float32(0.0) * Float32(Float32(2.0) * abs(x)));
	end
	return Float32(copysign(Float32(1.0), x) * tmp)
end

MATLAB

function tmp_2 = code(x)
	tmp = single(0.0);
	if (abs(x) <= single(1.0))
		tmp = log((single(1.0) + abs(x)));
	else
		tmp = single(0.0) * (single(2.0) * abs(x));
	end
	tmp_2 = (sign(x) * abs(single(1.0))) * tmp;
end

Derivation

1. Split input into 2 regimes

2. if x < 1

   1. Initial program 49.1%

      \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
   2. Step-by-step derivation

      1. lift-*.f32 N/A

         \[\leadsto \color{blue}{\frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right)} \]

      2. lift-log1p.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{1 - x}\right)} \]

      3. log-pow-rev N/A

         \[\leadsto \color{blue}{\log \left({\left(1 + \frac{2 \cdot x}{1 - x}\right)}^{\frac{1}{2}}\right)} \]

      4. lower-log.f32 N/A

         \[\leadsto \color{blue}{\log \left({\left(1 + \frac{2 \cdot x}{1 - x}\right)}^{\frac{1}{2}}\right)} \]

      5. unpow1/2 N/A

         \[\leadsto \log \color{blue}{\left(\sqrt{1 + \frac{2 \cdot x}{1 - x}}\right)} \]

      6. lower-sqrt.f32 N/A

         \[\leadsto \log \color{blue}{\left(\sqrt{1 + \frac{2 \cdot x}{1 - x}}\right)} \]

      7. +-commutative N/A

         \[\leadsto \log \left(\sqrt{\color{blue}{\frac{2 \cdot x}{1 - x} + 1}}\right) \]

      8. lift-/.f32 N/A

         \[\leadsto \log \left(\sqrt{\color{blue}{\frac{2 \cdot x}{1 - x}} + 1}\right) \]

      9. lift-*.f32 N/A

         \[\leadsto \log \left(\sqrt{\frac{\color{blue}{2 \cdot x}}{1 - x} + 1}\right) \]

      10. associate-/l* N/A

          \[\leadsto \log \left(\sqrt{\color{blue}{2 \cdot \frac{x}{1 - x}} + 1}\right) \]

      11. *-commutative N/A

          \[\leadsto \log \left(\sqrt{\color{blue}{\frac{x}{1 - x} \cdot 2} + 1}\right) \]

      12. lower-fma.f32 N/A

          \[\leadsto \log \left(\sqrt{\color{blue}{\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)}}\right) \]

      13. lower-/.f32 10.9%

          \[\leadsto \log \left(\sqrt{\mathsf{fma}\left(\color{blue}{\frac{x}{1 - x}}, 2, 1\right)}\right) \]

   3. Applied rewrites 10.9%

      \[\leadsto \color{blue}{\log \left(\sqrt{\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)}\right)} \]

   4. Taylor expanded in x around 0

      \[\leadsto \log \color{blue}{\left(1 + x\right)} \]
   5. Step-by-step derivation

      1. lower-+.f32 10.7%

         \[\leadsto \log \left(1 + \color{blue}{x}\right) \]

   6. Applied rewrites 10.7%

      \[\leadsto \log \color{blue}{\left(1 + x\right)} \]

   if 1 < x

   1. Initial program 49.1%

      \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
   2. Step-by-step derivation

      1. lift--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

      2. flip-- N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      3. remove-sound-/ N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      4. lower-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

      5. metadata-eval N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

      6. lower--.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

      7. lower-*.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

      8. +-commutative N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

      9. add-flip N/A

         \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

      10. metadata-eval N/A

          \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

      11. lower--.f32 74.1%

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

   3. Applied rewrites 74.1%

      \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
   4. Step-by-step derivation

      1. lift-log1p.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      2. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

      3. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

      4. log-div N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\left(\log \left(\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|\right) - \log \left(\left|\frac{1 - x \cdot x}{x - -1}\right|\right)\right)} \]

      5. diff-log N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\frac{\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|}{\left|\frac{1 - x \cdot x}{x - -1}\right|}\right)} \]

      6. fabs-div N/A

         \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      7. add-to-fraction N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|\color{blue}{1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      8. lift-/.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \log \left(\left|1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

      9. lower-log.f32 N/A

         \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

      10. lower-fabs.f32 N/A

          \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   5. Applied rewrites 53.2%

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

   6. Taylor expanded in undef-var around zero

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]
   7. Step-by-step derivation

   8. Applied rewrites 56.1%

      \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]

   9. Taylor expanded in x around 0

      \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
   10. Step-by-step derivation

       1. lower-*.f32 55.7%

          \[\leadsto 0 \cdot \left(2 \cdot \color{blue}{x}\right) \]

   11. Applied rewrites 55.7%

       \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
3. Recombined 2 regimes into one program.
4. Add Preprocessing

Alternative 4: 55.7% accurate, 3.4× speedup

Math

\[0 \cdot \left(2 \cdot x\right) \]

FPCore

(FPCore (x)
  :precision binary32
  (* 0.0 (* 2.0 x)))

C

float code(float x) {
	return 0.0f * (2.0f * x);
}

Fortran

real(4) function code(x)
use fmin_fmax_functions
    real(4), intent (in) :: x
    code = 0.0e0 * (2.0e0 * x)
end function

Julia

function code(x)
	return Float32(Float32(0.0) * Float32(Float32(2.0) * x))
end

MATLAB

function tmp = code(x)
	tmp = single(0.0) * (single(2.0) * x);
end

Derivation

1. Initial program 49.1%

   \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
2. Step-by-step derivation

   1. lift--.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

   2. flip-- N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   3. remove-sound-/ N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   4. lower-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   5. metadata-eval N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

   6. lower--.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

   7. lower-*.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

   8. +-commutative N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

   9. add-flip N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

   10. metadata-eval N/A

       \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

   11. lower--.f32 74.1%

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

3. Applied rewrites 74.1%

   \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
4. Step-by-step derivation

   1. lift-log1p.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

   2. lift-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

   3. add-to-fraction N/A

      \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

   4. log-div N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\left(\log \left(\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|\right) - \log \left(\left|\frac{1 - x \cdot x}{x - -1}\right|\right)\right)} \]

   5. diff-log N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\frac{\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|}{\left|\frac{1 - x \cdot x}{x - -1}\right|}\right)} \]

   6. fabs-div N/A

      \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   7. add-to-fraction N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(\left|\color{blue}{1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

   8. lift-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(\left|1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

   9. lower-log.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   10. lower-fabs.f32 N/A

       \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

5. Applied rewrites 53.2%

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

6. Taylor expanded in undef-var around zero

   \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]
7. Step-by-step derivation

8. Applied rewrites 56.1%

   \[\leadsto \color{blue}{0} \cdot \log \left(\left|\mathsf{fma}\left(\frac{x}{1 - x}, 2, 1\right)\right|\right) \]

9. Taylor expanded in x around 0

   \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
10. Step-by-step derivation

    1. lower-*.f32 55.7%

       \[\leadsto 0 \cdot \left(2 \cdot \color{blue}{x}\right) \]

11. Applied rewrites 55.7%

    \[\leadsto 0 \cdot \color{blue}{\left(2 \cdot x\right)} \]
12. Add Preprocessing

Alternative 5: 9.3% accurate, 5.0× speedup

Math

\[\frac{1}{x} \]

FPCore

(FPCore (x)
  :precision binary32
  (/ 1.0 x))

C

float code(float x) {
	return 1.0f / x;
}

Fortran

real(4) function code(x)
use fmin_fmax_functions
    real(4), intent (in) :: x
    code = 1.0e0 / x
end function

Julia

function code(x)
	return Float32(Float32(1.0) / x)
end

MATLAB

function tmp = code(x)
	tmp = single(1.0) / x;
end

Derivation

1. Initial program 49.1%

   \[0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{1 - x}\right) \]
2. Step-by-step derivation

   1. lift--.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{1 - x}}\right) \]

   2. flip-- N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   3. remove-sound-/ N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   4. lower-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 \cdot 1 - x \cdot x}{1 + x}}}\right) \]

   5. metadata-eval N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1} - x \cdot x}{1 + x}}\right) \]

   6. lower--.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{\color{blue}{1 - x \cdot x}}{1 + x}}\right) \]

   7. lower-*.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - \color{blue}{x \cdot x}}{1 + x}}\right) \]

   8. +-commutative N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x + 1}}}\right) \]

   9. add-flip N/A

      \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{\color{blue}{x - \left(\mathsf{neg}\left(1\right)\right)}}}\right) \]

   10. metadata-eval N/A

       \[\leadsto \frac{1}{2} \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - \color{blue}{-1}}}\right) \]

   11. lower--.f32 74.1%

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

3. Applied rewrites 74.1%

   \[\leadsto 0.5 \cdot \mathsf{log1p}\left(\frac{2 \cdot x}{\color{blue}{\frac{1 - x \cdot x}{x - -1}}}\right) \]
4. Step-by-step derivation

   1. lift-log1p.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

   2. lift-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right) \]

   3. add-to-fraction N/A

      \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right)} \]

   4. log-div N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\left(\log \left(\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|\right) - \log \left(\left|\frac{1 - x \cdot x}{x - -1}\right|\right)\right)} \]

   5. diff-log N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\frac{\left|1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x\right|}{\left|\frac{1 - x \cdot x}{x - -1}\right|}\right)} \]

   6. fabs-div N/A

      \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|\frac{1 \cdot \frac{1 - x \cdot x}{x - -1} + 2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   7. add-to-fraction N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(\left|\color{blue}{1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

   8. lift-/.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \log \left(\left|1 + \color{blue}{\frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}}\right|\right) \]

   9. lower-log.f32 N/A

      \[\leadsto \frac{1}{2} \cdot \color{blue}{\log \left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

   10. lower-fabs.f32 N/A

       \[\leadsto \frac{1}{2} \cdot \log \color{blue}{\left(\left|1 + \frac{2 \cdot x}{\frac{1 - x \cdot x}{x - -1}}\right|\right)} \]

5. Applied rewrites 53.2%

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

6. Taylor expanded in x around inf

   \[\leadsto \color{blue}{\frac{1}{x}} \]
7. Step-by-step derivation

   1. lower-/.f32 9.3%

      \[\leadsto \frac{1}{\color{blue}{x}} \]

8. Applied rewrites 9.3%

   \[\leadsto \color{blue}{\frac{1}{x}} \]
9. Add Preprocessing

Reproduce

herbie shell --seed 2025313 -o setup:search
(FPCore (x)
  :name "Rust f32::atanh"
  :precision binary32
  (* 0.5 (log1p (/ (* 2.0 x) (- 1.0 x)))))