HairBSDF, Mp, lower

Average Error: 0.1 → 0.1

Time: 19.5s

Precision: binary32

Cost: 10176

\[\left(\left(\left(\left(-1 \leq cosTheta_i \land cosTheta_i \leq 1\right) \land \left(-1 \leq cosTheta_O \land cosTheta_O \leq 1\right)\right) \land \left(-1 \leq sinTheta_i \land sinTheta_i \leq 1\right)\right) \land \left(-1 \leq sinTheta_O \land sinTheta_O \leq 1\right)\right) \land \left(-1.5707964 \leq v \land v \leq 0.1\right)\]

Math

\[e^{\left(\left(\left(\frac{cosTheta_i \cdot cosTheta_O}{v} - \frac{sinTheta_i \cdot sinTheta_O}{v}\right) - \frac{1}{v}\right) + 0.6931\right) + \log \left(\frac{1}{2 \cdot v}\right)} \]

↓

\[0.5 \cdot \left(\left(cosTheta_i \cdot \frac{cosTheta_O}{v} + 1\right) \cdot {\left(\sqrt[3]{\frac{e^{0.6931 + \frac{-1}{v}}}{v}}\right)}^{3}\right) \]

FPCore

(FPCore (cosTheta_i cosTheta_O sinTheta_i sinTheta_O v)
 :precision binary32
 (exp
  (+
   (+
    (-
     (- (/ (* cosTheta_i cosTheta_O) v) (/ (* sinTheta_i sinTheta_O) v))
     (/ 1.0 v))
    0.6931)
   (log (/ 1.0 (* 2.0 v))))))

↓

(FPCore (cosTheta_i cosTheta_O sinTheta_i sinTheta_O v)
 :precision binary32
 (*
  0.5
  (*
   (+ (* cosTheta_i (/ cosTheta_O v)) 1.0)
   (pow (cbrt (/ (exp (+ 0.6931 (/ -1.0 v))) v)) 3.0))))

C

float code(float cosTheta_i, float cosTheta_O, float sinTheta_i, float sinTheta_O, float v) {
	return expf(((((((cosTheta_i * cosTheta_O) / v) - ((sinTheta_i * sinTheta_O) / v)) - (1.0f / v)) + 0.6931f) + logf((1.0f / (2.0f * v)))));
}

↓

float code(float cosTheta_i, float cosTheta_O, float sinTheta_i, float sinTheta_O, float v) {
	return 0.5f * (((cosTheta_i * (cosTheta_O / v)) + 1.0f) * powf(cbrtf((expf((0.6931f + (-1.0f / v))) / v)), 3.0f));
}

Julia

function code(cosTheta_i, cosTheta_O, sinTheta_i, sinTheta_O, v)
	return exp(Float32(Float32(Float32(Float32(Float32(Float32(cosTheta_i * cosTheta_O) / v) - Float32(Float32(sinTheta_i * sinTheta_O) / v)) - Float32(Float32(1.0) / v)) + Float32(0.6931)) + log(Float32(Float32(1.0) / Float32(Float32(2.0) * v)))))
end

↓

function code(cosTheta_i, cosTheta_O, sinTheta_i, sinTheta_O, v)
	return Float32(Float32(0.5) * Float32(Float32(Float32(cosTheta_i * Float32(cosTheta_O / v)) + Float32(1.0)) * (cbrt(Float32(exp(Float32(Float32(0.6931) + Float32(Float32(-1.0) / v))) / v)) ^ Float32(3.0))))
end

Derivation

1. Initial program 0.1

   \[e^{\left(\left(\left(\frac{cosTheta_i \cdot cosTheta_O}{v} - \frac{sinTheta_i \cdot sinTheta_O}{v}\right) - \frac{1}{v}\right) + 0.6931\right) + \log \left(\frac{1}{2 \cdot v}\right)} \]

