bug323 (missed optimization)

Average Accuracy: 6.6% → 10.2%

Time: 10.9s

Precision: binary64

Cost: 45760

\[0 \leq x \land x \leq 0.5\]

Math

\[\cos^{-1} \left(1 - x\right) \]

↓

\[\begin{array}{l} t_0 := \sin^{-1} \left(1 - x\right)\\ \frac{\mathsf{fma}\left(-t_0, t_0, 0.25 \cdot {\pi}^{2}\right)}{\pi - \cos^{-1} \left(1 - x\right)} \end{array} \]

FPCore

(FPCore (x) :precision binary64 (acos (- 1.0 x)))

↓

(FPCore (x)
 :precision binary64
 (let* ((t_0 (asin (- 1.0 x))))
   (/ (fma (- t_0) t_0 (* 0.25 (pow PI 2.0))) (- PI (acos (- 1.0 x))))))

C

double code(double x) {
	return acos((1.0 - x));
}

↓

double code(double x) {
	double t_0 = asin((1.0 - x));
	return fma(-t_0, t_0, (0.25 * pow(((double) M_PI), 2.0))) / (((double) M_PI) - acos((1.0 - x)));
}

Julia

function code(x)
	return acos(Float64(1.0 - x))
end

↓

function code(x)
	t_0 = asin(Float64(1.0 - x))
	return Float64(fma(Float64(-t_0), t_0, Float64(0.25 * (pi ^ 2.0))) / Float64(pi - acos(Float64(1.0 - x))))
end

Wolfram

code[x_] := N[ArcCos[N[(1.0 - x), $MachinePrecision]], $MachinePrecision]

↓

