
| Date: | Sunday, January 19th, 2025 |
|---|---|
| Commit: | 455c599f on main |
| Seed: | 2025019 |
| Parameters: | 256 points for 4 iterations |
| Flags: | localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs default |
| Memory: | 377 787.8 MB |
Time bar (total: 5.5min)
| 54.3s | 433 995× | 0 | valid |
| 11.1s | 26 728× | 1 | valid |
| 4.6s | 9 023× | 2 | valid |
| 2.6s | 4 228× | 0 | invalid |
| 1.0s | 7 954× | 0 | exit |
| 312.0ms | 849× | 3 | valid |
ival-mult: 15.3s (28.8% of total)ival-add: 6.2s (11.7% of total)const: 5.4s (10.1% of total)ival-div: 4.7s (8.8% of total)ival-exp: 3.2s (6.1% of total)adjust: 2.6s (4.9% of total)ival-sub: 2.2s (4.1% of total)ival-hypot: 2.1s (3.9% of total)ival-log: 2.1s (3.9% of total)ival-asin: 1.2s (2.2% of total)ival-cos: 1.1s (2.1% of total)ival-sin: 1.0s (1.9% of total)ival-sqrt: 1.0s (1.9% of total)ival-atan2: 876.0ms (1.6% of total)ival->: 474.0ms (0.9% of total)ival-asinh: 430.0ms (0.8% of total)ival-pi: 386.0ms (0.7% of total)exact: 369.0ms (0.7% of total)ival-acosh: 303.0ms (0.6% of total)ival-pow: 295.0ms (0.6% of total)ival-sinu: 286.0ms (0.5% of total)ival-true: 280.0ms (0.5% of total)ival-atanh: 259.0ms (0.5% of total)ival-fabs: 231.0ms (0.4% of total)ival-<=: 200.0ms (0.4% of total)ival-assert: 196.0ms (0.4% of total)ival-neg: 185.0ms (0.3% of total)ival->=: 154.0ms (0.3% of total)ival-cosu: 124.0ms (0.2% of total)ival-and: 83.0ms (0.2% of total)| 579× | iter limit |
| 374× | node limit |
| 63× | saturated |
| 13.2s | 39 321× | 0 | valid |
| 6.7s | 4 896× | 1 | valid |
| 3.4s | 1 762× | 2 | valid |
| 877.0ms | 1 856× | 0 | invalid |
| 680.0ms | 655× | 0 | exit |
| 213.0ms | 46× | 5 | exit |
| 98.0ms | 101× | 3 | valid |
| 3.0ms | 3× | 4 | valid |
Compiled 70 361 to 6 108 computations (91.3% saved)
ival-mult: 5.2s (27.2% of total)ival-add: 2.4s (12.6% of total)adjust: 2.1s (10.9% of total)ival-div: 2.0s (10.2% of total)const: 1.6s (8.4% of total)ival-sub: 756.0ms (3.9% of total)ival-exp: 706.0ms (3.7% of total)ival-log: 660.0ms (3.4% of total)ival-pow: 641.0ms (3.3% of total)ival-cos: 602.0ms (3.1% of total)ival-hypot: 454.0ms (2.4% of total)ival-sqrt: 385.0ms (2% of total)ival-sin: 266.0ms (1.4% of total)ival-acos: 251.0ms (1.3% of total)ival-asin: 239.0ms (1.2% of total)ival-neg: 218.0ms (1.1% of total)ival-log1p: 131.0ms (0.7% of total)ival-pow2: 110.0ms (0.6% of total)ival-atan2: 109.0ms (0.6% of total)exact: 77.0ms (0.4% of total)ival-cosh: 45.0ms (0.2% of total)ival-sinh: 40.0ms (0.2% of total)ival-fabs: 40.0ms (0.2% of total)ival-true: 39.0ms (0.2% of total)ival-pi: 34.0ms (0.2% of total)ival-copysign: 27.0ms (0.1% of total)ival-assert: 21.0ms (0.1% of total)ival-asinh: 17.0ms (0.1% of total)ival-sinu: 14.0ms (0.1% of total)ival-cosu: 11.0ms (0.1% of total)ival-acosh: 6.0ms (0% of total)ival-cbrt: 4.0ms (0% of total)| 582× | iter limit |
| 141× | node limit |
| 46× | unsound |
| 3× | saturated |
| 36× | fuel |
| 21× | done |
Compiled 39 621 to 4 572 computations (88.5% saved)
Compiled 4 927 854 to 320 194 computations (93.5% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
sqrt.f64 | #f | oflow-rescue | 1255 | 0 |
-.f64 | #f | cancellation | 740 | 3 |
/.f64 | #f | o/o | 636 | 0 |
sin.f64 | #f | sensitivity | 197 | 1 |
cos.f64 | (cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | sensitivity | 194 | 0 |
/.f64 | #f | o/n | 184 | 0 |
sqrt.f32 | #f | oflow-rescue | 183 | 0 |
sqrt.f64 | #f | uflow-rescue | 142 | 0 |
+.f64 | #f | cancellation | 138 | 0 |
log.f32 | (log.f32 (+.f32 (fabs.f32 x) (sqrt.f32 (+.f32 (*.f32 x x) #s(literal 1 binary32))))) | sensitivity | 123 | 2 |
log.f64 | (log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) #s(literal 1 binary64))))) | sensitivity | 123 | 1 |
/.f64 | #f | n/o | 103 | 0 |
-.f64 | #f | nan-rescue | 94 | 0 |
*.f64 | #f | n*u | 70 | 0 |
/.f64 | #f | u/u | 54 | 0 |
+.f64 | #f | nan-rescue | 44 | 0 |
/.f64 | #f | u/n | 31 | 0 |
*.f64 | #f | n*o | 25 | 0 |
/.f64 | #f | n/u | 9 | 0 |
log.f32 | #f | oflow-rescue | 5 | 0 |
*.f64 | (*.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))) (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64))))) | o*u | 2 | 0 |
| ↳ | (*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))) | overflow | 3 | |
| ↳ | (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64))) | overflow | 3 | |
| ↳ | (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)))) | underflow | 2 | |
cos.f64 | (cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)) | overflow | 1 | |
| ↳ | (*.f64 x.re x.re) | overflow | 68 | |
| ↳ | (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) | overflow | 102 | |
| ↳ | (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) | overflow | 1 | |
| ↳ | (*.f64 x.im x.im) | overflow | 48 | |
exp.f64 | (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)))) | sensitivity | 1 | 0 |
sin.f64 | (sin.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))) | oflow-rescue | 1 | 0 |
| ↳ | (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)) | overflow | 1 | |
| ↳ | (*.f64 x.re x.re) | overflow | 68 | |
| ↳ | (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)) | overflow | 102 | |
| ↳ | (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) | overflow | 1 | |
| ↳ | (*.f64 x.im x.im) | overflow | 48 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3608 | 30 |
| - | 193 | 10761 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3608 | 7 | 23 |
| - | 193 | 2 | 10759 |
| number | freq |
|---|---|
| 0 | 10791 |
| 1 | 3249 |
| 2 | 550 |
| 3 | 2 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 38 | 0 | 0 |
| - | 0 | 1 | 18 |
| 3.5s | 25 542× | 0 | valid |
| 1.2s | 2 646× | 1 | valid |
| 791.0ms | 920× | 2 | valid |
| 67.0ms | 72× | 3 | valid |
| 2.0ms | 4× | 5 | exit |
Compiled 13 558 to 2 283 computations (83.2% saved)
ival-mult: 1.1s (29.4% of total)ival-add: 477.0ms (12.5% of total)adjust: 356.0ms (9.3% of total)ival-div: 267.0ms (7% of total)ival-hypot: 259.0ms (6.8% of total)const: 235.0ms (6.2% of total)ival-exp: 232.0ms (6.1% of total)ival-log: 218.0ms (5.7% of total)ival-sub: 158.0ms (4.1% of total)ival-atan2: 72.0ms (1.9% of total)ival-sin: 71.0ms (1.9% of total)ival-asin: 64.0ms (1.7% of total)ival-sqrt: 63.0ms (1.6% of total)ival-cos: 55.0ms (1.4% of total)ival-pi: 25.0ms (0.7% of total)ival-true: 25.0ms (0.7% of total)ival-pow: 24.0ms (0.6% of total)exact: 21.0ms (0.5% of total)ival-fabs: 20.0ms (0.5% of total)ival-copysign: 13.0ms (0.3% of total)ival-neg: 13.0ms (0.3% of total)ival-assert: 12.0ms (0.3% of total)ival-log1p: 7.0ms (0.2% of total)ival-sinu: 7.0ms (0.2% of total)ival-cosu: 6.0ms (0.2% of total)| 114× | iter limit |
| 72× | node limit |
| 42× | saturated |
Compiled 88 888 to 14 535 computations (83.6% saved)
132 calls:
| 959.0ms | re |
| 909.0ms | (sin.f64 re) |
| 787.0ms | y.im |
| 651.0ms | im |
| 538.0ms | y.re |
Compiled 14 716 to 10 355 computations (29.6% saved)
1188 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 125.0ms | x | @ | -inf | ((log (* (log x) x)) (* (log x) x) (log x) (log (/ x (log x))) (/ x (log x))) |
| 109.0ms | re | @ | 0 | ((* (atan2 im re) (/ (log base) (pow (log base) 2))) (atan2 im re) (/ (log base) (pow (log base) 2)) (/ 1 (log base)) (* (/ (* (log base) (atan2 im re)) (pow (log base) 4)) (pow (log base) 2)) (/ (* (log base) (atan2 im re)) (pow (log base) 4)) (/ (atan2 im re) (pow (log base) 3)) (* (pow (log base) 3) (/ (atan2 im re) (pow (log base) 4))) (pow (log base) 3) (log base) (/ (atan2 im re) (pow (log base) 4)) (/ (* (log base) (atan2 im re)) (pow (exp 2) (log (log base)))) (* (log base) (atan2 im re)) (* (* (log base) (atan2 im re)) (pow (log base) 4)) (/ (* (* (log base) (atan2 im re)) (pow (log base) 4)) (pow (log base) 6)) (pow (log base) 2) (pow (log base) 4) (pow (exp 2) (log (log base))) (log (log base)) (pow (log base) 6)) |
| 103.0ms | im | @ | -inf | ((/ (* 1/2 (log (+ (* im im) (* re re)))) (neg (log 1/10))) (* 1/2 (log (+ (* im im) (* re re)))) (log (+ (* im im) (* re re))) (+ (* (/ re im) (/ re im)) (* 2 (log im))) (/ (* 1/2 (log (+ (* im im) (* re re)))) (log 10)) (* 1/2 (log (+ (* im im) (* re re)))) (log (+ (* im im) (* re re))) (+ (* (/ re im) (/ re im)) (* 2 (log im))) (/ (* 1/2 (log (+ (* im im) (* re re)))) (log 10)) (* 1/2 (log (+ (* im im) (* re re)))) (log (+ (* im im) (* re re))) (+ (* (/ re im) (/ re im)) (* 2 (log im))) (/ (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (log 10)) (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4)))) (- (log (pow im 6)) (log (pow im 4))) (/ (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (log 10)) (* 1/2 (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))))) (- (log (+ (pow im 6) (pow re 6))) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4)))) (log (+ (pow im 6) (pow re 6))) (log 1/10) (* (/ re im) (/ re im)) (* (+ (* (/ 2 re) (/ (log im) re)) (/ 1 (* im im))) (* re re)) (+ (* (/ 2 re) (/ (log im) re)) (/ 1 (* im im))) (/ 1 (* im im)) (log (pow im 6)) (log (pow im 4)) (log (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4))) (+ (- (pow re 4) (pow (* im re) 2)) (pow im 4)) (- (pow re 4) (pow (* im re) 2))) |
| 96.0ms | y.im | @ | inf | ((* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (/ (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (pow (exp y.im) (atan2 x.im x.re))) (sin (+ (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im) (* (atan2 x.im x.re) y.re)))) (/ (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (pow (exp y.im) (atan2 x.im x.re))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sqrt (+ (* x.im x.im) (* x.re x.re))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (+ (* x.re x.re) (* x.im x.im)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (neg (* (neg (log x.im)) y.im)) (neg (* (neg (log x.im)) y.re)) (exp (- (neg (* (neg (log x.im)) y.re)) (* (atan2 x.im x.re) y.im))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (sin (+ (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im) (* (atan2 x.im x.re) y.re))) (* (atan2 x.im x.re) y.re) (+ (* (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) y.im) (* (atan2 x.im x.re) y.re)) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)) (sin (+ (* (atan2 x.im x.re) y.re) (neg (* (neg (log x.im)) y.im)))) (+ (* (atan2 x.im x.re) y.re) (neg (* (neg (log x.im)) y.im))) (* (neg (log x.im)) y.im) (sin (* (atan2 x.im x.re) y.re)) (cos (* (atan2 x.im x.re) y.re)) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) |
| 95.0ms | base | @ | -inf | ((/ (log base) (pow (log base) 2)) (* (atan2 im re) (/ (log base) (pow (log base) 2))) (atan2 im re) (log base) (/ (* (log base) (atan2 im re)) (log (pow base (log base)))) (* (log base) (atan2 im re)) (/ (* (log base) (atan2 im re)) (exp (* (log (log base)) 2))) (exp (* (log (log base)) 2)) (* (/ (* (log base) (atan2 im re)) (pow (log base) 4)) (pow (log base) 2)) (/ (* (log base) (atan2 im re)) (pow (log base) 4)) (/ (pow (* (log base) (atan2 im re)) 2) (* (* (log base) (atan2 im re)) (pow (log base) 2))) (pow (* (log base) (atan2 im re)) 2) (pow (log base) 2) (log (pow base (log base))) (pow base (log base)) (log (log base)) (pow (log base) 4) (pow (log base) 3) (* (pow (log base) 3) (atan2 im re))) |
Compiled 264 838 to 108 451 computations (59.1% saved)
| 245× | left-value |
| 242× | binary-search |
| 226× | narrow-enough |
| 16× | predicate-same |
| 2.3s | 16 516× | 0 | valid |
| 1.1s | 2 373× | 1 | valid |
| 70.0ms | 171× | 2 | valid |
| 31.0ms | 76× | 3 | valid |
Compiled 193 857 to 97 441 computations (49.7% saved)
ival-mult: 907.0ms (33% of total)ival-hypot: 295.0ms (10.7% of total)ival-log: 256.0ms (9.3% of total)ival-add: 227.0ms (8.3% of total)const: 152.0ms (5.5% of total)ival-sin: 152.0ms (5.5% of total)adjust: 146.0ms (5.3% of total)ival-sub: 145.0ms (5.3% of total)ival-exp: 118.0ms (4.3% of total)ival-cos: 108.0ms (3.9% of total)ival-div: 98.0ms (3.6% of total)ival-atan2: 85.0ms (3.1% of total)ival-sqrt: 22.0ms (0.8% of total)ival-true: 14.0ms (0.5% of total)ival-neg: 8.0ms (0.3% of total)ival-assert: 7.0ms (0.3% of total)exact: 6.0ms (0.2% of total)ival-fabs: 3.0ms (0.1% of total)| 58× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 86.3% | 13.7% | 0% | 0% | 0% | 0 |
| 55.4% | 47.8% | 38.5% | 13.7% | 0% | 0% | 0% | 1 |
| 65.9% | 55.7% | 28.9% | 13.7% | 0% | 1.7% | 0% | 2 |
| 71.2% | 58.4% | 23.6% | 13.7% | 0% | 4.3% | 0% | 3 |
| 77.4% | 62% | 18.1% | 13.7% | 0% | 6.2% | 0% | 4 |
| 83.5% | 66.8% | 13.2% | 13.7% | 0% | 6.3% | 0% | 5 |
| 85.8% | 68.3% | 11.3% | 13.7% | 0% | 6.6% | 0% | 6 |
| 88.3% | 70.3% | 9.4% | 13.7% | 0% | 6.6% | 0% | 7 |
| 89.9% | 71.5% | 8% | 13.7% | 0% | 6.8% | 0% | 8 |
| 91.1% | 72.5% | 7.1% | 13.7% | 0% | 6.8% | 0% | 9 |
| 92.6% | 73.6% | 5.9% | 13.7% | 0% | 6.8% | 0% | 10 |
| 94% | 74.7% | 4.8% | 13.7% | 0% | 6.8% | 0% | 11 |
| 94.5% | 75.1% | 4.4% | 13.7% | 0% | 6.9% | 0% | 12 |
Compiled 1 498 to 816 computations (45.5% saved)
Loading profile data...