2. Simplified 0.1

   \[\leadsto \color{blue}{e^{\left(\frac{cosTheta_i}{v} \cdot cosTheta_O - \frac{sinTheta_i}{v} \cdot sinTheta_O\right) + \left(\frac{-1}{v} + 0.6931\right)} \cdot \frac{0.5}{v}} \]
   Proof
   (*.f32 (exp.f32 (+.f32 (-.f32 (*.f32 (/.f32 cosTheta_i v) cosTheta_O) (*.f32 (/.f32 sinTheta_i v) sinTheta_O)) (+.f32 (/.f32 -1 v) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (*.f32 (/.f32 cosTheta_i v) cosTheta_O) (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (+.f32 (/.f32 -1 v) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (Rewrite=> associate-*l/_binary32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (+.f32 (/.f32 -1 v) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (Rewrite<= +-lft-identity_binary32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)))) (+.f32 (/.f32 -1 v) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (+.f32 (/.f32 (Rewrite<= metadata-eval (neg.f32 1)) v) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (+.f32 (Rewrite<= distribute-neg-frac_binary32 (neg.f32 (/.f32 1 v))) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (+.f32 (Rewrite=> neg-sub0_binary32 (-.f32 0 (/.f32 1 v))) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (Rewrite=> associate-+l-_binary32 (-.f32 0 (-.f32 (/.f32 1 v) 6931/10000))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (+.f32 0 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v))) (Rewrite<= neg-sub0_binary32 (neg.f32 (-.f32 (/.f32 1 v) 6931/10000))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (Rewrite<= associate-+r+_binary32 (+.f32 0 (+.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (neg.f32 (-.f32 (/.f32 1 v) 6931/10000)))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 0 (Rewrite<= sub-neg_binary32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (-.f32 (/.f32 1 v) 6931/10000))))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 0 (Rewrite<= associate-+l-_binary32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (Rewrite=> +-lft-identity_binary32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))) (/.f32 1/2 v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (/.f32 (Rewrite<= metadata-eval (/.f32 1 2)) v)): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (Rewrite<= associate-/r*_binary32 (/.f32 1 (*.f32 2 v)))): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (Rewrite<= rem-exp-log_binary32 (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v)))))): 0 points increase in error, 0 points decrease in error
   (*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) (Rewrite<= *-lft-identity_binary32 (*.f32 1 (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v))))))): 0 points increase in error, 0 points decrease in error
   (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)) 1) (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v)))))): 0 points increase in error, 0 points decrease in error
   (*.f32 (Rewrite=> *-commutative_binary32 (*.f32 1 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)))) (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v))))): 0 points increase in error, 0 points decrease in error
   (*.f32 (Rewrite=> *-lft-identity_binary32 (exp.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))) (exp.f32 (log.f32 (/.f32 1 (*.f32 2 v))))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= exp-sum_binary32 (exp.f32 (+.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000) (log.f32 (/.f32 1 (*.f32 2 v)))))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (Rewrite=> +-commutative_binary32 (+.f32 (log.f32 (/.f32 1 (*.f32 2 v))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (+.f32 (Rewrite=> log-div_binary32 (-.f32 (log.f32 1) (log.f32 (*.f32 2 v)))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (+.f32 (-.f32 (Rewrite=> metadata-eval 0) (log.f32 (*.f32 2 v))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (Rewrite=> associate-+l-_binary32 (-.f32 0 (-.f32 (log.f32 (*.f32 2 v)) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (Rewrite<= associate-+l-_binary32 (+.f32 (-.f32 0 (log.f32 (*.f32 2 v))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000)))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (+.f32 (-.f32 (Rewrite<= metadata-eval (log.f32 1)) (log.f32 (*.f32 2 v))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (+.f32 (Rewrite<= log-div_binary32 (log.f32 (/.f32 1 (*.f32 2 v)))) (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000))): 0 points increase in error, 0 points decrease in error
   (exp.f32 (Rewrite<= +-commutative_binary32 (+.f32 (+.f32 (-.f32 (-.f32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v) (/.f32 (*.f32 sinTheta_i sinTheta_O) v)) (/.f32 1 v)) 6931/10000) (log.f32 (/.f32 1 (*.f32 2 v)))))): 0 points increase in error, 0 points decrease in error

3. Taylor expanded in sinTheta_i around 0 0.1

   \[\leadsto \color{blue}{e^{\left(0.6931 + \frac{cosTheta_i \cdot cosTheta_O}{v}\right) - \frac{1}{v}}} \cdot \frac{0.5}{v} \]

4. Taylor expanded in cosTheta_i around 0 13.5

   \[\leadsto \color{blue}{0.5 \cdot \frac{cosTheta_i \cdot \left(cosTheta_O \cdot e^{0.6931 - \frac{1}{v}}\right)}{{v}^{2}} + 0.5 \cdot \frac{e^{0.6931 - \frac{1}{v}}}{v}} \]

5. Simplified 0.1

   \[\leadsto \color{blue}{0.5 \cdot \left(\left(cosTheta_i \cdot \frac{cosTheta_O}{v} + 1\right) \cdot \frac{e^{0.6931 + \frac{-1}{v}}}{v}\right)} \]
   Proof
   (*.f32 1/2 (*.f32 (+.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) 1) (/.f32 (exp.f32 (+.f32 6931/10000 (/.f32 -1 v))) v))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (*.f32 (+.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) 1) (/.f32 (exp.f32 (+.f32 6931/10000 (/.f32 (Rewrite<= metadata-eval (neg.f32 1)) v))) v))): 4 points increase in error, 0 points decrease in error
   (*.f32 1/2 (*.f32 (+.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) 1) (/.f32 (exp.f32 (+.f32 6931/10000 (Rewrite<= distribute-neg-frac_binary32 (neg.f32 (/.f32 1 v))))) v))): 0 points increase in error, 4 points decrease in error
   (*.f32 1/2 (*.f32 (+.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) 1) (/.f32 (exp.f32 (Rewrite<= sub-neg_binary32 (-.f32 6931/10000 (/.f32 1 v)))) v))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (Rewrite<= distribute-lft1-in_binary32 (+.f32 (*.f32 (*.f32 cosTheta_i (/.f32 cosTheta_O v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (+.f32 (*.f32 (Rewrite=> associate-*r/_binary32 (/.f32 (*.f32 cosTheta_i cosTheta_O) v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (+.f32 (Rewrite<= times-frac_binary32 (/.f32 (*.f32 (*.f32 cosTheta_i cosTheta_O) (exp.f32 (-.f32 6931/10000 (/.f32 1 v)))) (*.f32 v v))) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (+.f32 (/.f32 (Rewrite<= associate-*r*_binary32 (*.f32 cosTheta_i (*.f32 cosTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v)))))) (*.f32 v v)) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v))): 0 points increase in error, 0 points decrease in error
   (*.f32 1/2 (+.f32 (/.f32 (*.f32 cosTheta_i (*.f32 cosTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v))))) (Rewrite<= unpow2_binary32 (pow.f32 v 2))) (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v))): 0 points increase in error, 0 points decrease in error
   (Rewrite<= distribute-lft-out_binary32 (+.f32 (*.f32 1/2 (/.f32 (*.f32 cosTheta_i (*.f32 cosTheta_O (exp.f32 (-.f32 6931/10000 (/.f32 1 v))))) (pow.f32 v 2))) (*.f32 1/2 (/.f32 (exp.f32 (-.f32 6931/10000 (/.f32 1 v))) v)))): 0 points increase in error, 0 points decrease in error

6. Applied egg-rr 0.1

   \[\leadsto 0.5 \cdot \left(\left(cosTheta_i \cdot \frac{cosTheta_O}{v} + 1\right) \cdot \color{blue}{{\left(\sqrt[3]{\frac{e^{0.6931 + \frac{-1}{v}}}{v}}\right)}^{3}}\right) \]

7. Final simplification 0.1

   \[\leadsto 0.5 \cdot \left(\left(cosTheta_i \cdot \frac{cosTheta_O}{v} + 1\right) \cdot {\left(\sqrt[3]{\frac{e^{0.6931 + \frac{-1}{v}}}{v}}\right)}^{3}\right) \]

Alternatives

Alternative 1
Error	0.1
Cost	3744

\[0.5 \cdot \left(\left(cosTheta_i \cdot \frac{cosTheta_O}{v} + 1\right) \cdot \frac{e^{0.6931 + \frac{-1}{v}}}{v}\right) \]

Alternative 2
Error	0.1
Cost	3680

\[0.5 \cdot \frac{e^{\left(0.6931 + \frac{cosTheta_i \cdot cosTheta_O}{v}\right) - \frac{1}{v}}}{v} \]

Alternative 3
Error	0.1
Cost	3616

\[0.5 \cdot \frac{e^{0.6931 + \frac{-1 + cosTheta_i \cdot cosTheta_O}{v}}}{v} \]

Alternative 4
Error	0.1
Cost	3488

\[0.5 \cdot \frac{e^{0.6931 + \frac{-1}{v}}}{v} \]

Alternative 5
Error	29.0
Cost	288

\[-0.5 \cdot \frac{sinTheta_i}{\frac{v \cdot v}{sinTheta_O}} \]

Alternative 6
Error	25.2
Cost	288

\[\frac{-0.5}{\frac{v \cdot v}{sinTheta_i \cdot sinTheta_O}} \]

Alternative 7
Error	20.5
Cost	288

\[-0.5 \cdot \frac{\frac{sinTheta_i \cdot sinTheta_O}{v}}{v} \]

Alternative 8
Error	30.5
Cost	96

\[\frac{0.5}{v} \]

Reproduce

herbie shell --seed 2022343 
(FPCore (cosTheta_i cosTheta_O sinTheta_i sinTheta_O v)
  :name "HairBSDF, Mp, lower"
  :precision binary32
  :pre (and (and (and (and (and (<= -1.0 cosTheta_i) (<= cosTheta_i 1.0)) (and (<= -1.0 cosTheta_O) (<= cosTheta_O 1.0))) (and (<= -1.0 sinTheta_i) (<= sinTheta_i 1.0))) (and (<= -1.0 sinTheta_O) (<= sinTheta_O 1.0))) (and (<= -1.5707964 v) (<= v 0.1)))
  (exp (+ (+ (- (- (/ (* cosTheta_i cosTheta_O) v) (/ (* sinTheta_i sinTheta_O) v)) (/ 1.0 v)) 0.6931) (log (/ 1.0 (* 2.0 v))))))