code[x_] := Block[{t$95$0 = N[ArcSin[N[(1.0 - x), $MachinePrecision]], $MachinePrecision]}, N[(N[((-t$95$0) * t$95$0 + N[(0.25 * N[Power[Pi, 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(Pi - N[ArcCos[N[(1.0 - x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Target

Original	6.6%
Target	100.0%
Herbie	10.2%

\[2 \cdot \sin^{-1} \left(\sqrt{\frac{x}{2}}\right) \]

Derivation

1. Initial program 6.6%

   \[\cos^{-1} \left(1 - x\right) \]

2. Applied egg-rr 6.6%

   \[\leadsto \color{blue}{\frac{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)}} \]
   Proof

   [Start] 6.6	\[ \cos^{-1} \left(1 - x\right) \]
   acos-asin [=>] 6.6	\[ \color{blue}{\frac{\pi}{2} - \sin^{-1} \left(1 - x\right)} \]
   flip-- [=>] 6.6	\[ \color{blue}{\frac{\frac{\pi}{2} \cdot \frac{\pi}{2} - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\frac{\pi}{2} + \sin^{-1} \left(1 - x\right)}} \]
   div-inv [=>] 6.6	\[ \frac{\color{blue}{\left(\pi \cdot \frac{1}{2}\right)} \cdot \frac{\pi}{2} - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\frac{\pi}{2} + \sin^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 6.6	\[ \frac{\left(\pi \cdot \color{blue}{0.5}\right) \cdot \frac{\pi}{2} - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\frac{\pi}{2} + \sin^{-1} \left(1 - x\right)} \]
   div-inv [=>] 6.6	\[ \frac{\left(\pi \cdot 0.5\right) \cdot \color{blue}{\left(\pi \cdot \frac{1}{2}\right)} - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\frac{\pi}{2} + \sin^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 6.6	\[ \frac{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot \color{blue}{0.5}\right) - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\frac{\pi}{2} + \sin^{-1} \left(1 - x\right)} \]
   div-inv [=>] 6.6	\[ \frac{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\color{blue}{\pi \cdot \frac{1}{2}} + \sin^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 6.6	\[ \frac{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\pi \cdot \color{blue}{0.5} + \sin^{-1} \left(1 - x\right)} \]

3. Applied egg-rr 10.2%

   \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   Proof

   [Start] 6.6	\[ \frac{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) - \sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   sub-neg [=>] 6.6	\[ \frac{\color{blue}{\left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right) + \left(-\sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)\right)}}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   +-commutative [=>] 6.6	\[ \frac{\color{blue}{\left(-\sin^{-1} \left(1 - x\right) \cdot \sin^{-1} \left(1 - x\right)\right) + \left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right)}}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   distribute-lft-neg-in [=>] 6.6	\[ \frac{\color{blue}{\left(-\sin^{-1} \left(1 - x\right)\right) \cdot \sin^{-1} \left(1 - x\right)} + \left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   fma-def [=>] 10.2	\[ \frac{\color{blue}{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), \left(\pi \cdot 0.5\right) \cdot \left(\pi \cdot 0.5\right)\right)}}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   pow2 [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), \color{blue}{{\left(\pi \cdot 0.5\right)}^{2}}\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   *-commutative [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), {\color{blue}{\left(0.5 \cdot \pi\right)}}^{2}\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   unpow-prod-down [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), \color{blue}{{0.5}^{2} \cdot {\pi}^{2}}\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), \color{blue}{0.25} \cdot {\pi}^{2}\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]

4. Applied egg-rr 10.2%

   \[\leadsto \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\sqrt[3]{{\left(\mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)\right)}^{3}}}} \]
   Proof

   [Start] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)} \]
   add-cbrt-cube [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\sqrt[3]{\left(\left(\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)\right) \cdot \left(\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)\right)\right) \cdot \left(\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)\right)}}} \]
   pow3 [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\sqrt[3]{\color{blue}{{\left(\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)\right)}^{3}}}} \]
   fma-def [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\sqrt[3]{{\color{blue}{\left(\mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)\right)}}^{3}}} \]

5. Applied egg-rr 10.2%

   \[\leadsto \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\mathsf{fma}\left(\pi, 0.5, \pi \cdot 0.5\right) - \cos^{-1} \left(1 - x\right)}} \]
   Proof

   [Start] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\sqrt[3]{{\left(\mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)\right)}^{3}}} \]
   rem-cbrt-cube [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\mathsf{fma}\left(\pi, 0.5, \sin^{-1} \left(1 - x\right)\right)}} \]
   fma-udef [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\pi \cdot 0.5 + \sin^{-1} \left(1 - x\right)}} \]
   metadata-eval [<=] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\pi \cdot \color{blue}{\frac{1}{2}} + \sin^{-1} \left(1 - x\right)} \]
   div-inv [<=] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\frac{\pi}{2}} + \sin^{-1} \left(1 - x\right)} \]
   asin-acos [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\frac{\pi}{2} + \color{blue}{\left(\frac{\pi}{2} - \cos^{-1} \left(1 - x\right)\right)}} \]
   associate-+r- [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\left(\frac{\pi}{2} + \frac{\pi}{2}\right) - \cos^{-1} \left(1 - x\right)}} \]
   div-inv [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\left(\color{blue}{\pi \cdot \frac{1}{2}} + \frac{\pi}{2}\right) - \cos^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\left(\pi \cdot \color{blue}{0.5} + \frac{\pi}{2}\right) - \cos^{-1} \left(1 - x\right)} \]
   fma-def [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\mathsf{fma}\left(\pi, 0.5, \frac{\pi}{2}\right)} - \cos^{-1} \left(1 - x\right)} \]
   div-inv [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\mathsf{fma}\left(\pi, 0.5, \color{blue}{\pi \cdot \frac{1}{2}}\right) - \cos^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\mathsf{fma}\left(\pi, 0.5, \pi \cdot \color{blue}{0.5}\right) - \cos^{-1} \left(1 - x\right)} \]

6. Simplified 10.2%

   \[\leadsto \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\pi - \cos^{-1} \left(1 - x\right)}} \]
   Proof

   [Start] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\mathsf{fma}\left(\pi, 0.5, \pi \cdot 0.5\right) - \cos^{-1} \left(1 - x\right)} \]
   fma-udef [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\left(\pi \cdot 0.5 + \pi \cdot 0.5\right)} - \cos^{-1} \left(1 - x\right)} \]
   distribute-lft-out [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\pi \cdot \left(0.5 + 0.5\right)} - \cos^{-1} \left(1 - x\right)} \]
   metadata-eval [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\pi \cdot \color{blue}{1} - \cos^{-1} \left(1 - x\right)} \]
   *-rgt-identity [=>] 10.2	\[ \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\color{blue}{\pi} - \cos^{-1} \left(1 - x\right)} \]

