Spherical law of cosines

Time bar (total: 7.4s)

analyze896.0ms (12.1%)

Algorithm
1×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.8%0.2%0%0%0%0
0%0%99.8%0.2%0%0%0%1
0%0%99.8%0.2%0%0%0%2
0%0%99.8%0.2%0%0%0%3
0%0%99.8%0.2%0%0%0%4
0%0%99.8%0.2%0%0%0%5
0%0%99.8%0.2%0%0%0%6
0%0%99.8%0.2%0%0%0%7
0%0%99.8%0.2%0%0%0%8
0%0%99.8%0.2%0%0%0%9
0%0%99.8%0.2%0%0%0%10
1.6%1.6%98.2%0.2%0%0%0%11
1.6%1.6%98.2%0.2%0%0%0%12
Compiler

Compiled 25 to 18 computations (28% saved)

Precisions
Click to see histograms. Total time spent on operations: 566.0ms
ival-mult: 173.0ms (30.6% of total)
ival-cos: 168.0ms (29.7% of total)
ival-sin: 150.0ms (26.5% of total)
ival-acos: 31.0ms (5.5% of total)
ival-sub: 21.0ms (3.7% of total)
ival-add: 21.0ms (3.7% of total)
const: 3.0ms (0.5% of total)

sample5.8s (77.5%)

Results
2.6s2917×1024valid
1.1s3159×256valid
979.0ms1894×512valid
531.0ms286×2048valid
Precisions
Click to see histograms. Total time spent on operations: 4.5s
ival-cos: 1.5s (34.6% of total)
ival-sin: 1.2s (27.5% of total)
ival-acos: 901.0ms (20.2% of total)
ival-mult: 574.0ms (12.9% of total)
ival-sub: 106.0ms (2.4% of total)
ival-add: 96.0ms (2.2% of total)
const: 13.0ms (0.3% of total)
Bogosity

preprocess294.0ms (4%)

