
| Date: | Sunday, December 29th, 2024 |
|---|---|
| Commit: | fbbe2c7d on main |
| Seed: | 2024364 |
| 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: | 241 869.3 MB |
Time bar (total: 4.5min)
| 29.3s | 43 862× | 2 | valid |
| 24.2s | 148 999× | 0 | invalid |
| 21.4s | 96 553× | 1 | valid |
| 17.8s | 7 075× | 5 | exit |
| 8.0s | 87 361× | 0 | valid |
| 2.9s | 3 389× | 3 | valid |
| 332.0ms | 4 263× | 0 | exit |
| 4.0ms | 3× | 4 | valid |
ival-pow: 16.9s (19.3% of total)ival-tan: 12.9s (14.7% of total)adjust: 8.7s (10% of total)ival-mult: 6.5s (7.4% of total)const: 5.3s (6.1% of total)ival-cos: 4.4s (5.1% of total)ival-div: 4.3s (4.9% of total)ival-log: 3.9s (4.4% of total)ival-sub: 3.7s (4.2% of total)ival-sin: 3.3s (3.8% of total)ival-add: 3.0s (3.4% of total)ival-<=: 2.4s (2.8% of total)ival-exp: 2.3s (2.6% of total)ival-fabs: 2.1s (2.4% of total)ival-expm1: 1.8s (2% of total)ival-sqrt: 1.3s (1.5% of total)ival-log1p: 1.2s (1.4% of total)ival-<: 724.0ms (0.8% of total)ival-and: 627.0ms (0.7% of total)ival-fmin: 484.0ms (0.6% of total)ival-neg: 357.0ms (0.4% of total)exact: 347.0ms (0.4% of total)ival-atan: 331.0ms (0.4% of total)ival->: 257.0ms (0.3% of total)ival-cbrt: 232.0ms (0.3% of total)ival-assert: 161.0ms (0.2% of total)ival-true: 69.0ms (0.1% of total)| 328× | iter limit |
| 219× | node limit |
| 27× | saturated |
| 9.0s | 6 009× | 2 | valid |
| 8.5s | 10 958× | 1 | valid |
| 2.9s | 10 150× | 0 | valid |
| 886.0ms | 487× | 3 | valid |
| 126.0ms | 56× | 5 | exit |
| 84.0ms | 142× | 0 | invalid |
| 75.0ms | 78× | 0 | exit |
| 36.0ms | 24× | 1 | exit |
Compiled 23 145 to 3 478 computations (85% saved)
adjust: 3.7s (21.1% of total)ival-mult: 2.6s (14.6% of total)ival-tan: 2.5s (14.3% of total)ival-div: 1.5s (8.6% of total)ival-add: 1.0s (5.7% of total)ival-sub: 973.0ms (5.5% of total)ival-log: 971.0ms (5.5% of total)ival-pow: 880.0ms (5% of total)ival-sin: 806.0ms (4.5% of total)const: 674.0ms (3.8% of total)ival-cos: 555.0ms (3.1% of total)ival-exp: 318.0ms (1.8% of total)ival-sqrt: 269.0ms (1.5% of total)ival-neg: 225.0ms (1.3% of total)ival-log1p: 196.0ms (1.1% of total)ival-pow2: 128.0ms (0.7% of total)ival-cosh: 55.0ms (0.3% of total)ival-cbrt: 55.0ms (0.3% of total)ival-expm1: 52.0ms (0.3% of total)exact: 45.0ms (0.3% of total)ival-pi: 23.0ms (0.1% of total)ival-true: 22.0ms (0.1% of total)ival-hypot: 19.0ms (0.1% of total)ival-atan2: 13.0ms (0.1% of total)ival-assert: 12.0ms (0.1% of total)ival-atan: 10.0ms (0.1% of total)ival-fabs: 10.0ms (0.1% of total)ival-sinh: 7.0ms (0% of total)ival->: 1.0ms (0% of total)ival-then: 0.0ms (0% of total)| 221× | iter limit |
| 109× | node limit |
| 204× | iter limit |
| 139× | node limit |
| 25× | fuel |
| 3× | done |
Compiled 7 824 to 2 020 computations (74.2% saved)
Compiled 2 282 853 to 242 159 computations (89.4% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 4124 | 40 |
log.f64 | #f | sensitivity | 763 | 3 |
/.f64 | #f | u/u | 442 | 0 |
sqrt.f64 | #f | oflow-rescue | 384 | 0 |
+.f64 | #f | cancellation | 342 | 1 |
/.f64 | #f | u/n | 108 | 0 |
pow.f64 | (pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n)) | sensitivity | 64 | 0 |
/.f64 | (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) | n/u | 21 | 0 |
| ↳ | (*.f64 b eps) | underflow | 142 | |
| ↳ | (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) | underflow | 145 | |
| ↳ | (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) | underflow | 142 | |
| ↳ | (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))) | underflow | 227 | |
| ↳ | (*.f64 a eps) | underflow | 145 | |
sqrt.f64 | #f | uflow-rescue | 20 | 0 |
-.f64 | #f | nan-rescue | 19 | 0 |
cos.f64 | (cos.f64 (+.f64 x eps)) | sensitivity | 8 | 0 |
tan.f64 | (tan.f64 (+.f64 x eps)) | sensitivity | 7 | 1 |
sin.f64 | (sin.f64 (+.f64 x eps)) | sensitivity | 6 | 1 |
exp.f64 | (exp.f64 (neg.f64 x)) | sensitivity | 3 | 2 |
/.f64 | (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x)) | n/o | 2 | 0 |
| ↳ | (*.f64 x x) | overflow | 67 | |
/.f64 | (/.f64 (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) (-.f64 (exp.f64 x) #s(literal 1 binary64))) | o/o | 2 | 0 |
| ↳ | (exp.f64 (*.f64 #s(literal 2 binary64) x)) | overflow | 2 | |
| ↳ | (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) | overflow | 2 | |
| ↳ | (exp.f64 x) | overflow | 2 | |
| ↳ | (-.f64 (exp.f64 x) #s(literal 1 binary64)) | overflow | 2 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 5216 | 22 |
| - | 116 | 1814 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5216 | 18 | 4 |
| - | 116 | 28 | 1786 |
| number | freq |
|---|---|
| 0 | 1836 |
| 1 | 4553 |
| 2 | 629 |
| 3 | 96 |
| 4 | 54 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 28 | 0 | 0 |
| - | 0 | 0 | 0 |
| 1.9s | 2 764× | 2 | valid |
| 1.3s | 6 044× | 1 | valid |
| 479.0ms | 5 328× | 0 | valid |
| 169.0ms | 200× | 3 | valid |
Compiled 2 154 to 763 computations (64.6% saved)
ival-tan: 881.0ms (28.7% of total)adjust: 444.0ms (14.5% of total)ival-log: 259.0ms (8.4% of total)ival-cos: 226.0ms (7.4% of total)ival-sin: 183.0ms (6% of total)ival-div: 172.0ms (5.6% of total)ival-sub: 165.0ms (5.4% of total)ival-exp: 145.0ms (4.7% of total)ival-pow: 143.0ms (4.7% of total)ival-add: 107.0ms (3.5% of total)ival-mult: 98.0ms (3.2% of total)ival-log1p: 62.0ms (2% of total)ival-sqrt: 56.0ms (1.8% of total)ival-cbrt: 37.0ms (1.2% of total)ival-expm1: 27.0ms (0.9% of total)ival-atan: 24.0ms (0.8% of total)ival-neg: 15.0ms (0.5% of total)ival-true: 12.0ms (0.4% of total)exact: 8.0ms (0.3% of total)ival-assert: 6.0ms (0.2% of total)| 56× | iter limit |
| 33× | saturated |
| 23× | node limit |
Compiled 18 262 to 5 601 computations (69.3% saved)
507 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 149.0ms | b_2 | @ | -inf | ((* (- 1 (* (/ (/ c b_2) b_2) a)) b_2) (* (* (- 1 (* (/ (/ c b_2) b_2) a)) b_2) b_2) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (* -1/2 (/ c b_2)) (/ c b_2) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (neg b_2) (sqrt (- (* b_2 b_2) (* a c))) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c))) (/ (- (neg b_2) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4)) a) (- (neg b_2) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4)) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4) (sqrt (- (* b_2 b_2) (* a c))) (* (/ (/ c b_2) b_2) a) (- (* b_2 b_2) (* a c)) (- (* b_2 b_2) (* a c)) (+ (* c a) (* b_2 b_2))) |
| 90.0ms | b_2 | @ | 0 | ((/ (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) a) (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) (pow (- (* b_2 b_2) (* a c)) 1/8) (- (* b_2 b_2) (* a c)) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (* -2 b_2) (* (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (neg b_2)) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (/ (/ c b_2) b_2) (+ (* (* (/ (* c c) b_2) (/ a (* b_2 b_2))) -1/8) (* (/ c b_2) -1/2)) (* (/ (* c c) b_2) (/ a (* b_2 b_2))) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (/ (* c c) b_2) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c))) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4)) (pow (- (* b_2 b_2) (* a c)) 3/4) (/ a (* b_2 b_2)) (sqrt (- (* b_2 b_2) (* a c))) (* (/ c b_2) a)) |
| 75.0ms | a | @ | 0 | ((/ (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) a) (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) (pow (- (* b_2 b_2) (* a c)) 1/8) (- (* b_2 b_2) (* a c)) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (* -2 b_2) (* (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (neg b_2)) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (/ (/ c b_2) b_2) (+ (* (* (/ (* c c) b_2) (/ a (* b_2 b_2))) -1/8) (* (/ c b_2) -1/2)) (* (/ (* c c) b_2) (/ a (* b_2 b_2))) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (/ (* c c) b_2) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c))) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4)) (pow (- (* b_2 b_2) (* a c)) 3/4) (/ a (* b_2 b_2)) (sqrt (- (* b_2 b_2) (* a c))) (* (/ c b_2) a)) |
| 62.0ms | a | @ | inf | ((/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ (/ (+ b a) b) a) (/ (+ b a) b) (+ b a) (/ (+ (* (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) b) 1) b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (+ (* (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) b) 1) (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) (/ (pow (exp a) eps) (- (exp (* eps a)) 1))) |
| 56.0ms | x | @ | inf | ((/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (- (neg (log (+ 1 x))) (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2) (/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n))) n)) (log x)) (neg n)) (+ (- (neg (log (+ 1 x))) (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2) (/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n))) n)) (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (/ (log x) n)) (* n x)) (/ (/ 1 n) x) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (/ (exp (/ (log x) n)) x) n) (/ (exp (/ (log x) n)) x) (exp (/ (log x) n)) (+ (* (+ (* (neg x) (- (/ 1/2 n) (/ 1/2 (* n n)))) (/ 1 n)) x) (/ (neg (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (+ (* 1/2 (/ (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n)) (- (log (+ 1 x)) (log x)))) (neg n)) (+ (* (neg x) (- (/ 1/2 n) (/ 1/2 (* n n)))) (/ 1 n)) (* (/ (/ 2 n) 4) 4) (/ (/ 2 n) 4) (pow (pow x (pow n -1)) 2) (/ (- (pow (+ 1 x) (* (/ (/ 2 n) 4) 4)) (pow (pow x (pow n -1)) 2)) (+ (pow (pow (+ 1 x) 2) (/ (/ 2 n) 4)) (pow x (pow n -1)))) (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (/ (log x) n) (/ 1/2 (* n n)) (- (pow (+ 1 x) (* (/ (/ 2 n) 4) 4)) (pow (pow x (pow n -1)) 2)) (pow (pow (+ 1 x) 2) (/ (/ 2 n) 4)) (pow (+ 1 x) (* (/ (/ 2 n) 4) 4))) |
Compiled 103 105 to 54 395 computations (47.2% saved)
43 calls:
| 864.0ms | x |
| 365.0ms | eps |
| 132.0ms | (-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x)) |
| 131.0ms | n |
| 115.0ms | b |
Compiled 2 285 to 2 124 computations (7% saved)
| 28× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 61.1% | 38.9% | 0% | 0% | 0% | 0 |
| 7.4% | 4.5% | 56.6% | 38.9% | 0% | 0% | 0% | 1 |
| 22.3% | 13.6% | 47.5% | 38.9% | 0% | 0% | 0% | 2 |
| 40.2% | 23.5% | 34.9% | 38.9% | 0% | 2.7% | 0% | 3 |
| 53.4% | 31.1% | 27.2% | 38.9% | 0% | 2.8% | 0% | 4 |
| 63% | 36.3% | 21.3% | 38.9% | 0% | 3.6% | 0% | 5 |
| 65.9% | 37.5% | 19.4% | 38.9% | 0% | 4.2% | 0% | 6 |
| 70.4% | 38.8% | 16.3% | 38.9% | 0% | 6% | 0% | 7 |
| 73.6% | 40.2% | 14.4% | 38.9% | 0% | 6.5% | 0% | 8 |
| 76.3% | 40.9% | 12.7% | 38.9% | 0% | 7.5% | 0% | 9 |
| 78.4% | 41.4% | 11.4% | 38.9% | 0% | 8.3% | 0% | 10 |
| 81.1% | 42.4% | 9.9% | 38.9% | 0% | 8.8% | 0% | 11 |
| 82.3% | 42.7% | 9.2% | 38.9% | 0% | 9.3% | 0% | 12 |
Compiled 483 to 337 computations (30.2% saved)
| 69× | binary-search |
| 15× | left-value |
| 64× | narrow-enough |
| 5× | predicate-same |
| 326.0ms | 4 110× | 0 | valid |
| 79.0ms | 572× | 1 | valid |
| 77.0ms | 776× | 0 | invalid |
| 60.0ms | 228× | 2 | valid |
| 1.0ms | 15× | 0 | exit |
| 1.0ms | 2× | 3 | valid |
Compiled 23 219 to 17 617 computations (24.1% saved)
ival-mult: 91.0ms (24.8% of total)ival-neg: 46.0ms (12.5% of total)ival-div: 41.0ms (11.2% of total)ival-sub: 35.0ms (9.5% of total)ival-sqrt: 32.0ms (8.7% of total)adjust: 29.0ms (7.9% of total)ival-pow: 29.0ms (7.9% of total)ival-add: 25.0ms (6.8% of total)ival-cos: 10.0ms (2.7% of total)ival-expm1: 8.0ms (2.2% of total)ival-exp: 6.0ms (1.6% of total)ival-cbrt: 5.0ms (1.4% of total)ival-true: 4.0ms (1.1% of total)exact: 3.0ms (0.8% of total)ival-assert: 2.0ms (0.5% of total)ival-tan: 1.0ms (0.3% of total)Loading profile data...