
| Date: | Wednesday, April 9th, 2025 |
|---|---|
| Commit: | 5cea69ef on main |
| Seed: | 2025099 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs default |
| Memory: | 84 495.7 MB |
Time bar (total: 1.2min)
| 10.9s | 15 590× | 5 | exit |
| 7.3s | 39 607× | 1 | valid |
| 6.3s | 16 821× | 2 | valid |
| 6.1s | 108 692× | 0 | valid |
| 542.0ms | 4 023× | 0 | invalid |
| 233.0ms | 1 190× | 1 | exit |
| 103.0ms | 1 387× | 0 | exit |
| 1.0ms | 1× | 4 | exit |
ival-exp: 3.6s (14.2% of total)adjust: 3.2s (12.6% of total)ival-pow: 2.9s (11.6% of total)ival-cos: 2.4s (9.4% of total)ival-sqrt: 1.8s (7.2% of total)ival-log: 1.7s (6.8% of total)ival-tan: 1.7s (6.7% of total)ival-sinh: 1.7s (6.6% of total)ival-mult!: 1.6s (6.3% of total)ival-fmod: 991.0ms (3.9% of total)ival-sin: 778.0ms (3.1% of total)ival-div!: 735.0ms (2.9% of total)ival-acos: 536.0ms (2.1% of total)ival-sub!: 385.0ms (1.5% of total)ival-pow2: 376.0ms (1.5% of total)ival-add!: 364.0ms (1.4% of total)ival-neg: 193.0ms (0.8% of total)ival-hypot: 162.0ms (0.6% of total)ival-<=: 107.0ms (0.4% of total)ival-atan: 54.0ms (0.2% of total)ival-and: 38.0ms (0.2% of total)ival-or: 17.0ms (0.1% of total)ival-assert: 4.0ms (0% of total)ival->: 2.0ms (0% of total)ival-<: 2.0ms (0% of total)| 195× | iter-limit |
| 55× | node-limit |
| 15× | unsound |
| 4× | saturated |
53 calls:
| 788.0ms | x |
| 578.0ms | a |
| 306.0ms | b |
| 270.0ms | r |
| 253.0ms | (tan.f64 a) |
Compiled 1 855 to 2 145 computations (-15.6% saved)
399 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 449.0ms | a | @ | -inf | ((* r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a))))) r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (sin b) b (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (cos b) (cos a) a (* (sin b) (sin a)) (sin a) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (tan b) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (cos (+ a b)) (+ a b) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (cos (+ a b)) (+ a b) (* (+ (/ b a) 1) a) (+ (/ b a) 1) (/ b a) 1 (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (cos (+ a b)) (+ (* (neg b) (sin a)) (cos a)) (neg b)) |
| 365.0ms | x | @ | inf | ((- (sin x) x) (* (- (/ (sin x) x) 1) x) (- (/ (sin x) x) 1) (* (- (* (* (+ (* (- (* 1/362880 (* x x)) 1/5040) (* x x)) 1/120) x) x) 1/6) (* x x)) (- (* (* (+ (* (- (* 1/362880 (* x x)) 1/5040) (* x x)) 1/120) x) x) 1/6) (* (* (+ (* (- (* 1/362880 (* x x)) 1/5040) (* x x)) 1/120) x) x) (* (+ (* (- (* 1/362880 (* x x)) 1/5040) (* x x)) 1/120) x) (+ (* (- (* 1/362880 (* x x)) 1/5040) (* x x)) 1/120) (- (* 1/362880 (* x x)) 1/5040) (* 1/362880 (* x x)) 1/362880 (* x x) x 1/5040 1/120 1/6 (- (sin x) x) (* (* x x) (* x -1/6)) (* x -1/6) -1/6 (- (sin x) x) (* (* (* x x) x) -1/6) (* (* x x) x) (/ (- (pow (sin x) 2) (* x x)) (+ (sin x) x)) (- (pow (sin x) 2) (* x x)) (* (pow x 4) -1/3) (pow x 4) 4 -1/3 (+ (sin x) x) (sin x) (/ (- (* (pow (sin x) 2) (+ (sin x) x)) (* (+ (sin x) x) (* x x))) (* (+ (sin x) x) (+ (sin x) x))) (- (* (pow (sin x) 2) (+ (sin x) x)) (* (+ (sin x) x) (* x x))) (* (pow (sin x) 2) (+ (sin x) x)) (pow (sin x) 2) 2 (* (+ (sin x) x) (* x x)) (* (+ (sin x) x) (+ (sin x) x))) |
| 110.0ms | w | @ | 0 | ((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) (/ 1 (pow l (neg (exp w)))) 1 (pow l (neg (exp w))) l (neg (exp w)) (exp w) (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (pow (pow l (neg (exp w))) -1) (* (exp (neg w)) (pow l (exp w))) (+ (* (+ (* (log l) l) (neg l)) w) l) (+ (* (- (* (log l) l) l) w) l) (- (* (log l) l) l) (* (log l) l) (log l) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) (pow l (exp w)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ (* (+ (* (+ (* -1/6 w) 1/2) w) -1) w) 1) (+ (* (+ (* -1/6 w) 1/2) w) -1) (+ (* -1/6 w) 1/2) (* -1/6 w) -1/6 -1) |
| 85.0ms | x | @ | 0 | ((* (sqrt 2) x) (sqrt 2) 2 x (* (sqrt (* x 2)) (sqrt x)) (sqrt (* x 2)) (* x 2) (sqrt x) (* (pow (* (* x x) 2) 1/4) (pow (* (* x x) 2) 1/4)) (pow (* (* x x) 2) 1/4) (* (* x x) 2) (* x x) 1/4 (sqrt (+ (* x x) (* x x)))) |
| 61.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) x)) (log (* (/ -1 x) (* -1/2 (* 2 (sinh x))))) (* (/ -1 x) (* -1/2 (* 2 (sinh x)))) (/ -1 x) -1 (* -1/2 (* 2 (sinh x))) -1/2 (* 2 (sinh x)) 2 (sinh x)) |
Compiled 717 810 to 90 713 computations (87.4% saved)
| 14× | fuel |
| 6× | done |
Compiled 4 037 to 935 computations (76.8% 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)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
cos.f64 | #f | sensitivity | 521 | 2 |
sqrt.f64 | #f | oflow-rescue | 514 | 0 |
-.f64 | #f | cancellation | 335 | 0 |
sqrt.f64 | #f | uflow-rescue | 310 | 0 |
/.f64 | #f | n/o | 258 | 0 |
acos.f64 | (acos.f64 (-.f64 #s(literal 1 binary64) x)) | sensitivity | 256 | 0 |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | sensitivity | 251 | 1 |
tan.f64 | (tan.f64 (+.f64 y z)) | sensitivity | 196 | 0 |
pow.f64 | (pow.f64 l (exp.f64 w)) | sensitivity | 132 | 20 |
*.f64 | #f | n*o | 39 | 0 |
*.f64 | #f | n*u | 30 | 0 |
*.f64 | (*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)) | u*o | 12 | 0 |
| ↳ | (pow.f64 c #s(literal 2 binary64)) | underflow | 57 | |
| ↳ | (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x) | overflow | 71 | |
| ↳ | (*.f64 x (pow.f64 s #s(literal 2 binary64))) | overflow | 60 | |
| ↳ | (pow.f64 s #s(literal 2 binary64)) | overflow | 66 | |
*.f64 | (*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)) | o*u | 12 | 0 |
| ↳ | (pow.f64 c #s(literal 2 binary64)) | overflow | 59 | |
| ↳ | (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x) | underflow | 76 | |
| ↳ | (*.f64 x (pow.f64 s #s(literal 2 binary64))) | underflow | 65 | |
| ↳ | (pow.f64 s #s(literal 2 binary64)) | underflow | 60 | |
-.f64 | (-.f64 (*.f64 a a) (*.f64 b b)) | nan-rescue | 9 | 0 |
| ↳ | (*.f64 a a) | overflow | 109 | |
| ↳ | (*.f64 b b) | overflow | 9 | |
exp.f64 | (exp.f64 (neg.f64 x)) | sensitivity | 1 | 0 |
log.f64 | (log.f64 (/.f64 (sinh.f64 x) x)) | oflow-rescue | 1 | 0 |
| ↳ | (sinh.f64 x) | overflow | 1 | |
| ↳ | (/.f64 (sinh.f64 x) x) | overflow | 1 | |
+.f64 | (+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a))) | cancellation | 1 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 2079 | 269 |
| - | 743 | 2029 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 2079 | 2 | 267 |
| - | 743 | 22 | 2007 |
| number | freq |
|---|---|
| 0 | 2298 |
| 1 | 2768 |
| 2 | 52 |
| 3 | 2 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 18 | 0 | 0 |
| - | 0 | 0 | 2 |
| 691.0ms | 1 036× | 2 | valid |
| 447.0ms | 6 568× | 0 | valid |
| 427.0ms | 2 544× | 1 | valid |
| 12.0ms | 92× | 1 | exit |
Compiled 1 067 to 440 computations (58.8% saved)
ival-log: 446.0ms (38.9% of total)ival-sqrt: 81.0ms (7.1% of total)adjust: 80.0ms (7% of total)ival-tan: 78.0ms (6.8% of total)ival-cos: 73.0ms (6.4% of total)ival-mult!: 51.0ms (4.4% of total)ival-pow2: 46.0ms (4% of total)ival-sin: 44.0ms (3.8% of total)ival-exp: 41.0ms (3.6% of total)ival-sinh: 35.0ms (3.1% of total)ival-fmod: 35.0ms (3.1% of total)ival-acos: 34.0ms (3% of total)ival-sub!: 29.0ms (2.5% of total)ival-div!: 27.0ms (2.4% of total)ival-add!: 22.0ms (1.9% of total)ival-hypot: 9.0ms (0.8% of total)ival-pow: 8.0ms (0.7% of total)ival-neg: 5.0ms (0.4% of total)ival-atan: 3.0ms (0.3% of total)| 15× | node-limit |
| 5× | saturated |
Compiled 19 388 to 8 948 computations (53.8% saved)
Compiled 81 115 to 42 997 computations (47% saved)
| 43× | binary-search |
| 16× | left-value |
| 24× | narrow-enough |
| 12× | predicate-same |
| 7× | predicate-failed |
| 264.0ms | 1 080× | 1 | valid |
| 197.0ms | 1 656× | 0 | valid |
| 73.0ms | 707× | 0 | invalid |
| 1.0ms | 12× | 0 | exit |
Compiled 10 344 to 8 468 computations (18.1% saved)
ival-tan: 122.0ms (29.4% of total)ival-cos: 81.0ms (19.5% of total)ival-mult!: 39.0ms (9.4% of total)ival-pow2: 38.0ms (9.1% of total)ival-exp: 33.0ms (7.9% of total)adjust: 27.0ms (6.5% of total)ival-fmod: 20.0ms (4.8% of total)ival-sin: 14.0ms (3.4% of total)ival-add!: 11.0ms (2.6% of total)ival-sqrt: 9.0ms (2.2% of total)ival-pow: 7.0ms (1.7% of total)ival-neg: 6.0ms (1.4% of total)ival-div!: 5.0ms (1.2% of total)ival-sub!: 4.0ms (1% of total)Loading profile data...