Algorithm
1×egg-herbie
Rules
1840×fma-define
664×fma-neg
625×distribute-lft-in
395×distribute-lft-neg-in
374×unsub-neg
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
01391768
13001768
25461752
39691752
417771752
528941752
632821752
740401752
847011752
954921752
1061381752
1164271752
1266211752
1375221752
Stop Event
1×node limit
Calls
Call 1
Inputs
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) (neg.f64 R))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 (neg.f64 phi1)) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 (neg.f64 phi1)) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 (neg.f64 phi2))) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 (neg.f64 phi2))) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) (neg.f64 R)))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))) R))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))) R))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 (neg.f64 phi1)) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 (neg.f64 phi1)) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 (neg.f64 phi2))) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 (neg.f64 phi2))) (cos.f64 (-.f64 lambda1 lambda2))))) R))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 R lambda2))))) lambda1)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 R))))) lambda2)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 R) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 R) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) phi1)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 R)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 R)) (cos.f64 (-.f64 lambda1 lambda2))))) phi2)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 lambda1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 lambda1) (cos.f64 phi2)) (cos.f64 (-.f64 phi1 lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 lambda1)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 lambda1)) (cos.f64 (-.f64 phi2 lambda2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 lambda2) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 lambda2) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 phi1))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 lambda2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 lambda2)) (cos.f64 (-.f64 lambda1 phi2))))) R)
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi2) (sin.f64 phi1)) (*.f64 (*.f64 (cos.f64 phi2) (cos.f64 phi1)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
Outputs
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) R)
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) R)
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) (neg.f64 R))
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) (neg.f64 R))
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) (neg.f64 R))
(*.f64 R (neg.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))))))))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (neg.f64 (+.f64 lambda1 lambda2))))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (+.f64 lambda1 lambda2)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (neg.f64 (+.f64 lambda1 lambda2))))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (+.f64 lambda1 lambda2)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 (neg.f64 phi1)) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 (neg.f64 phi1)) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 R (acos.f64 (fma.f64 (neg.f64 (sin.f64 phi1)) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (acos.f64 (-.f64 (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 (neg.f64 phi2))) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 (neg.f64 phi2))) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 R (acos.f64 (fma.f64 (neg.f64 (sin.f64 phi1)) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (acos.f64 (-.f64 (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) (neg.f64 R)))
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) R)
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2))))) R))
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))) (neg.f64 R))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (neg.f64 (+.f64 lambda1 lambda2))))))))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (+.f64 lambda1 lambda2)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 (neg.f64 lambda2)))))) R))
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 (neg.f64 lambda1) lambda2)))))) (neg.f64 R))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (neg.f64 (+.f64 lambda1 lambda2))))))))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (+.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (+.f64 lambda1 lambda2)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 (neg.f64 phi1)) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 (neg.f64 phi1)) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R))
(*.f64 (acos.f64 (fma.f64 (neg.f64 (sin.f64 phi1)) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) (neg.f64 R))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (neg.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2)))))))
(*.f64 R (neg.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2)))))))
(*.f64 R (neg.f64 (acos.f64 (-.f64 (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2))))))
(neg.f64 (*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 (neg.f64 phi2))) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 (neg.f64 phi2))) (cos.f64 (-.f64 lambda1 lambda2))))) R))
(*.f64 (acos.f64 (fma.f64 (neg.f64 (sin.f64 phi1)) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) (neg.f64 R))
(*.f64 (neg.f64 R) (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2))))))
(*.f64 R (neg.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2)))))))
(*.f64 R (neg.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1))) (*.f64 (sin.f64 phi1) (neg.f64 (sin.f64 phi2)))))))
(*.f64 R (neg.f64 (acos.f64 (-.f64 (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))) (*.f64 (sin.f64 phi1) (sin.f64 phi2))))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 R lambda2))))) lambda1)
(*.f64 lambda1 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 R lambda2)))))))
(*.f64 lambda1 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 R lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 R))))) lambda2)
(*.f64 lambda2 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 R))))))
(*.f64 lambda2 (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 R)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 lambda2 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 R)))))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 R) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 R) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) phi1)
(*.f64 phi1 (acos.f64 (fma.f64 (sin.f64 R) (sin.f64 phi2) (*.f64 (cos.f64 (-.f64 lambda1 lambda2)) (*.f64 (cos.f64 phi2) (cos.f64 R))))))
(*.f64 phi1 (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 R) (*.f64 (cos.f64 (-.f64 lambda1 lambda2)) (*.f64 (cos.f64 phi2) (cos.f64 R))))))
(*.f64 phi1 (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 R) (*.f64 (cos.f64 R) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 phi1 (acos.f64 (fma.f64 (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (cos.f64 phi2) (cos.f64 R)) (*.f64 (sin.f64 phi2) (sin.f64 R)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 R)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 R)) (cos.f64 (-.f64 lambda1 lambda2))))) phi2)
(*.f64 phi2 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 R) (*.f64 (cos.f64 (-.f64 lambda1 lambda2)) (*.f64 (cos.f64 phi1) (cos.f64 R))))))
(*.f64 phi2 (acos.f64 (fma.f64 (cos.f64 (-.f64 lambda1 lambda2)) (*.f64 (cos.f64 phi1) (cos.f64 R)) (*.f64 (sin.f64 phi1) (sin.f64 R)))))
(*.f64 phi2 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 R) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 (-.f64 lambda1 lambda2)) (cos.f64 R))))))
(*.f64 phi2 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 R) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 (-.f64 lambda2 lambda1)) (cos.f64 R))))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1))))) R)
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) R)
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 lambda1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 lambda1) (cos.f64 phi2)) (cos.f64 (-.f64 phi1 lambda2))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 lambda1) (sin.f64 phi2) (*.f64 (cos.f64 lambda1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 phi1 lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 lambda1) (*.f64 (cos.f64 lambda1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 phi1 lambda2)))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 lambda1) (*.f64 (*.f64 (cos.f64 phi2) (cos.f64 lambda1)) (cos.f64 (-.f64 phi1 lambda2))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 lambda1) (*.f64 (cos.f64 phi2) (*.f64 (cos.f64 lambda1) (cos.f64 (-.f64 lambda2 phi1)))))))
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi2) (sin.f64 lambda1) (*.f64 (cos.f64 lambda1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 phi1)))))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 lambda1)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 lambda1)) (cos.f64 (-.f64 phi2 lambda2))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 lambda1) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 lambda1) (cos.f64 (-.f64 phi2 lambda2)))))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 lambda2) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 lambda2) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 phi1))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 lambda2) (sin.f64 phi2) (*.f64 (*.f64 (cos.f64 phi2) (cos.f64 lambda2)) (cos.f64 (-.f64 lambda1 phi1))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi2) (cos.f64 lambda2)) (cos.f64 (-.f64 lambda1 phi1)) (*.f64 (sin.f64 phi2) (sin.f64 lambda2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 lambda2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 lambda2)) (cos.f64 (-.f64 lambda1 phi2))))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 lambda2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 lambda2) (cos.f64 (-.f64 lambda1 phi2)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 lambda2)) (cos.f64 (-.f64 lambda1 phi2)) (*.f64 (sin.f64 phi1) (sin.f64 lambda2)))))
(*.f64 R (acos.f64 (fma.f64 (cos.f64 lambda2) (*.f64 (cos.f64 phi1) (cos.f64 (-.f64 lambda1 phi2))) (*.f64 (sin.f64 phi1) (sin.f64 lambda2)))))
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi2) (sin.f64 phi1)) (*.f64 (*.f64 (cos.f64 phi2) (cos.f64 phi1)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
(*.f64 (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2)))))) R)
(*.f64 (acos.f64 (fma.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda1 lambda2))) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))) R)
(*.f64 R (acos.f64 (fma.f64 (sin.f64 phi1) (sin.f64 phi2) (*.f64 (cos.f64 phi1) (*.f64 (cos.f64 phi2) (cos.f64 (-.f64 lambda2 lambda1)))))))
(*.f64 R (acos.f64 (fma.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda2 lambda1)) (*.f64 (sin.f64 phi1) (sin.f64 phi2)))))
Symmetry

