Average Error: 13.4 → 0.6
Time: 23.9s
Precision: binary32
\[2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1 \land 2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1 \land 0 \leq maxCos \land maxCos \leq 1\]
\[\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)}\]
↓
\[\sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \frac{\sqrt{\left(\left(2 + ux \cdot maxCos\right) - ux\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{ux \cdot ux + ux \cdot \left(maxCos \cdot \left(ux + ux \cdot maxCos\right)\right)}}\]
\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)}
↓
\sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \frac{\sqrt{\left(\left(2 + ux \cdot maxCos\right) - ux\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{ux \cdot ux + ux \cdot \left(maxCos \cdot \left(ux + ux \cdot maxCos\right)\right)}}
(FPCore (ux uy maxCos)
 :precision binary32
 (*
  (sin (* (* uy 2.0) PI))
  (sqrt
   (- 1.0 (* (+ (- 1.0 ux) (* ux maxCos)) (+ (- 1.0 ux) (* ux maxCos)))))))
↓
(FPCore (ux uy maxCos)
 :precision binary32
 (*
  (sin (* (* uy PI) 2.0))
  (/
   (sqrt
    (* (- (+ 2.0 (* ux maxCos)) ux) (- (pow ux 3.0) (pow (* ux maxCos) 3.0))))
   (sqrt (+ (* ux ux) (* ux (* maxCos (+ ux (* ux maxCos)))))))))
float code(float ux, float uy, float maxCos) {
	return sinf((uy * 2.0f) * ((float) M_PI)) * sqrtf(1.0f - (((1.0f - ux) + (ux * maxCos)) * ((1.0f - ux) + (ux * maxCos))));
}
↓
float code(float ux, float uy, float maxCos) {
	return sinf((uy * ((float) M_PI)) * 2.0f) * (sqrtf(((2.0f + (ux * maxCos)) - ux) * (powf(ux, 3.0f) - powf((ux * maxCos), 3.0f))) / sqrtf((ux * ux) + (ux * (maxCos * (ux + (ux * maxCos))))));
}

Error

Bits error versus ux

Bits error versus uy

Bits error versus maxCos

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 13.4

    \[\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{1 - \left(\left(1 - ux\right) + ux \cdot maxCos\right) \cdot \left(\left(1 - ux\right) + ux \cdot maxCos\right)}\]

  2. Simplified0.6

    \[\leadsto \color{blue}{\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left(ux - ux \cdot maxCos\right) \cdot \left(\left(\left(1 - ux\right) + ux \cdot maxCos\right) + 1\right)}}\]
  3. Using strategy rm

  4. Applied flip3--_binary320.6

    \[\leadsto \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\color{blue}{\frac{{ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}}{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}} \cdot \left(\left(\left(1 - ux\right) + ux \cdot maxCos\right) + 1\right)}\]

  5. Applied associate-*l/_binary320.6

    \[\leadsto \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\color{blue}{\frac{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(\left(1 - ux\right) + ux \cdot maxCos\right) + 1\right)}{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  6. Applied sqrt-div_binary320.6

    \[\leadsto \sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \color{blue}{\frac{\sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(\left(1 - ux\right) + ux \cdot maxCos\right) + 1\right)}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  7. Applied associate-*r/_binary320.6

    \[\leadsto \color{blue}{\frac{\sin \left(\left(uy \cdot 2\right) \cdot \pi\right) \cdot \sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(\left(1 - ux\right) + ux \cdot maxCos\right) + 1\right)}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  8. Simplified0.6

    \[\leadsto \frac{\color{blue}{\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{\left(2 - \left(ux - ux \cdot maxCos\right)\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}\]
  9. Using strategy rm

  10. Applied *-un-lft-identity_binary320.6

    \[\leadsto \frac{\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{\left(2 - \left(ux - ux \cdot maxCos\right)\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{\color{blue}{1 \cdot \left(ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)\right)}}}\]

  11. Applied sqrt-prod_binary320.6

    \[\leadsto \frac{\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{\left(2 - \left(ux - ux \cdot maxCos\right)\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\color{blue}{\sqrt{1} \cdot \sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  12. Applied associate-/r*_binary320.6

    \[\leadsto \color{blue}{\frac{\frac{\sin \left(2 \cdot \left(uy \cdot \pi\right)\right) \cdot \sqrt{\left(2 - \left(ux - ux \cdot maxCos\right)\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{1}}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  13. Simplified0.6

    \[\leadsto \frac{\color{blue}{\sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(2 - ux\right) + ux \cdot maxCos\right)}}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}\]
  14. Using strategy rm

  15. Applied *-un-lft-identity_binary320.6

    \[\leadsto \frac{\sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(2 - ux\right) + ux \cdot maxCos\right)}}{\sqrt{\color{blue}{1 \cdot \left(ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)\right)}}}\]

  16. Applied sqrt-prod_binary320.6

    \[\leadsto \frac{\sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(2 - ux\right) + ux \cdot maxCos\right)}}{\color{blue}{\sqrt{1} \cdot \sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  17. Applied times-frac_binary320.6

    \[\leadsto \color{blue}{\frac{\sin \left(\left(uy \cdot \pi\right) \cdot 2\right)}{\sqrt{1}} \cdot \frac{\sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(2 - ux\right) + ux \cdot maxCos\right)}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}}\]

  18. Simplified0.6

    \[\leadsto \color{blue}{\sin \left(\left(uy \cdot \pi\right) \cdot 2\right)} \cdot \frac{\sqrt{\left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right) \cdot \left(\left(2 - ux\right) + ux \cdot maxCos\right)}}{\sqrt{ux \cdot ux + \left(\left(ux \cdot maxCos\right) \cdot \left(ux \cdot maxCos\right) + ux \cdot \left(ux \cdot maxCos\right)\right)}}\]

  19. Simplified0.6

    \[\leadsto \sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \color{blue}{\frac{\sqrt{\left(\left(2 + ux \cdot maxCos\right) - ux\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{ux \cdot ux + ux \cdot \left(maxCos \cdot \left(ux + ux \cdot maxCos\right)\right)}}}\]

  20. Final simplification0.6

    \[\leadsto \sin \left(\left(uy \cdot \pi\right) \cdot 2\right) \cdot \frac{\sqrt{\left(\left(2 + ux \cdot maxCos\right) - ux\right) \cdot \left({ux}^{3} - {\left(ux \cdot maxCos\right)}^{3}\right)}}{\sqrt{ux \cdot ux + ux \cdot \left(maxCos \cdot \left(ux + ux \cdot maxCos\right)\right)}}\]

Reproduce

herbie shell --seed 2021173 
(FPCore (ux uy maxCos)
  :name "UniformSampleCone, y"
  :precision binary32
  :pre (and (<= 2.328306437e-10 ux 1.0) (<= 2.328306437e-10 uy 1.0) (<= 0.0 maxCos 1.0))
  (* (sin (* (* uy 2.0) PI)) (sqrt (- 1.0 (* (+ (- 1.0 ux) (* ux maxCos)) (+ (- 1.0 ux) (* ux maxCos)))))))