
| 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: | 171 161.9 MB |
Time bar (total: 2.6min)
| 26.2s | 284 610× | 0 | valid |
| 13.7s | 44 198× | 1 | valid |
| 8.0s | 17 555× | 2 | valid |
| 926.0ms | 389× | 3 | valid |
| 425.0ms | 4 200× | 0 | invalid |
| 176.0ms | 202× | 5 | exit |
| 142.0ms | 999× | 0 | exit |
ival-mult: 10.1s (27.4% of total)adjust: 4.1s (11.2% of total)ival-pow: 4.0s (11% of total)ival-add: 3.7s (10% of total)ival-sub: 3.6s (9.8% of total)ival-div: 3.6s (9.6% of total)ival-sin: 2.3s (6.3% of total)ival-cos: 1.5s (4.1% of total)const: 1.5s (4.1% of total)ival-sqrt: 465.0ms (1.3% of total)ival-exp: 451.0ms (1.2% of total)ival-neg: 333.0ms (0.9% of total)exact: 270.0ms (0.7% of total)ival-pow2: 223.0ms (0.6% of total)ival-log1p: 146.0ms (0.4% of total)ival-expm1: 124.0ms (0.3% of total)ival-assert: 118.0ms (0.3% of total)ival-atan: 80.0ms (0.2% of total)ival-tan: 50.0ms (0.1% of total)ival-pi: 40.0ms (0.1% of total)ival-hypot: 29.0ms (0.1% of total)ival-<=: 16.0ms (0% of total)ival-true: 10.0ms (0% of total)ival-and: 9.0ms (0% of total)ival-if: 5.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-==: 3.0ms (0% of total)ival-<: 1.0ms (0% of total)| 359× | iter limit |
| 145× | node limit |
| 9× | saturated |
| 3× | unsound |
| 84× | iter limit |
| 64× | node limit |
| 20× | saturated |
Compiled 58 665 to 9 426 computations (83.9% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 1311 | 6 |
+.f64 | #f | cancellation | 358 | 77 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 224 | 0 |
sqrt.f64 | #f | oflow-rescue | 202 | 0 |
log.f64 | (log.f64 (+.f64 #s(literal 1 binary64) x)) | sensitivity | 160 | 0 |
/.f64 | #f | n/o | 156 | 0 |
/.f64 | #f | o/o | 156 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | sensitivity | 137 | 0 |
-.f64 | #f | nan-rescue | 108 | 0 |
/.f64 | #f | u/n | 90 | 0 |
/.f64 | #f | n/u | 65 | 0 |
/.f64 | #f | u/u | 60 | 0 |
/.f64 | #f | o/n | 54 | 0 |
+.f64 | #f | nan-rescue | 42 | 0 |
*.f64 | #f | n*o | 29 | 0 |
*.f64 | #f | n*u | 29 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | oflow-rescue | 26 | 0 |
| ↳ | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | overflow | 24 | |
| ↳ | (/.f64 i n) | overflow | 26 | |
| ↳ | (+.f64 #s(literal 1 binary64) (/.f64 i n)) | overflow | 26 | |
sqrt.f64 | #f | uflow-rescue | 12 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3864 | 208 |
| - | 120 | 6560 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3864 | 141 | 67 |
| - | 120 | 199 | 6361 |
| number | freq |
|---|---|
| 0 | 6768 |
| 1 | 3529 |
| 2 | 400 |
| 3 | 55 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 30 | 1 | 0 |
| - | 2 | 0 | 9 |
| 1.5s | 16 304× | 0 | valid |
| 1.2s | 3 704× | 1 | valid |
| 639.0ms | 1 462× | 2 | valid |
| 19.0ms | 32× | 3 | valid |
| 3.0ms | 2× | 4 | valid |
Compiled 7 535 to 1 486 computations (80.3% saved)
ival-mult: 644.0ms (28.2% of total)adjust: 387.0ms (16.9% of total)ival-pow: 256.0ms (11.2% of total)ival-add: 244.0ms (10.7% of total)ival-div: 210.0ms (9.2% of total)ival-sub: 174.0ms (7.6% of total)ival-sin: 105.0ms (4.6% of total)ival-cos: 63.0ms (2.8% of total)const: 45.0ms (2% of total)ival-exp: 30.0ms (1.3% of total)ival-sqrt: 25.0ms (1.1% of total)ival-pow2: 20.0ms (0.9% of total)ival-true: 18.0ms (0.8% of total)exact: 18.0ms (0.8% of total)ival-neg: 17.0ms (0.7% of total)ival-assert: 8.0ms (0.3% of total)ival-log1p: 5.0ms (0.2% of total)ival-tan: 4.0ms (0.2% of total)ival-atan: 4.0ms (0.2% of total)ival-pi: 4.0ms (0.2% of total)ival-expm1: 3.0ms (0.1% of total)| 26× | fuel |
| 16× | done |
Compiled 26 007 to 2 839 computations (89.1% saved)
Compiled 2 103 530 to 191 815 computations (90.9% saved)
96 calls:
| 599.0ms | x |
| 395.0ms | b |
| 360.0ms | a |
| 266.0ms | (*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x)))) |
| 211.0ms | c |
Compiled 8 693 to 5 755 computations (33.8% saved)
Compiled 139 918 to 62 300 computations (55.5% saved)
882 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 64.0ms | x | @ | -inf | ((* (+ (* -6450306886639899/50000000000000000 (* x x)) 238732414637843/250000000000000) x) (+ (* -6450306886639899/50000000000000000 (* x x)) 238732414637843/250000000000000) (* (* (- (* (pow x -2) 238732414637843/250000000000000) 6450306886639899/50000000000000000) x) x) (* (- (* (pow x -2) 238732414637843/250000000000000) 6450306886639899/50000000000000000) x) (/ 238732414637843/250000000000000 x) 238732414637843/250000000000000 x (* (+ (* -6450306886639899/50000000000000000 (* x x)) 238732414637843/250000000000000) x) (+ (* -6450306886639899/50000000000000000 (* x x)) 238732414637843/250000000000000) (* (* (- (* (pow x -2) 238732414637843/250000000000000) 6450306886639899/50000000000000000) x) x) (* (- (* (pow x -2) 238732414637843/250000000000000) 6450306886639899/50000000000000000) x) (- (* (pow x -2) 238732414637843/250000000000000) 6450306886639899/50000000000000000) -6450306886639899/50000000000000000 (/ (* (- (pow (* (* x x) -6450306886639899/50000000000000000) 2) 56993165798814994692847692649/62500000000000000000000000000) x) (+ (* (* -6450306886639899/50000000000000000 x) x) -238732414637843/250000000000000)) (* (- (pow (* (* x x) -6450306886639899/50000000000000000) 2) 56993165798814994692847692649/62500000000000000000000000000) x) (- (pow (* (* x x) -6450306886639899/50000000000000000) 2) 56993165798814994692847692649/62500000000000000000000000000) -56993165798814994692847692649/62500000000000000000000000000 (+ (* (* -6450306886639899/50000000000000000 x) x) -238732414637843/250000000000000) (* -6450306886639899/50000000000000000 x) -238732414637843/250000000000000) |
| 53.0ms | y | @ | 0 | ((- (pow x 4) (pow y 4)) (neg (pow y 4)) (pow y 4) y 4 (- (pow x 4) (pow y 4)) (pow x 4) x (* (+ (* x x) (* y y)) (- (* x x) (* y y))) (+ (* x x) (* y y)) (* y y) (- (* x x) (* y y)) (* x x)) |
| 51.0ms | eps | @ | -inf | ((/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (+ 1 (/ 1 eps)) 1 (/ 1 eps) eps (exp (neg (* (- 1 eps) x))) (neg (* (- 1 eps) x)) (* (- 1 eps) x) (- 1 eps) x (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x)))) (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))) (neg (* (+ 1 eps) x)) (* (+ 1 eps) x) (+ 1 eps) 2) |
| 50.0ms | b | @ | -inf | ((/ (* (/ (PI) (* (* 2 (+ a b)) (- b a))) (- b a)) (* a b)) (* (/ (PI) (* (* 2 (+ a b)) (- b a))) (- b a)) (/ (PI) (* (* 2 (+ a b)) (- b a))) (PI) (* (* 2 (+ a b)) (- b a)) (* 2 (+ a b)) 2 (+ a b) a b (- b a) (* a b) (* (* (/ (PI) 2) (/ 1 (- (* b b) (* a a)))) (- (/ 1 a) (/ 1 b))) (* (/ (PI) (* a (* a b))) 1/2) (/ (PI) (* a (* a b))) (* a (* a b)) 1/2 (/ (* (- (* 1 b) (* a 1)) (* (PI) 1)) (* (* a b) (* 2 (* (+ b a) (- b a))))) (* (- (* 1 b) (* a 1)) (* (PI) 1)) (* (PI) b) (* (* a b) (* 2 (* (+ b a) (- b a)))) (* 2 (* (+ b a) (- b a))) (* (+ b a) (- b a)) (+ b a) (* (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (- (/ 1 a) (/ 1 b))) (* (/ (/ (PI) 2) (+ b a)) (/ 1 (- b a))) (* (/ (PI) (* a a)) -1/2) (/ (PI) (* a a)) (* a a) -1/2 (- (/ 1 a) (/ 1 b)) (/ 1 a) 1 (/ 1 b) (/ (* (- (* 1 b) (* a 1)) (* (PI) 1)) (* a (* b (* (* 2 (+ a b)) (- b a))))) (* (- (* 1 b) (* a 1)) (* (PI) 1)) (- (* 1 b) (* a 1)) (* 1 b) (* a 1) (* (PI) 1) (* a (* b (* (* 2 (+ a b)) (- b a)))) (* b (* (* 2 (+ a b)) (- b a)))) |
| 50.0ms | b | @ | inf | ((* (+ a (+ b (+ c d))) 2) (* 2 (+ b (+ (+ d c) a))) 2 (+ b (+ (+ d c) a)) b (+ (+ d c) a) (* c (+ 1 (/ (+ a d) c))) c (+ 1 (/ (+ a d) c)) 1 (/ (+ a d) c) (+ a d) a d (* (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) 2) (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) (* (+ a (+ (+ c b) d)) 2) (+ a (+ (+ c b) d)) (+ (+ c b) d) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ c b) a) d) 2) 2) d) (+ (* (/ (+ (+ c b) a) d) 2) 2) (/ (+ (+ c b) a) d) (+ (+ c b) a) (+ c b) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) b) a) 2) 2) a) (+ (* (/ (+ (+ d c) b) a) 2) 2) (/ (+ (+ d c) b) a) (+ (+ d c) b) (+ d c)) |
| 43× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 54.5% | 45.5% | 0% | 0% | 0% | 0 |
| 21.4% | 11.7% | 42.9% | 45.5% | 0% | 0% | 0% | 1 |
| 37.4% | 20.4% | 34.1% | 45.5% | 0% | 0% | 0% | 2 |
| 48.7% | 26.2% | 27.7% | 45.5% | 0% | 0.6% | 0% | 3 |
| 57.7% | 30.7% | 22.6% | 45.5% | 0% | 1.2% | 0% | 4 |
| 71.2% | 37.7% | 15.3% | 45.5% | 0% | 1.6% | 0% | 5 |
| 72.9% | 38.4% | 14.3% | 45.5% | 0% | 1.8% | 0% | 6 |
| 77.9% | 40.7% | 11.6% | 45.5% | 0% | 2.2% | 0% | 7 |
| 81.5% | 42.6% | 9.7% | 45.5% | 0% | 2.3% | 0% | 8 |
| 84.1% | 43.8% | 8.3% | 45.5% | 0% | 2.5% | 0% | 9 |
| 86.2% | 44.6% | 7.2% | 45.5% | 0% | 2.7% | 0% | 10 |
| 88.2% | 45.6% | 6.1% | 45.5% | 0% | 2.8% | 0% | 11 |
| 89.1% | 45.9% | 5.6% | 45.5% | 0% | 2.9% | 0% | 12 |
Compiled 1 402 to 721 computations (48.6% saved)
| 182× | binary-search |
| 104× | left-value |
| 164× | narrow-enough |
| 17× | predicate-same |
| 1× | predicate-failed |
| 1.1s | 11 339× | 0 | valid |
| 346.0ms | 991× | 1 | valid |
| 295.0ms | 522× | 2 | valid |
| 142.0ms | 1 381× | 0 | invalid |
| 14.0ms | 94× | 0 | exit |
| 11.0ms | 12× | 3 | valid |
Compiled 145 962 to 76 304 computations (47.7% saved)
ival-mult: 464.0ms (31.6% of total)ival-pow: 215.0ms (14.7% of total)ival-div: 214.0ms (14.6% of total)ival-sub: 185.0ms (12.6% of total)ival-add: 114.0ms (7.8% of total)adjust: 95.0ms (6.5% of total)ival-exp: 63.0ms (4.3% of total)ival-neg: 42.0ms (2.9% of total)ival-sqrt: 29.0ms (2% of total)exact: 12.0ms (0.8% of total)ival-pi: 10.0ms (0.7% of total)ival-true: 10.0ms (0.7% of total)ival-assert: 5.0ms (0.3% of total)const: 4.0ms (0.3% of total)ival-expm1: 4.0ms (0.3% of total)| 33× | node limit |
| 9× | saturated |
Loading profile data...