
| 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: | 81 161.4 MB |
Time bar (total: 1.3min)
| 11.8s | 16 377× | 5 | exit |
| 6.8s | 39 448× | 1 | valid |
| 6.6s | 108 825× | 0 | valid |
| 5.3s | 16 847× | 2 | valid |
| 428.0ms | 3 867× | 0 | invalid |
| 136.0ms | 1 376× | 0 | exit |
ival-pow: 4.5s (18% of total)ival-exp: 4.4s (17.9% of total)adjust: 2.8s (11.3% of total)ival-cos: 2.0s (8.1% of total)ival-log: 1.6s (6.5% of total)ival-mult!: 1.5s (6.1% of total)ival-tan: 1.4s (5.6% of total)ival-sqrt: 1.4s (5.5% of total)ival-sinh: 792.0ms (3.2% of total)ival-fmod: 767.0ms (3.1% of total)ival-div!: 685.0ms (2.8% of total)ival-sin: 676.0ms (2.7% of total)ival-acos: 484.0ms (2% of total)ival-pow2: 466.0ms (1.9% of total)ival-sub!: 346.0ms (1.4% of total)ival-add!: 330.0ms (1.3% of total)ival-neg: 241.0ms (1% of total)ival-hypot: 183.0ms (0.7% of total)ival-<=: 74.0ms (0.3% of total)ival-atan: 49.0ms (0.2% of total)ival-and: 35.0ms (0.1% of total)ival-or: 16.0ms (0.1% of total)ival-assert: 3.0ms (0% of total)ival-<: 2.0ms (0% of total)ival->: 1.0ms (0% of total)| 190× | iter limit |
| 50× | node limit |
| 17× | unsound |
| 4× | saturated |
53 calls:
| 798.0ms | b |
| 786.0ms | x |
| 620.0ms | a |
| 397.0ms | r |
| 262.0ms | (+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a))) |
Compiled 1 724 to 2 035 computations (-18% saved)
| 38× | iter limit |
| 29× | node limit |
| 13× | saturated |
Compiled 10 539 to 3 412 computations (67.6% saved)
Compiled 633 615 to 78 705 computations (87.6% saved)
| 12× | fuel |
| 8× | done |
Compiled 4 193 to 1 030 computations (75.4% saved)
390 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 318.0ms | r | @ | 0 | ((/ (* r (sin b)) (+ (* (sin a) (neg (sin b))) (* (cos a) (cos b)))) (* r (sin b)) r (sin b) b (+ (* (sin a) (neg (sin b))) (* (cos a) (cos b))) (sin a) a (neg (sin b)) (* (cos a) (cos b)) (cos a) (cos b) (/ (* r (sin b)) (cos (+ a b))) (* r (tan b)) (* (+ (* 1/3 (* (* b b) r)) r) b) (+ (* 1/3 (* (* b b) r)) r) 1/3 (* (* b b) r) (* b b) (/ (* r (sin b)) (sin (+ (neg (+ a b)) (/ (PI) 2)))) (sin (+ (neg (+ a b)) (/ (PI) 2))) (+ (neg (+ a b)) (/ (PI) 2)) (neg (+ a b)) (+ a b) (/ (PI) 2) (PI) 2 (/ (* r (sin b)) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (* (sin b) (sin a)) (/ (* r (sin b)) (cos (+ a b))) (cos (+ a b)) (+ a b) (* (/ (+ (pow (/ b a) 3) 1) (+ (pow (/ b a) 2) (- 1 (/ b a)))) a) (/ (+ (pow (/ b a) 3) 1) (+ (pow (/ b a) 2) (- 1 (/ b a)))) (+ (pow (/ b a) 3) 1) (pow (/ b a) 3) (/ b a) 3 1 (+ (pow (/ b a) 2) (- 1 (/ b a))) (pow (/ b a) 2) (- 1 (/ b a))) |
| 109.0ms | x | @ | inf | ((log (/ (sinh x) x)) (/ (sinh x) x) (sinh x) x) |
| 79.0ms | x | @ | 0 | ((* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) x (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (* (- (pow x -2) 1/4) x) x) (* (- (pow x -2) 1/4) x) (- (pow x -2) 1/4) (pow x -2) -2 1/4 (exp (neg x)) (neg x) (* (fmod (exp x) (sqrt (cos x))) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x))) (fmod (exp x) (sqrt (cos x))) (exp x) 1 (sqrt (cos x)) (cos x) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x)) (+ (* (- (* 1/2 x) 1) x) 1) (- (* 1/2 x) 1) (* 1/2 x) 1/2 (* (fmod (exp x) (sqrt (cos x))) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* x x) -1/4 (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (- (* (/ -1 x) (/ -1 x)) 1/4) (* x x)) (- (* (/ -1 x) (/ -1 x)) 1/4) (* (/ -1 x) (/ -1 x)) (/ -1 x) -1 (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (- (pow x -2) 1/4) (exp (* (log x) 2))) (exp (* (log x) 2)) (* (log x) 2) (log x) 2) |
| 74.0ms | x | @ | inf | ((- (log (sinh x)) (log x)) (* (* (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) x) (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* (+ (* -1/37800 (* x x)) 1/2835) x) (+ (* -1/37800 (* x x)) 1/2835) 1/2835 x -1/180 (* x x) 1/6 (- (log (sinh x)) (log x)) (* (* (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) x) (+ (* (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (* x x)) 1/6) (+ (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) -1/180) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (* 1/6 x) x) 1) (* 1/6 x) 1 (log (/ (sinh x) x)) (* (/ (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)) x) (/ (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)) (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36) (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) (* (* (+ (* (* x x) 1/2835) -1/180) x) x) (* (+ (* (* x x) 1/2835) -1/180) x) (+ (* (* x x) 1/2835) -1/180) 2 1/36 (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6) -1/6 (log (/ (sinh x) x)) (/ (* (* x x) (+ 1/216 (* (pow (+ (* (* x x) 1/2835) -1/180) 3) (pow x 6)))) (+ 1/36 (* (* (* (+ (* (* x x) 1/2835) -1/180) x) x) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)))) (* (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (pow x 6)) (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (+ (/ 1/6 (pow x 4)) 1/2835) (/ 1/6 (pow x 4)) (pow x 4) 4 (* (pow x -2) 1/180) (pow x -2) -2 1/180 (pow x 6) 6) |
| 66.0ms | x | @ | -inf | ((log (/ (sinh x) x)) (* (* (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) x) x) (* (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) x) (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) (- (* 1/2835 (* x x)) 1/180) (* 1/2835 (* x x)) 1/2835 (* x x) x 1/180 1/6 (log (/ (sinh x) x)) (* (* x x) 1/6) (log (/ (sinh x) x)) (* (+ (* (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* x x)) 1/6) (* x x)) (+ (* (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* x x)) 1/6) (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) (* (+ (* -1/37800 (* x x)) 1/2835) x) (+ (* -1/37800 (* x x)) 1/2835) -1/37800 (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) 1/120 1 (- (log (sinh x)) (log x)) (log (sinh x)) (sinh x) (log x)) |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
sqrt.f64 | #f | oflow-rescue | 583 | 0 |
cos.f64 | #f | sensitivity | 516 | 2 |
-.f64 | #f | cancellation | 344 | 0 |
sqrt.f64 | #f | uflow-rescue | 327 | 0 |
/.f64 | #f | n/o | 260 | 0 |
acos.f64 | (acos.f64 (-.f64 #s(literal 1 binary64) x)) | sensitivity | 251 | 0 |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | sensitivity | 245 | 1 |
tan.f64 | (tan.f64 (+.f64 y z)) | sensitivity | 195 | 0 |
pow.f64 | (pow.f64 l (exp.f64 w)) | sensitivity | 121 | 16 |
*.f64 | #f | n*o | 35 | 0 |
*.f64 | #f | n*u | 35 | 0 |
*.f64 | (*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)) | u*o | 18 | 0 |
| ↳ | (pow.f64 c #s(literal 2 binary64)) | underflow | 75 | |
| ↳ | (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x) | overflow | 65 | |
| ↳ | (*.f64 x (pow.f64 s #s(literal 2 binary64))) | overflow | 60 | |
| ↳ | (pow.f64 s #s(literal 2 binary64)) | overflow | 67 | |
*.f64 | (*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)) | o*u | 17 | 0 |
| ↳ | (pow.f64 c #s(literal 2 binary64)) | overflow | 56 | |
| ↳ | (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x) | underflow | 81 | |
| ↳ | (*.f64 x (pow.f64 s #s(literal 2 binary64))) | underflow | 72 | |
| ↳ | (pow.f64 s #s(literal 2 binary64)) | underflow | 70 | |
-.f64 | (-.f64 (*.f64 a a) (*.f64 b b)) | nan-rescue | 9 | 0 |
| ↳ | (*.f64 a a) | overflow | 110 | |
| ↳ | (*.f64 b b) | overflow | 9 | |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | oflow-rescue | 5 | 0 |
| ↳ | (sinh.f64 x) | overflow | 5 | |
| ↳ | (/.f64 (sinh.f64 x) x) | overflow | 5 | |
tan.f64 | (tan.f64 (+.f64 y z)) | cancellation | 1 | 0 |
+.f64 | (+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a))) | cancellation | 1 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 2214 | 271 |
| - | 682 | 1953 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 2214 | 3 | 268 |
| - | 682 | 16 | 1937 |
| number | freq |
|---|---|
| 0 | 2224 |
| 1 | 2830 |
| 2 | 65 |
| 3 | 1 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 17 | 0 | 1 |
| - | 0 | 0 | 2 |
| 612.0ms | 2 496× | 1 | valid |
| 378.0ms | 6 594× | 0 | valid |
| 324.0ms | 1 046× | 2 | valid |
| 14.0ms | 104× | 1 | exit |
Compiled 1 067 to 440 computations (58.8% saved)
ival-sqrt: 128.0ms (14.1% of total)ival-tan: 115.0ms (12.7% of total)ival-cos: 105.0ms (11.6% of total)adjust: 84.0ms (9.3% of total)ival-mult!: 73.0ms (8.1% of total)ival-log: 66.0ms (7.3% of total)ival-sinh: 57.0ms (6.3% of total)ival-exp: 40.0ms (4.4% of total)ival-sub!: 40.0ms (4.4% of total)ival-sin: 40.0ms (4.4% of total)ival-pow2: 35.0ms (3.9% of total)ival-fmod: 29.0ms (3.2% of total)ival-acos: 29.0ms (3.2% of total)ival-div!: 23.0ms (2.5% of total)ival-add!: 18.0ms (2% of total)ival-hypot: 9.0ms (1% of total)ival-pow: 8.0ms (0.9% of total)ival-neg: 5.0ms (0.6% of total)ival-atan: 3.0ms (0.3% of total)Compiled 86 998 to 45 219 computations (48% saved)
| 20× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 73.7% | 26.3% | 0% | 0% | 0% | 0 |
| 28.8% | 21.3% | 52.5% | 26.3% | 0% | 0% | 0% | 1 |
| 44.1% | 32.5% | 41.2% | 26.3% | 0% | 0% | 0% | 2 |
| 52.6% | 38.7% | 35% | 26.3% | 0% | 0% | 0% | 3 |
| 61.9% | 45.6% | 28.1% | 26.3% | 0% | 0% | 0% | 4 |
| 65.2% | 47.5% | 25.3% | 26.3% | 0% | 0.9% | 0% | 5 |
| 66.8% | 48.4% | 24% | 26.3% | 0% | 1.2% | 0% | 6 |
| 71.1% | 51.1% | 20.8% | 26.3% | 0% | 1.9% | 0% | 7 |
| 72.1% | 51.6% | 20% | 26.3% | 0% | 2.1% | 0% | 8 |
| 74.4% | 53% | 18.2% | 26.3% | 0% | 2.5% | 0% | 9 |
| 75.8% | 53.9% | 17.2% | 26.3% | 0% | 2.6% | 0% | 10 |
| 76.6% | 54.3% | 16.6% | 26.3% | 0% | 2.8% | 0% | 11 |
| 77.3% | 54.8% | 16.1% | 26.3% | 0% | 2.9% | 0% | 12 |
Compiled 279 to 216 computations (22.6% saved)
| 51× | binary-search |
| 18× | left-value |
| 31× | narrow-enough |
| 11× | predicate-same |
| 9× | predicate-failed |
| 338.0ms | 1 516× | 1 | valid |
| 127.0ms | 1 316× | 0 | valid |
| 106.0ms | 909× | 0 | invalid |
| 93.0ms | 160× | 2 | valid |
Compiled 13 315 to 10 511 computations (21.1% saved)
ival-cos: 131.0ms (24.2% of total)ival-exp: 112.0ms (20.7% of total)ival-tan: 70.0ms (12.9% of total)ival-fmod: 50.0ms (9.2% of total)ival-sin: 38.0ms (7% of total)adjust: 36.0ms (6.7% of total)ival-mult!: 28.0ms (5.2% of total)ival-div!: 26.0ms (4.8% of total)ival-sqrt: 16.0ms (3% of total)ival-pow2: 10.0ms (1.8% of total)ival-add!: 9.0ms (1.7% of total)ival-neg: 6.0ms (1.1% of total)ival-acos: 4.0ms (0.7% of total)ival-sub!: 3.0ms (0.6% of total)ival-pow: 1.0ms (0.2% of total)| 15× | node limit |
| 5× | saturated |
Loading profile data...