Herbie run
| Date: | Wednesday, March 26th, 2025 |
|---|---|
| Commit: | a931ba94 on hardware-accelerators |
| Seed: | 2025085 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs default |
| Memory: | 3 603 928.8 MB |
Time bar (total: 51.2min)
| 6.1min | 3 936 807× | 0 | valid |
| 2.1min | 18 390× | 3 | exit |
| 2.0min | 444 308× | 1 | valid |
| 1.1min | 138 920× | 2 | valid |
| 40.0s | 317 343× | 0 | invalid |
| 34.9s | 37 557× | 5 | exit |
| 20.5s | 4 630× | 4 | exit |
| 13.2s | 15 360× | 3 | valid |
| 7.7s | 27 223× | 1 | invalid |
| 6.7s | 50 821× | 0 | exit |
| 680.0ms | 1 495× | 2 | invalid |
| 657.0ms | 5 357× | 1 | exit |
| 98.0ms | 41× | 4 | valid |
| 1.0ms | 1× | 2 | exit |
ival-mult!: 1.8min (18.4% of total)adjust: 55.1s (9.3% of total)ival-div!: 49.4s (8.4% of total)ival-pow: 46.9s (8% of total)ival-exp: 39.8s (6.7% of total)ival-log: 38.9s (6.6% of total)ival-pow2: 33.1s (5.6% of total)ival-sub!: 31.8s (5.4% of total)ival-add!: 30.6s (5.2% of total)ival-cos: 25.7s (4.4% of total)ival-sin: 24.3s (4.1% of total)ival-sqrt: 23.3s (4% of total)ival-tan: 15.5s (2.6% of total)ival-neg: 13.8s (2.3% of total)ival-sinu: 7.7s (1.3% of total)ival-cosu: 5.8s (1% of total)ival-hypot: 4.6s (0.8% of total)ival-fmax: 4.3s (0.7% of total)ival-fabs: 4.2s (0.7% of total)ival-fmin: 4.1s (0.7% of total)ival-expm1: 3.8s (0.6% of total)ival-atan: 3.5s (0.6% of total)ival-acos: 2.3s (0.4% of total)ival-atan2: 1.6s (0.3% of total)ival-log1p: 1.5s (0.3% of total)ival-<=: 1.2s (0.2% of total)ival-sinh: 1.1s (0.2% of total)ival-asin: 1.0s (0.2% of total)ival-floor: 871.0ms (0.1% of total)ival-fmod: 767.0ms (0.1% of total)ival-and: 751.0ms (0.1% of total)ival-<: 661.0ms (0.1% of total)ival-cbrt: 570.0ms (0.1% of total)ival-cosh: 420.0ms (0.1% of total)ival-acosh: 352.0ms (0.1% of total)ival-asinh: 316.0ms (0.1% of total)ival-if: 259.0ms (0% of total)const: 254.0ms (0% of total)ival-log2: 232.0ms (0% of total)ival-tanu: 197.0ms (0% of total)ival-atanh: 166.0ms (0% of total)ival-tanh: 132.0ms (0% of total)ival-assert: 106.0ms (0% of total)ival->=: 59.0ms (0% of total)ival->: 56.0ms (0% of total)ival-or: 16.0ms (0% of total)ival-==: 3.0ms (0% of total)ival-pi: 0.0ms (0% of total)| 4 674× | iter limit |
| 1 810× | node limit |
| 123× | unsound |
| 35× | saturated |
| 7.7s | 98 540× | 0 | valid |
| 5.3s | 67 477× | 0 | invalid |
| 90.0ms | 343× | 1 | valid |
| 3.0ms | 23× | 3 | valid |
| 2.0ms | 17× | 2 | valid |
Compiled 238 244 943 to 3 966 688 computations (98.3% saved)
ival-mult!: 5.1s (76.6% of total)ival-add!: 1.5s (22.8% of total)adjust: 38.0ms (0.6% of total)| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 8793 | 65 |
sqrt.f64 | #f | oflow-rescue | 8033 | 0 |
cos.f64 | #f | sensitivity | 3757 | 14 |
log.f64 | #f | sensitivity | 3673 | 9 |
+.f64 | #f | cancellation | 3103 | 141 |
sin.f64 | #f | sensitivity | 2425 | 4 |
/.f64 | #f | o/n | 1996 | 0 |
/.f64 | #f | o/o | 1773 | 0 |
-.f64 | #f | nan-rescue | 1470 | 0 |
log.f32 | #f | sensitivity | 1155 | 70 |
*.f64 | #f | n*o | 1095 | 0 |
/.f64 | #f | n/o | 1007 | 0 |
sqrt.f64 | #f | uflow-rescue | 1002 | 0 |
/.f64 | #f | u/u | 981 | 0 |
+.f64 | #f | nan-rescue | 786 | 0 |
/.f64 | #f | u/n | 688 | 0 |
sqrt.f32 | #f | oflow-rescue | 578 | 0 |
acos.f64 | #f | sensitivity | 528 | 6 |
*.f64 | #f | n*u | 499 | 0 |
tan.f64 | #f | sensitivity | 432 | 1 |
pow.f64 | #f | sensitivity | 427 | 36 |
-.f32 | #f | cancellation | 407 | 22 |
/.f64 | #f | n/u | 322 | 0 |
exp.f64 | #f | sensitivity | 208 | 26 |
cos.f64 | #f | oflow-rescue | 208 | 0 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 203 | 0 |
cos.f32 | #f | sensitivity | 197 | 17 |
tan.f32 | (tan.f32 (+.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u1) (*.f32 #s(literal 1/2 binary32) (PI.f32)))) | cancellation | 187 | 18 |
*.f64 | #f | u*o | 171 | 0 |
*.f64 | #f | o*u | 163 | 0 |
/.f32 | #f | o/n | 142 | 0 |
asin.f64 | #f | sensitivity | 140 | 1 |
pow.f64 | #f | oflow-rescue | 137 | 0 |
log.f64 | #f | oflow-rescue | 92 | 0 |
cbrt.f64 | #f | oflow-rescue | 89 | 0 |
log.f64 | #f | uflow-rescue | 72 | 0 |
pow.f64 | #f | uflow-rescue | 58 | 0 |
sin.f64 | #f | oflow-rescue | 35 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 34 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 34 | |
exp.f32 | #f | sensitivity | 33 | 12 |
cbrt.f64 | #f | uflow-rescue | 27 | 0 |
/.f32 | #f | u/n | 17 | 0 |
sqrt.f32 | (sqrt.f32 (-.f32 (*.f32 eta eta) (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O)))))) | uflow-rescue | 16 | 0 |
| ↳ | (*.f32 sinTheta_O sinTheta_O) | underflow | 276 | |
| ↳ | (-.f32 (*.f32 eta eta) (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O))))) | underflow | 16 | |
| ↳ | (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O)))) | underflow | 138 | |
| ↳ | (*.f32 eta eta) | underflow | 16 | |
/.f32 | #f | o/o | 8 | 0 |
log.f32 | #f | oflow-rescue | 5 | 0 |
/.f32 | (/.f32 (neg.f32 (log.f32 (-.f32 #s(literal 1 binary32) u0))) (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay)))) | n/o | 4 | 0 |
| ↳ | (/.f32 sin2phi (*.f32 alphay alphay)) | overflow | 12 | |
| ↳ | (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay))) | overflow | 12 | |
tan.f64 | (tan.f64 (+.f64 y z)) | cancellation | 1 | 0 |
*.f32 | (*.f32 (sin.f32 (*.f32 u normAngle)) (/.f32 #s(literal 1 binary32) (sin.f32 normAngle))) | n*u | 1 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 31202 | 921 |
| - | 6320 | 101845 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 31202 | 265 | 656 |
| - | 6320 | 405 | 101440 |
| number | freq |
|---|---|
| 0 | 102766 |
| 1 | 31012 |
| 2 | 5060 |
| 3 | 688 |
| 4 | 295 |
| 5 | 213 |
| 6 | 70 |
| 7 | 55 |
| 8 | 7 |
| 9 | 1 |
| 16 | 27 |
| 17 | 66 |
| 21 | 28 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 347 | 1 | 4 |
| - | 17 | 3 | 176 |
| 24.1s | 234 990× | 0 | valid |
| 10.2s | 32 872× | 1 | valid |
| 6.2s | 11 334× | 2 | valid |
| 1.0s | 1 202× | 3 | valid |
| 1.0s | 56× | 5 | exit |
| 235.0ms | 20× | 4 | valid |
| 14.0ms | 104× | 1 | exit |
Compiled 9 324 402 to 30 069 computations (99.7% saved)
ival-mult!: 7.2s (26.7% of total)adjust: 2.2s (8.1% of total)ival-div!: 2.0s (7.4% of total)ival-sin: 1.9s (7.2% of total)ival-cos: 1.8s (6.5% of total)ival-log: 1.7s (6.3% of total)ival-add!: 1.4s (5.3% of total)ival-sub!: 1.4s (5.2% of total)ival-sqrt: 1.1s (4% of total)ival-tan: 1.0s (3.8% of total)ival-exp: 921.0ms (3.4% of total)ival-pow2: 795.0ms (2.9% of total)ival-fmax: 695.0ms (2.6% of total)ival-pow: 440.0ms (1.6% of total)ival-cosu: 354.0ms (1.3% of total)ival-sinu: 318.0ms (1.2% of total)ival-neg: 314.0ms (1.2% of total)ival-fmin: 249.0ms (0.9% of total)ival-hypot: 248.0ms (0.9% of total)ival-atan2: 207.0ms (0.8% of total)ival-log1p: 122.0ms (0.5% of total)ival-fabs: 86.0ms (0.3% of total)ival-acos: 83.0ms (0.3% of total)ival-sinh: 73.0ms (0.3% of total)ival-atan: 67.0ms (0.2% of total)ival-if: 54.0ms (0.2% of total)ival-floor: 45.0ms (0.2% of total)ival-cbrt: 36.0ms (0.1% of total)ival-fmod: 29.0ms (0.1% of total)ival-copysign: 27.0ms (0.1% of total)ival-expm1: 26.0ms (0.1% of total)ival-asin: 20.0ms (0.1% of total)ival-tanu: 14.0ms (0.1% of total)ival-log2: 14.0ms (0.1% of total)ival-cosh: 12.0ms (0% of total)ival-tanh: 7.0ms (0% of total)ival->=: 6.0ms (0% of total)const: 4.0ms (0% of total)ival->: 3.0ms (0% of total)ival-<: 1.0ms (0% of total)ival-pi: 0.0ms (0% of total)| 2.1s | 29 983× | 0 | valid |
| 553.0ms | 7 642× | 0 | invalid |
| 1.0ms | 7× | 1 | valid |
Compiled 3 223 463 to 1 425 415 computations (55.8% saved)
ival-mult!: 878.0ms (66% of total)ival-add!: 446.0ms (33.5% of total)adjust: 7.0ms (0.5% of total)| 1 094× | iter limit |
| 804× | node limit |
| 294× | saturated |
| 6.4s | 76 105× | 0 | valid |
| 441.0ms | 6 454× | 0 | invalid |
| 0.0ms | 1× | 1 | valid |
Compiled 809 288 to 147 514 computations (81.8% saved)
ival-mult!: 3.2s (82% of total)ival-add!: 692.0ms (17.6% of total)adjust: 15.0ms (0.4% of total)1 236 calls:
| 13.1s | x |
| 9.3s | y |
| 8.4s | z |
| 5.1s | a |
| 4.9s | t |
Compiled 121 437 to 124 034 computations (-2.1% saved)
16275 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 3.4s | x | @ | -inf | ((- (- (* x (log y)) z) y) (- (* x (log y)) z) (* (+ (* (/ (log y) z) x) -1) z) (+ (* (/ (log y) z) x) -1) (/ (log y) z) (log y) y z x -1 (- (- (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) z) y) (neg z) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (neg z) x) (- (- (* x (log y)) z) y) (* (log y) x) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (+ z y) x) (+ z y)) |
| 1.0s | ew | @ | inf | ((fabs (+ (* eh (* (cos t) (tanh (asinh (/ (/ eh ew) (tan t)))))) (* (* (sin t) ew) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))))))) (+ (* eh (* (cos t) (tanh (asinh (/ (/ eh ew) (tan t)))))) (* (* (sin t) ew) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2)))))) eh (* (cos t) (tanh (asinh (/ (/ eh ew) (tan t))))) (cos t) t (tanh (asinh (/ (/ eh ew) (tan t)))) (asinh (/ (/ eh ew) (tan t))) (/ (/ eh ew) (tan t)) (/ eh ew) ew (tan t) (* (* (sin t) ew) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))))) (* (sin t) ew) (sin t) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2)))) 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))) (+ 1 (pow (/ (/ eh ew) (tan t)) 2)) (pow (/ (/ eh ew) (tan t)) 2) 2 (fabs (+ (* (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t))))))) (+ (* (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t)))))) (* ew (sin t)) (fabs (+ (* (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t))))))) (+ (* (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t)))))) (* (tanh (asinh (* (/ (cos t) ew) (/ eh (sin t))))) eh) (tanh (asinh (* (/ (cos t) ew) (/ eh (sin t))))) (asinh (* (/ (cos t) ew) (/ eh (sin t)))) (* (/ (cos t) ew) (/ eh (sin t))) (/ (cos t) ew) (/ eh (sin t)) (sin t) (fabs (+ (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t))))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t))))))) (+ (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t))))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t)))))) (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t))))))) (/ 1 (sqrt (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t)))))) (sqrt (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t))))) (+ 1 (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t)))) (* (/ (/ eh ew) (tan t)) (/ (/ eh ew) (tan t))) (/ (/ eh ew) (tan t)) (tan t) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t))))) (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t)))) (atan (/ (/ eh ew) (tan t))) (fabs (+ (* eh (* (cos t) (tanh (asinh (/ (/ eh ew) (tan t)))))) (* (* (sin t) ew) (cos (atan (/ (/ eh ew) (tan t))))))) (+ (* eh (* (cos t) (tanh (asinh (/ (/ eh ew) (tan t)))))) (* (* (sin t) ew) (cos (atan (/ (/ eh ew) (tan t)))))) (+ (* ew (* (cos (atan (/ (* eh (cos t)) (* ew (sin t))))) (sin t))) (/ (pow (* eh (cos t)) 2) (* ew (sin t)))) (* (cos (atan (/ (* eh (cos t)) (* ew (sin t))))) (sin t)) (cos (atan (/ (* eh (cos t)) (* ew (sin t))))) (atan (/ (* eh (cos t)) (* ew (sin t)))) (/ (* eh (cos t)) (* ew (sin t))) (/ (pow (* eh (cos t)) 2) (* ew (sin t))) (pow (* eh (cos t)) 2)) |
| 986.0ms | R | @ | 0 | ((* R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))))) R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))))) 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))) (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))) (pow (sin (/ (- phi1 phi2) 2)) 2) (sin (/ (- phi1 phi2) 2)) (/ (- phi1 phi2) 2) (- phi1 phi2) phi1 phi2 (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))) (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (* (cos phi1) (cos phi2)) (cos phi1) (cos phi2) (sin (/ (- lambda1 lambda2) 2)) (/ (- lambda1 lambda2) 2) (- lambda1 lambda2) lambda1 lambda2 (sqrt (- 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))) (- 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) 1 (+ (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))) (pow (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) 2) (- (* (sin (/ phi1 2)) (cos (/ phi2 2))) (* (cos (/ phi1 2)) (sin (/ phi2 2)))) (* (sin (/ phi1 2)) (cos (/ phi2 2))) (sin (/ phi1 2)) (/ phi1 2) (cos (/ phi2 2)) (/ phi2 2) (* (cos (/ phi1 2)) (sin (/ phi2 2))) (cos (/ phi1 2)) (sin (/ phi2 2)) (* (* (atan2 (sqrt (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))) (sqrt (- 1 (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))))) 2) R) (* (atan2 (sqrt (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))) (sqrt (- 1 (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))))) 2) (atan2 (sqrt (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))) (sqrt (- 1 (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))))) (sqrt (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))) (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2)) (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2))))) 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))) (cos (* 2 (/ (- lambda1 lambda2) 2))) (* 2 (/ (- lambda1 lambda2) 2)) (sqrt (- 1 (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2)))) (- 1 (+ (* (* (cos phi2) (cos phi1)) (- 1/2 (* 1/2 (cos (* 2 (/ (- lambda1 lambda2) 2)))))) (pow (sin (/ (- phi1 phi2) 2)) 2))) (* R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))))) (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))))) (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))) (sqrt (- 1 (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))) (- 1 (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (+ (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))) (- 1/2 (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2))))) (* 1/2 (cos (* 2 (/ (- phi1 phi2) 2)))) (cos (* 2 (/ (- phi1 phi2) 2))) (* 2 (/ (- phi1 phi2) 2)) (* R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))))) (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))))) (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))) (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))) (pow (sin (/ (- phi1 phi2) 2)) 2) (sin (/ (- phi1 phi2) 2)) (/ (- phi1 phi2) 2) (* (- (* (/ phi1 phi2) 1/2) 1/2) phi2) (- (* (/ phi1 phi2) 1/2) 1/2) (* (/ phi1 phi2) 1/2) (/ phi1 phi2) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))) (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (* R (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))))) (* 2 (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))))))) (atan2 (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (sqrt (- 1 (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))))) (sqrt (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))))) (+ (pow (sin (/ (- phi1 phi2) 2)) 2) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)))) (* (* (* (cos phi1) (cos phi2)) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2))) (sin (/ (- lambda1 lambda2) 2)) (+ (* (* 1/2 lambda1) (cos (* -1/2 lambda2))) (sin (* -1/2 lambda2))) (* 1/2 lambda1) (cos (* -1/2 lambda2)) (* -1/2 lambda2) -1/2 (sin (* -1/2 lambda2))) |
| 984.0ms | x | @ | -inf | ((log (+ x (sqrt (- (* x x) 1)))) (+ (neg (neg (log x))) (log 2)) (neg (neg (log x))) (neg (log x)) (log x) x (log 2) 2) |
| 776.0ms | M | @ | inf | ((* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (/ (* (* (pow (* (/ M 2) (/ D d)) 2) 1/2) h) l))) (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (pow (/ d h) (/ 1 2)) (/ d h) d h (/ 1 2) 1 2 (pow (/ d l) (/ 1 2)) (/ d l) l (- 1 (/ (* (* (pow (* (/ M 2) (/ D d)) 2) 1/2) h) l)) (/ (* (* (pow (* (/ M 2) (/ D d)) 2) 1/2) h) l) (* (* (pow (* (/ M 2) (/ D d)) 2) 1/2) h) (* (pow (* (/ M 2) (/ D d)) 2) 1/2) (pow (* (/ M 2) (/ D d)) 2) (* (/ M 2) (/ D d)) (/ M 2) M (/ D d) D 1/2 (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) (* (sqrt (pow (* l h) -1)) d) (sqrt (pow (* l h) -1)) (pow (* l h) -1) (* l h) -1 (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) (* (* -1/8 (/ (pow (* D M) 2) d)) (sqrt (/ h (pow l 3)))) (* -1/8 (/ (pow (* D M) 2) d)) -1/8 (/ (pow (* D M) 2) d) (pow (* D M) 2) (* D M) (sqrt (/ h (pow l 3))) (/ h (pow l 3)) (pow l 3) 3 (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (* (* -1 d) (sqrt (pow (* l h) -1))) (* -1 d) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l))) (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)) (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (pow (/ (* M D) (* 2 d)) 2) (/ (* M D) (* 2 d)) (* M D) (* 2 d) (/ h l) (* (* (pow (/ d h) (/ 1 2)) (pow (/ d l) (/ 1 2))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l)))) (- 1 (* (* (/ 1 2) (pow (/ (* M D) (* 2 d)) 2)) (/ h l))) (/ (- l (/ (* 1/8 (* (pow (* D M) 2) h)) (* d d))) l) (- l (/ (* 1/8 (* (pow (* D M) 2) h)) (* d d))) (/ (* 1/8 (* (pow (* D M) 2) h)) (* d d)) (* 1/8 (* (pow (* D M) 2) h)) 1/8 (* (pow (* D M) 2) h) (* d d)) |
| 354× | fuel |
| 192× | done |
| 132.0ms | 2 340× | 0 | valid |
| 17.0ms | 219× | 0 | invalid |
| 0.0ms | 1× | 1 | valid |
Compiled 329 733 to 43 266 computations (86.9% saved)
ival-mult!: 53.0ms (67% of total)ival-add!: 26.0ms (32.9% of total)adjust: 1.0ms (1.3% of total)| 554× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 84.7% | 15.3% | 0% | 0% | 0% | 0 |
| 39.5% | 33.4% | 51.2% | 15.3% | 0% | 0% | 0% | 1 |
| 45.4% | 38.1% | 45.8% | 15.3% | 0% | 0.8% | 0% | 2 |
| 53.9% | 44.1% | 37.8% | 15.3% | 0% | 2.8% | 0% | 3 |
| 60.6% | 49.1% | 31.9% | 15.3% | 0% | 3.7% | 0% | 4 |
| 66.9% | 53.9% | 26.6% | 15.3% | 0% | 4.2% | 0% | 5 |
| 70.9% | 56.8% | 23.3% | 15.3% | 0% | 4.6% | 0% | 6 |
| 74.9% | 59.5% | 20% | 15.3% | 0% | 5.2% | 0% | 7 |
| 76.9% | 60.9% | 18.3% | 15.3% | 0% | 5.6% | 0% | 8 |
| 79.6% | 62.7% | 16.1% | 15.3% | 0% | 5.9% | 0% | 9 |
| 81.1% | 63.7% | 14.8% | 15.3% | 0% | 6.2% | 0% | 10 |
| 83.4% | 65.4% | 13% | 15.3% | 0% | 6.3% | 0% | 11 |
| 84.5% | 66.1% | 12.1% | 15.3% | 0% | 6.5% | 0% | 12 |
Compiled 60 013 to 16 996 computations (71.7% saved)
| 2 996× | binary-search |
| 1 781× | left-value |
| 2 900× | narrow-enough |
| 87× | predicate-same |
| 9× | predicate-failed |
| 21.4s | 208 901× | 0 | valid |
| 6.6s | 16 202× | 1 | valid |
| 1.1s | 2 477× | 2 | valid |
| 1.1s | 10 768× | 0 | invalid |
| 128.0ms | 324× | 3 | valid |
| 64.0ms | 223× | 1 | invalid |
| 13.0ms | 39× | 2 | invalid |
| 4.0ms | 61× | 0 | exit |
| 0.0ms | 3× | 1 | exit |
Compiled 1 662 344 to 1 120 918 computations (32.6% saved)
ival-mult!: 7.1s (33.5% of total)ival-sin: 2.2s (10.6% of total)ival-cos: 2.2s (10.4% of total)ival-sub!: 1.6s (7.7% of total)ival-div!: 1.6s (7.6% of total)ival-add!: 1.3s (6.2% of total)adjust: 885.0ms (4.2% of total)ival-log: 658.0ms (3.1% of total)ival-pow2: 587.0ms (2.8% of total)ival-pow: 543.0ms (2.6% of total)ival-exp: 484.0ms (2.3% of total)ival-sqrt: 463.0ms (2.2% of total)ival-tan: 279.0ms (1.3% of total)ival-neg: 234.0ms (1.1% of total)ival-atan2: 185.0ms (0.9% of total)ival-hypot: 156.0ms (0.7% of total)ival-sinu: 124.0ms (0.6% of total)ival-cosu: 110.0ms (0.5% of total)ival-fabs: 66.0ms (0.3% of total)ival-acos: 59.0ms (0.3% of total)ival-fmod: 50.0ms (0.2% of total)ival-sinh: 44.0ms (0.2% of total)ival-atan: 37.0ms (0.2% of total)ival-tanh: 30.0ms (0.1% of total)ival-fmax: 27.0ms (0.1% of total)ival-if: 13.0ms (0.1% of total)ival-cosh: 10.0ms (0% of total)ival-tanu: 9.0ms (0% of total)ival-asin: 9.0ms (0% of total)ival-log1p: 9.0ms (0% of total)ival->=: 9.0ms (0% of total)ival-fmin: 6.0ms (0% of total)ival-expm1: 6.0ms (0% of total)ival-cbrt: 4.0ms (0% of total)const: 0.0ms (0% of total)ival-pi: 0.0ms (0% of total)| 444× | node limit |
| 102× | saturated |
Loading profile data...