
| Date: | Thursday, February 20th, 2025 |
|---|---|
| Commit: | 87019920 on main |
| Seed: | 2025051 |
| 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 724 359.4 MB |
Time bar (total: 53.4min)
| 7.6min | 3 947 307× | 0 | valid |
| 3.7min | 51 282× | 5 | exit |
| 2.5min | 440 255× | 1 | valid |
| 1.2min | 139 643× | 2 | valid |
| 47.6s | 320 205× | 0 | invalid |
| 15.0s | 14 640× | 3 | valid |
| 8.6s | 28 212× | 1 | invalid |
| 7.1s | 49 695× | 0 | exit |
| 1.1s | 2 435× | 2 | invalid |
| 260.0ms | 41× | 4 | valid |
| 107.0ms | 1× | 4 | exit |
| 22.0ms | 33× | 1 | exit |
| 3.0ms | 1× | 3 | exit |
| 2.0ms | 1× | 2 | exit |
ival-mult: 2.3min (18.4% of total)ival-pow: 1.4min (11.6% of total)ival-div: 1.0min (8.4% of total)adjust: 59.5s (8.1% of total)ival-add: 54.3s (7.4% of total)ival-sub: 52.5s (7.1% of total)const: 45.0s (6.1% of total)ival-log: 36.5s (4.9% of total)ival-exp: 36.2s (4.9% of total)ival-cos: 26.1s (3.5% of total)ival-sin: 24.6s (3.3% of total)ival-pow2: 21.2s (2.9% of total)ival-sqrt: 21.2s (2.9% of total)ival-tan: 15.7s (2.1% of total)ival-sinu: 7.0s (0.9% of total)ival-neg: 6.9s (0.9% of total)ival-cosu: 6.2s (0.8% of total)ival-fabs: 4.3s (0.6% of total)ival-hypot: 3.8s (0.5% of total)exact: 3.4s (0.5% of total)ival-fmax: 3.1s (0.4% of total)ival-fmin: 2.8s (0.4% of total)ival-log1p: 2.7s (0.4% of total)ival-expm1: 2.5s (0.3% of total)ival-e: 2.4s (0.3% of total)ival-asin: 1.8s (0.2% of total)ival-acos: 1.7s (0.2% of total)ival-atan2: 1.7s (0.2% of total)ival-assert: 1.6s (0.2% of total)ival-sinh: 1.5s (0.2% of total)ival-pi: 1.5s (0.2% of total)ival-<=: 1.0s (0.1% of total)ival-atan: 1.0s (0.1% of total)ival-fmod: 872.0ms (0.1% of total)ival-and: 826.0ms (0.1% of total)ival-floor: 763.0ms (0.1% of total)ival-<: 616.0ms (0.1% of total)ival-cbrt: 586.0ms (0.1% of total)ival-cosh: 327.0ms (0% of total)ival-asinh: 300.0ms (0% of total)ival-acosh: 282.0ms (0% of total)ival-if: 280.0ms (0% of total)ival-atanh: 256.0ms (0% of total)ival-log2: 243.0ms (0% of total)ival-tanu: 177.0ms (0% of total)ival-tanh: 135.0ms (0% of total)ival->=: 53.0ms (0% of total)ival->: 51.0ms (0% of total)ival-or: 18.0ms (0% of total)ival-==: 10.0ms (0% of total)ival-true: 10.0ms (0% of total)| 4 640× | iter limit |
| 1 813× | node limit |
| 118× | unsound |
| 35× | saturated |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 9063 | 51 |
sqrt.f64 | #f | oflow-rescue | 8203 | 0 |
cos.f64 | #f | sensitivity | 3788 | 5 |
log.f64 | #f | sensitivity | 3687 | 10 |
+.f64 | #f | cancellation | 3054 | 108 |
sin.f64 | #f | sensitivity | 2431 | 1 |
/.f64 | #f | o/n | 2041 | 0 |
/.f64 | #f | o/o | 1836 | 0 |
-.f64 | #f | nan-rescue | 1475 | 0 |
*.f64 | #f | n*o | 1154 | 0 |
log.f32 | #f | sensitivity | 1140 | 83 |
/.f64 | #f | u/u | 982 | 0 |
/.f64 | #f | n/o | 970 | 0 |
sqrt.f64 | #f | uflow-rescue | 871 | 0 |
+.f64 | #f | nan-rescue | 842 | 0 |
/.f64 | #f | u/n | 671 | 0 |
sqrt.f32 | #f | oflow-rescue | 539 | 0 |
acos.f64 | #f | sensitivity | 530 | 3 |
*.f64 | #f | n*u | 457 | 0 |
pow.f64 | #f | sensitivity | 431 | 43 |
tan.f64 | #f | sensitivity | 394 | 0 |
-.f32 | #f | cancellation | 385 | 26 |
/.f64 | #f | n/u | 356 | 0 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 224 | 0 |
cos.f32 | (cos.f32 (atan.f32 (*.f32 (/.f32 alphay alphax) (tan.f32 (+.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u1) (*.f32 #s(literal 1/2 binary32) (PI.f32))))))) | sensitivity | 191 | 15 |
tan.f32 | (tan.f32 (+.f32 (*.f32 (*.f32 #s(literal 2 binary32) (PI.f32)) u1) (*.f32 #s(literal 1/2 binary32) (PI.f32)))) | cancellation | 190 | 15 |
cos.f64 | #f | oflow-rescue | 185 | 0 |
*.f64 | #f | u*o | 183 | 0 |
exp.f64 | #f | sensitivity | 181 | 41 |
pow.f64 | #f | oflow-rescue | 157 | 0 |
*.f64 | #f | o*u | 140 | 0 |
asin.f64 | (asin.f64 (sqrt.f64 (/.f64 (-.f64 #s(literal 1 binary64) (pow.f64 (/.f64 Om Omc) #s(literal 2 binary64))) (+.f64 #s(literal 1 binary64) (*.f64 #s(literal 2 binary64) (pow.f64 (/.f64 t l) #s(literal 2 binary64))))))) | sensitivity | 132 | 1 |
/.f32 | #f | o/n | 128 | 0 |
cbrt.f64 | #f | oflow-rescue | 110 | 0 |
log.f64 | #f | oflow-rescue | 93 | 0 |
pow.f64 | #f | uflow-rescue | 75 | 0 |
log.f64 | #f | uflow-rescue | 69 | 0 |
cbrt.f64 | #f | uflow-rescue | 53 | 0 |
exp.f32 | #f | sensitivity | 50 | 14 |
sin.f64 | #f | oflow-rescue | 32 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 29 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 29 | |
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 | 21 | 0 |
| ↳ | (*.f32 sinTheta_O sinTheta_O) | underflow | 312 | |
| ↳ | (-.f32 (*.f32 eta eta) (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O))))) | underflow | 21 | |
| ↳ | (/.f32 (*.f32 sinTheta_O sinTheta_O) (sqrt.f32 (-.f32 #s(literal 1 binary32) (*.f32 sinTheta_O sinTheta_O)))) | underflow | 156 | |
| ↳ | (*.f32 eta eta) | underflow | 21 | |
/.f32 | #f | u/n | 21 | 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 | 6 | 0 |
| ↳ | (/.f32 sin2phi (*.f32 alphay alphay)) | overflow | 10 | |
| ↳ | (+.f32 (/.f32 cos2phi (*.f32 alphax alphax)) (/.f32 sin2phi (*.f32 alphay alphay))) | overflow | 10 | |
/.f32 | #f | o/o | 6 | 0 |
*.f32 | (*.f32 (sin.f32 (*.f32 u normAngle)) (/.f32 #s(literal 1 binary32) (sin.f32 normAngle))) | n*u | 4 | 0 |
log.f32 | #f | oflow-rescue | 3 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 31420 | 900 |
| - | 6378 | 101846 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 31420 | 236 | 664 |
| - | 6378 | 417 | 101429 |
| number | freq |
|---|---|
| 0 | 102746 |
| 1 | 31387 |
| 2 | 4924 |
| 3 | 644 |
| 4 | 341 |
| 5 | 231 |
| 6 | 74 |
| 7 | 60 |
| 8 | 6 |
| 9 | 6 |
| 16 | 43 |
| 17 | 51 |
| 21 | 31 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 343 | 2 | 3 |
| - | 15 | 1 | 185 |
| 28.4s | 236 227× | 0 | valid |
| 12.7s | 32 168× | 1 | valid |
| 8.4s | 11 342× | 2 | valid |
| 1.5s | 144× | 5 | exit |
| 1.2s | 1 180× | 3 | valid |
| 239.0ms | 28× | 4 | valid |
Compiled 9 324 519 to 30 106 computations (99.7% saved)
ival-mult: 7.2s (19.7% of total)adjust: 3.3s (9.2% of total)ival-div: 3.0s (8.3% of total)ival-add: 3.0s (8.3% of total)ival-sin: 2.9s (8.1% of total)ival-sub: 2.8s (7.9% of total)ival-cos: 2.2s (6.2% of total)const: 2.0s (5.4% of total)ival-log: 1.4s (3.8% of total)ival-exp: 955.0ms (2.6% of total)ival-sqrt: 860.0ms (2.4% of total)ival-tan: 840.0ms (2.3% of total)ival-pow2: 815.0ms (2.2% of total)ival-fmax: 769.0ms (2.1% of total)ival-pow: 682.0ms (1.9% of total)ival-cosu: 453.0ms (1.2% of total)ival-sinu: 409.0ms (1.1% of total)ival-neg: 330.0ms (0.9% of total)ival-fmin: 256.0ms (0.7% of total)ival-true: 241.0ms (0.7% of total)ival-hypot: 232.0ms (0.6% of total)exact: 184.0ms (0.5% of total)ival-fabs: 157.0ms (0.4% of total)ival-log1p: 154.0ms (0.4% of total)ival-asin: 131.0ms (0.4% of total)ival-acos: 129.0ms (0.4% of total)ival-assert: 119.0ms (0.3% of total)ival-atan2: 114.0ms (0.3% of total)ival-pi: 103.0ms (0.3% of total)ival-fmod: 70.0ms (0.2% of total)ival-atan: 64.0ms (0.2% of total)ival-sinh: 61.0ms (0.2% of total)ival-if: 45.0ms (0.1% of total)ival-cbrt: 41.0ms (0.1% of total)ival-floor: 40.0ms (0.1% of total)ival-e: 26.0ms (0.1% of total)ival-expm1: 26.0ms (0.1% of total)ival-cosh: 17.0ms (0% of total)ival-copysign: 12.0ms (0% of total)ival-log2: 12.0ms (0% of total)ival-tanu: 11.0ms (0% of total)ival-tanh: 7.0ms (0% of total)ival->=: 6.0ms (0% of total)ival->: 3.0ms (0% of total)ival-<: 1.0ms (0% of total)Compiled 236 210 036 to 3 880 696 computations (98.4% saved)
Compiled 3 338 898 to 1 483 096 computations (55.6% saved)
1 241 calls:
| 15.6s | x |
| 9.8s | y |
| 9.0s | z |
| 5.4s | b |
| 5.1s | a |
Compiled 124 212 to 128 126 computations (-3.2% saved)
16293 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 2.9s | y | @ | -inf | ((+ (* (neg (log y)) x) (* (log x) x)) (neg (log y)) (log y) y x (* (log x) x) (log x) (log (pow (/ x y) x)) (pow (/ x y) x) (/ x y) (+ (* (log (/ -1 y)) x) (* (log (neg x)) x)) (log (/ -1 y)) (/ -1 y) -1 (* (log (neg x)) x) (log (neg x)) (neg x) (/ (* (- (pow (log x) 2) (pow (log y) 2)) x) (log (* x y))) (* (- (pow (log x) 2) (pow (log y) 2)) x) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) 2 (pow (log y) 2) (log (* x y)) (* x y) (* x (/ (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)))) (/ (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2))) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) 3 (pow (log (/ -1 y)) 3) (+ (* (log (neg x)) (log (* x y))) (pow (log (/ -1 y)) 2)) (pow (log (/ -1 y)) 2)) |
| 1.2s | t | @ | 0 | ((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)))))) (+ (* (* (cos (atan (* (/ (cos t) ew) (/ eh (sin t))))) ew) (sin t)) (* (* (cos t) eh) (tanh (asinh (* (/ (cos t) ew) (/ eh (sin t))))))) (* (cos (atan (* (/ (cos t) ew) (/ eh (sin t))))) ew) (cos (atan (* (/ (cos t) ew) (/ eh (sin t))))) (atan (* (/ (cos t) ew) (/ eh (sin t)))) (* (/ (cos t) ew) (/ eh (sin t))) (/ (cos t) ew) (cos t) t ew (/ eh (sin t)) eh (sin t) (* (* (cos t) eh) (tanh (asinh (* (/ (cos t) ew) (/ eh (sin t)))))) (* (cos t) eh) (tanh (asinh (* (/ (cos t) ew) (/ eh (sin t))))) (asinh (* (/ (cos t) ew) (/ eh (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) (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)))))) (* (* (cos (atan (* (/ (cos t) ew) (/ eh (sin 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)))))) (* (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t))))) (* ew (sin t)) (cos (atan (/ (/ eh ew) (tan t)))) (atan (/ (/ eh ew) (tan t))) (/ (/ eh ew) (tan t)) (/ eh ew) (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))) (/ (/ eh ew) (tan t)) (tan t) (fabs (+ (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t))))))) (+ (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))))) (* (* eh (cos t)) (sin (atan (/ (/ eh ew) (tan t)))))) (* (* ew (sin t)) (/ 1 (sqrt (+ 1 (pow (/ (/ eh ew) (tan t)) 2))))) (/ 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) |
| 1.1s | phi1 | @ | inf | ((+ lambda1 (atan2 (* (cos phi2) (sin (- lambda1 lambda2))) (+ (cos phi1) (* (cos phi2) (cos (- lambda1 lambda2)))))) lambda1 (atan2 (* (cos phi2) (sin (- lambda1 lambda2))) (+ (cos phi1) (* (cos phi2) (cos (- lambda1 lambda2))))) (* (cos phi2) (sin (- lambda1 lambda2))) (cos phi2) phi2 (sin (- lambda1 lambda2)) (- lambda1 lambda2) lambda2 (+ (cos phi1) (* (cos phi2) (cos (- lambda1 lambda2)))) (cos phi1) phi1 (* (cos phi2) (cos (- lambda1 lambda2))) (cos (- lambda1 lambda2))) |
| 837.0ms | dY.v | @ | 0 | ((if (>= (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (* (/ dX.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (floor w)) (/ (* (floor w) dY.u) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2)))))) (>= (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (pow (* (floor h) dX.v) 2) (* (floor h) dX.v) (floor h) h dX.v 2 (pow (* (floor w) dX.u) 2) (* (floor w) dX.u) (floor w) w dX.u (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2)) (pow (* (floor h) dY.v) 2) (* (floor h) dY.v) dY.v (pow (* (floor w) dY.u) 2) (* (floor w) dY.u) dY.u (* (/ dX.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (floor w)) (/ dX.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2)))) (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))) (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2)) (/ (* (floor w) dY.u) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))))) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2)))) (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (if (>= (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (/ (* (floor w) dX.u) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))))) (* dY.u (/ (floor w) (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))))) (>= (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (/ (* (floor w) dX.u) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))))) (* dY.u (/ (floor w) (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2)))))) (/ (floor w) (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (if (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (* (pow (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))) -1/2) (* (floor w) dX.u)) (* (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dY.u))) (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))) (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)) (* (pow (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))) -1/2) (* (floor w) dX.u)) (pow (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))) -1/2) -1/2 (* (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dY.u)) (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))) (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v)) (if (>= (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))) (/ (* (floor w) dX.u) (sqrt (fmax (+ (pow (* (floor h) dX.v) 2) (pow (* (floor w) dX.u) 2)) (+ (pow (* (floor h) dY.v) 2) (pow (* (floor w) dY.u) 2))))) (* (/ dY.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (floor w))) (* (/ dY.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (floor w)) (/ dY.u (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (if (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (* (/ 1 (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (* (floor w) dX.u)) (* (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dY.u))) (>= (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (* (/ 1 (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (* (floor w) dX.u)) (/ 1 (sqrt (fmax (+ (pow (* (floor w) dX.u) 2) (pow (* (floor h) dX.v) 2)) (+ (pow (* (floor w) dY.u) 2) (pow (* (floor h) dY.v) 2))))) (* (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (* (floor w) dY.u)) (/ 1 (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))))) (sqrt (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))))) (fmax (+ (* (* (floor w) dX.u) (* (floor w) dX.u)) (* (* (floor h) dX.v) (* (floor h) dX.v))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v)))) (+ (* (* (floor w) dY.u) (* (floor w) dY.u)) (* (* (floor h) dY.v) (* (floor h) dY.v))) (exp (+ (* (log (floor h)) 2) (* (log dY.v) 2))) (+ (* (log (floor h)) 2) (* (log dY.v) 2)) (log (floor h)) (* (log dY.v) 2) (log dY.v)) |
| 716.0ms | re | @ | -inf | ((/ (atan2 im re) (log 10)) (atan2 im re) im re (log 10) 10) |
| 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.5% | 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 997 computations (71.7% saved)
| 1 096× | iter limit |
| 806× | node limit |
| 294× | saturated |
Compiled 809 747 to 154 405 computations (80.9% saved)
| 351× | fuel |
| 196× | done |
Compiled 332 331 to 44 635 computations (86.6% saved)
| 2 967× | binary-search |
| 1 779× | left-value |
| 2 848× | narrow-enough |
| 117× | predicate-same |
| 2× | predicate-failed |
| 25.6s | 209 056× | 0 | valid |
| 8.9s | 17 613× | 1 | valid |
| 8.7s | 2 215× | 5 | exit |
| 1.5s | 2 835× | 2 | valid |
| 1.2s | 10 513× | 0 | invalid |
| 506.0ms | 434× | 3 | valid |
| 372.0ms | 46× | 4 | valid |
| 20.0ms | 196× | 0 | exit |
| 18.0ms | 73× | 1 | invalid |
Compiled 1 685 247 to 1 132 120 computations (32.8% saved)
ival-mult: 7.9s (21.5% of total)ival-pow: 7.8s (21.3% of total)ival-sub: 3.2s (8.7% of total)ival-sin: 2.6s (7.1% of total)ival-div: 2.6s (7.1% of total)ival-add: 2.4s (6.6% of total)adjust: 2.4s (6.5% of total)ival-cos: 2.0s (5.6% of total)ival-exp: 898.0ms (2.5% of total)const: 765.0ms (2.1% of total)ival-pow2: 705.0ms (1.9% of total)ival-log: 682.0ms (1.9% of total)ival-sqrt: 402.0ms (1.1% of total)ival-cosu: 293.0ms (0.8% of total)ival-sinu: 270.0ms (0.7% of total)ival-neg: 253.0ms (0.7% of total)ival-hypot: 228.0ms (0.6% of total)ival-true: 178.0ms (0.5% of total)ival-atan2: 171.0ms (0.5% of total)ival-tan: 171.0ms (0.5% of total)exact: 128.0ms (0.3% of total)ival-acos: 119.0ms (0.3% of total)ival-assert: 98.0ms (0.3% of total)ival-atan: 67.0ms (0.2% of total)ival-sinh: 56.0ms (0.2% of total)ival-fabs: 44.0ms (0.1% of total)ival-fmax: 33.0ms (0.1% of total)ival-fmod: 24.0ms (0.1% of total)ival-pi: 21.0ms (0.1% of total)ival-asin: 17.0ms (0% of total)ival-e: 15.0ms (0% of total)ival-if: 11.0ms (0% of total)ival-tanu: 10.0ms (0% of total)ival-tanh: 10.0ms (0% of total)ival-expm1: 10.0ms (0% of total)ival-log1p: 8.0ms (0% of total)ival->=: 6.0ms (0% of total)ival-fmin: 5.0ms (0% of total)ival-cosh: 5.0ms (0% of total)ival-cbrt: 3.0ms (0% of total)| 444× | node limit |
| 103× | saturated |
Loading profile data...