VandenBroeck and Keller, Equation (24)

Average Accuracy: 99.7% → 99.8%

Time: 13.0s

Precision: binary64

Cost: 13248

Math

\[\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(1, \mathsf{tan.f64}\left(B\right)\right)\right)\right), \mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\right) \]

↓

\[\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{/.f64}\left(x, \mathsf{tan.f64}\left(B\right)\right)\right) \]

FPCore

(FPCore (B x)
 :precision binary64
 (+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B))))

↓

(FPCore (B x)
 :precision binary64
 (-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B))))

Derivation

1. Initial program 99.7%

   \[\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(1, \mathsf{tan.f64}\left(B\right)\right)\right)\right), \mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\right) \]

2. Simplified 99.8%

   \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{/.f64}\left(x, \mathsf{tan.f64}\left(B\right)\right)\right)} \]
   Proof

   [Start] 99.7	\[ \mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(1, \mathsf{tan.f64}\left(B\right)\right)\right)\right), \mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\right) \]
   +-commutative [=>] 99.7	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(1, \mathsf{tan.f64}\left(B\right)\right)\right)\right)\right)} \]
   unsub-neg [=>] 99.7	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{*.f64}\left(x, \mathsf{/.f64}\left(1, \mathsf{tan.f64}\left(B\right)\right)\right)\right)} \]
   associate-*r/ [=>] 99.8	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(x, 1\right), \mathsf{tan.f64}\left(B\right)\right)}\right) \]
   *-rgt-identity [=>] 99.8	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{/.f64}\left(\color{blue}{x}, \mathsf{tan.f64}\left(B\right)\right)\right) \]

3. Final simplification 99.8%

   \[\leadsto \mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{/.f64}\left(x, \mathsf{tan.f64}\left(B\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	98.1%
Cost	7113

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-8264141345021879}{1180591620717411303424}\right) \lor \neg \mathsf{<=.f64}\left(x, \frac{6422418416702717}{18889465931478580854784}\right):\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, B\right), \mathsf{/.f64}\left(x, \mathsf{tan.f64}\left(B\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	98.5%
Cost	7113

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-2476979795053773}{1125899906842624}\right) \lor \neg \mathsf{<=.f64}\left(x, \frac{1080863910568919}{72057594037927936}\right):\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, B\right), \mathsf{/.f64}\left(x, \mathsf{tan.f64}\left(B\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right), \mathsf{/.f64}\left(x, B\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	97.4%
Cost	6921

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-4728779608739021}{4503599627370496}\right) \lor \neg \mathsf{<=.f64}\left(x, 1\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(x\right), \mathsf{tan.f64}\left(B\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	71.3%
Cost	6857

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-2184094498327211}{590295810358705651712}\right) \lor \neg \mathsf{<=.f64}\left(x, \frac{944473296573929}{590295810358705651712}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(B, \frac{1}{6}\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), B\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sin.f64}\left(B\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	44.7%
Cost	576

\[\mathsf{+.f64}\left(\mathsf{*.f64}\left(B, \frac{1}{6}\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), B\right)\right) \]

Alternative 6
Accuracy	43.3%
Cost	521

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-3022314549036573}{75557863725914323419136}\right) \lor \neg \mathsf{<=.f64}\left(x, 1\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(x\right), B\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, B\right)\\ \end{array} \]

Alternative 7
Accuracy	44.6%
Cost	320

\[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(1, x\right), B\right) \]

Alternative 8
Accuracy	3.3%
Cost	192

\[\mathsf{*.f64}\left(B, \frac{1}{6}\right) \]

Alternative 9
Accuracy	29.8%
Cost	192

\[\mathsf{/.f64}\left(1, B\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (B x)
  :name "VandenBroeck and Keller, Equation (24)"
  :precision binary64
  (+ (- (* x (/ 1.0 (tan B)))) (/ 1.0 (sin B))))