(negabs R)

(sort lambda1 lambda2)

(sort phi1 phi2)

explain416.0ms (5.6%)

FPErrors
Click to see full error table
Ground TruthOverpredictionsExampleUnderpredictionsExampleSubexpression
71126(1.5428304275968285e-150 -2.9796589521564964e+222 1.0665784701214692e-131 -1.3251190805136685e+28 5.6222447694349216e+196)0-(cos.f64 (-.f64 lambda1 lambda2))
110-0-(acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2)))))
00-0-(cos.f64 phi1)
00-0-(+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))
00-0-(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
00-0-(sin.f64 phi2)
00-0-phi1
00-0-(*.f64 (sin.f64 phi1) (sin.f64 phi2))
00-0-(*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2)))
00-0-lambda1
00-0-(cos.f64 phi2)
00-0-(sin.f64 phi1)
00-0-R
00-0-(-.f64 lambda1 lambda2)
00-0-(*.f64 (cos.f64 phi1) (cos.f64 phi2))
00-0-phi2
00-0-lambda2
Results
163.0ms166×1024valid
78.0ms130×512valid
59.0ms196×256valid
38.0ms20×2048valid
Compiler

Compiled 220 to 53 computations (75.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 256.0ms
ival-cos: 78.0ms (30.4% of total)
ival-sin: 73.0ms (28.5% of total)
ival-acos: 57.0ms (22.2% of total)
ival-mult: 34.0ms (13.3% of total)
ival-add: 8.0ms (3.1% of total)
ival-sub: 6.0ms (2.3% of total)
const: 1.0ms (0.4% of total)

eval0.0ms (0%)

Compiler

Compiled 5 to 5 computations (0% saved)

prune1.0ms (0%)

Alt Table
Click to see full alt table
StatusAccuracyProgram
75.2%
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
Compiler

Compiled 48 to 34 computations (29.2% saved)

simplify3.0ms (0%)

Algorithm
1×egg-herbie
Rules
5×*-commutative
3×+-commutative
2×sub-neg
1×neg-sub0
1×neg-mul-1
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
02682
13382
23882
34082
44182
Stop Event
1×saturated
Calls
Call 1
Inputs
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)
Outputs
(*.f64 (acos.f64 (+.f64 (*.f64 (sin.f64 phi1) (sin.f64 phi2)) (*.f64 (*.f64 (cos.f64 phi1) (cos.f64 phi2)) (cos.f64 (-.f64 lambda1 lambda2))))) R)

soundness0.0ms (0%)

Stop Event
1×fuel
Compiler

Compiled 24 to 17 computations (29.2% saved)

preprocess59.0ms (0.8%)

Remove

(sort phi1 phi2)

(sort lambda1 lambda2)

(negabs R)

Compiler

Compiled 384 to 272 computations (29.2% saved)

end0.0ms (0%)

Profiling

Loading profile data...