7. Final simplification 10.2%

   \[\leadsto \frac{\mathsf{fma}\left(-\sin^{-1} \left(1 - x\right), \sin^{-1} \left(1 - x\right), 0.25 \cdot {\pi}^{2}\right)}{\pi - \cos^{-1} \left(1 - x\right)} \]

Alternatives

Alternative 1
Accuracy	10.1%
Cost	45696

\[\begin{array}{l} t_0 := \sin^{-1} \left(1 - x\right)\\ t_1 := \sqrt{t_0}\\ \cos^{-1} \left(1 - x\right) + \mathsf{fma}\left(-t_1, t_1, t_0\right) \end{array} \]

Alternative 2
Accuracy	10.1%
Cost	38976

\[\begin{array}{l} t_0 := \sqrt{\sin^{-1} \left(1 - x\right)}\\ \mathsf{fma}\left(t_0, -t_0, \pi \cdot 0.5\right) \end{array} \]

Alternative 3
Accuracy	10.1%
Cost	38912

\[\mathsf{fma}\left(\sqrt{{\pi}^{2} \cdot 0.5}, \sqrt{0.5}, -\sin^{-1} \left(1 - x\right)\right) \]

Alternative 4
Accuracy	10.1%
Cost	32576

\[\sqrt{{\pi}^{2} \cdot 0.5} \cdot \sqrt{0.5} - \sin^{-1} \left(1 - x\right) \]

Alternative 5
Accuracy	10.1%
Cost	26176

\[-1 + 3 \cdot \log \left(\sqrt[3]{e^{1 + \cos^{-1} \left(1 - x\right)}}\right) \]

Alternative 6
Accuracy	9.2%
Cost	19844

\[\begin{array}{l} \mathbf{if}\;x \leq 5.6 \cdot 10^{-17}:\\ \;\;\;\;\mathsf{hypot}\left(\pi \cdot 0.5, \sin^{-1} \left(1 - x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;-1 + \sqrt[3]{{\left(1 + \cos^{-1} \left(1 - x\right)\right)}^{3}}\\ \end{array} \]

Alternative 7
Accuracy	9.2%
Cost	19780

\[\begin{array}{l} \mathbf{if}\;x \leq 5.6 \cdot 10^{-17}:\\ \;\;\;\;\mathsf{hypot}\left(\pi \cdot 0.5, \sin^{-1} \left(1 - x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;e^{\log \left(-1 + \left(1 + \cos^{-1} \left(1 - x\right)\right)\right)}\\ \end{array} \]

Alternative 8
Accuracy	6.6%
Cost	19652

\[\begin{array}{l} t_0 := \cos^{-1} \left(1 - x\right)\\ \mathbf{if}\;1 - x \leq 1:\\ \;\;\;\;e^{\log t_0}\\ \mathbf{else}:\\ \;\;\;\;\pi - t_0\\ \end{array} \]

Alternative 9
Accuracy	9.2%
Cost	19652

\[\begin{array}{l} \mathbf{if}\;x \leq 5.6 \cdot 10^{-17}:\\ \;\;\;\;\mathsf{hypot}\left(\pi \cdot 0.5, \sin^{-1} \left(1 - x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;e^{\log \cos^{-1} \left(1 - x\right)}\\ \end{array} \]

Alternative 10
Accuracy	6.6%
Cost	13316

\[\begin{array}{l} t_0 := \cos^{-1} \left(1 - x\right)\\ \mathbf{if}\;1 - x \leq 1:\\ \;\;\;\;-1 + \left(1 + t_0\right)\\ \mathbf{else}:\\ \;\;\;\;\pi - t_0\\ \end{array} \]

Alternative 11
Accuracy	6.6%
Cost	6848

\[-1 + \left(1 + \cos^{-1} \left(1 - x\right)\right) \]

Alternative 12
Accuracy	6.6%
Cost	6592

\[\cos^{-1} \left(1 - x\right) \]

Reproduce

herbie shell --seed 2023151 
(FPCore (x)
  :name "bug323 (missed optimization)"
  :precision binary64
  :pre (and (<= 0.0 x) (<= x 0.5))

  :herbie-target
  (* 2.0 (asin (sqrt (/ x 2.0))))

  (acos (- 1.0 x)))