Average Error: 0.0 → 0.0
Time: 22.5s
Precision: binary32
\[\left(\left(2.328306437 \cdot 10^{-10} \leq ux \land ux \leq 1\right) \land \left(2.328306437 \cdot 10^{-10} \leq uy \land uy \leq 1\right)\right) \land \left(0 \leq maxCos \land maxCos \leq 1\right)\]
\[\left(1 - ux\right) + ux \cdot maxCos \]
↓
\[1 + \left(maxCos \cdot ux - ux\right) \]
\left(1 - ux\right) + ux \cdot maxCos
↓
1 + \left(maxCos \cdot ux - ux\right)

(FPCore (ux uy maxCos) :precision binary32 (+ (- 1.0 ux) (* ux maxCos)))
↓
(FPCore (ux uy maxCos) :precision binary32 (+ 1.0 (- (* maxCos ux) ux)))
float code(float ux, float uy, float maxCos) {
	return (1.0f - ux) + (ux * maxCos);
}
↓
float code(float ux, float uy, float maxCos) {
	return 1.0f + ((maxCos * ux) - ux);
}

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 0.0

    \[\left(1 - ux\right) + ux \cdot maxCos \]

  2. Simplified0.0

    \[\leadsto \color{blue}{\mathsf{fma}\left(ux, maxCos, 1 - ux\right)} \]

  3. Applied add-exp-log_binary320.0

    \[\leadsto \color{blue}{e^{\log \left(\mathsf{fma}\left(ux, maxCos, 1 - ux\right)\right)}} \]

  4. Simplified0.0

    \[\leadsto e^{\color{blue}{\mathsf{log1p}\left(maxCos \cdot ux - ux\right)}} \]

  5. Applied log1p-udef_binary320.0

    \[\leadsto e^{\color{blue}{\log \left(1 + \left(maxCos \cdot ux - ux\right)\right)}} \]

  6. Applied rem-exp-log_binary320.0

    \[\leadsto \color{blue}{1 + \left(maxCos \cdot ux - ux\right)} \]

  7. Final simplification0.0

    \[\leadsto 1 + \left(maxCos \cdot ux - ux\right) \]

Reproduce

herbie shell --seed 2022067 
(FPCore (ux uy maxCos)
  :name "UniformSampleCone, z"
  :precision binary32
  :pre (and (and (and (<= 2.328306437e-10 ux) (<= ux 1.0)) (and (<= 2.328306437e-10 uy) (<= uy 1.0))) (and (<= 0.0 maxCos) (<= maxCos 1.0)))
  (+ (- 1.0 ux) (* ux maxCos)))