
| Date: | Saturday, December 28th, 2024 |
|---|---|
| Commit: | e085da8f on no-big-exponents |
| Seed: | 2024363 |
| 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: | 1 755 289.6 MB |
Time bar (total: 27.9min)
| 3.9min | 2 144 411× | 0 | valid |
| 24.7s | 69 719× | 1 | valid |
| 12.4s | 64 027× | 0 | invalid |
| 1.9s | 6 024× | 2 | valid |
| 1.6s | 1 579× | 5 | exit |
| 645.0ms | 1 840× | 1 | invalid |
| 271.0ms | 710× | 3 | valid |
ival-mult: 57.2s (33.9% of total)ival-add: 24.1s (14.3% of total)ival-sub: 21.6s (12.8% of total)ival-div: 19.2s (11.3% of total)ival-log: 9.9s (5.9% of total)ival-sin: 7.6s (4.5% of total)const: 6.3s (3.7% of total)adjust: 6.2s (3.7% of total)ival-sqrt: 5.2s (3.1% of total)ival-cos: 3.7s (2.2% of total)ival-exp: 2.2s (1.3% of total)ival-true: 1.6s (1% of total)exact: 1.1s (0.6% of total)ival-assert: 869.0ms (0.5% of total)ival-acos: 459.0ms (0.3% of total)ival-hypot: 373.0ms (0.2% of total)ival-tan: 365.0ms (0.2% of total)ival-fabs: 280.0ms (0.2% of total)ival-sinh: 250.0ms (0.1% of total)ival-cosh: 245.0ms (0.1% of total)ival-tanh: 116.0ms (0.1% of total)| 2 865× | iter limit |
| 1 475× | node limit |
| 726× | saturated |
| 4× | unsound |
| 2 006× | iter limit |
| 911× | node limit |
| 38× | unsound |
| 18× | saturated |
| 1 433× | iter limit |
| 976× | node limit |
| 155× | fuel |
| 114× | done |
| 21× | saturated |
| 11× | unsound |
Compiled 129 031 to 18 867 computations (85.4% saved)
| 57.9s | 218 630× | 0 | valid |
| 12.1s | 11 935× | 1 | valid |
| 5.5s | 3 358× | 2 | valid |
| 4.2s | 9 415× | 0 | invalid |
| 915.0ms | 662× | 5 | exit |
| 556.0ms | 1 130× | 0 | exit |
| 428.0ms | 291× | 3 | valid |
| 141.0ms | 56× | 1 | invalid |
| 42.0ms | 6× | 1 | exit |
| 33.0ms | 21× | 4 | valid |
Compiled 150 673 to 23 866 computations (84.2% saved)
ival-mult: 19.0s (33.6% of total)ival-div: 7.7s (13.6% of total)ival-add: 7.4s (13% of total)ival-sub: 4.5s (7.9% of total)adjust: 4.0s (7.1% of total)const: 2.5s (4.3% of total)ival-log: 2.1s (3.6% of total)ival-sin: 1.8s (3.2% of total)ival-pow: 1.7s (3% of total)ival-neg: 1.4s (2.5% of total)ival-sqrt: 1.1s (2% of total)ival-cos: 1.0s (1.8% of total)ival-pow2: 887.0ms (1.6% of total)ival-exp: 459.0ms (0.8% of total)exact: 243.0ms (0.4% of total)ival-true: 183.0ms (0.3% of total)ival-assert: 152.0ms (0.3% of total)ival-hypot: 91.0ms (0.2% of total)ival-acos: 91.0ms (0.2% of total)ival-log1p: 70.0ms (0.1% of total)ival-sinh: 59.0ms (0.1% of total)ival-cosh: 50.0ms (0.1% of total)ival-tan: 30.0ms (0.1% of total)ival-expm1: 23.0ms (0% of total)ival-fabs: 22.0ms (0% of total)ival-tanh: 21.0ms (0% of total)ival-pi: 20.0ms (0% of total)ival-sinu: 16.0ms (0% of total)ival-asin: 14.0ms (0% of total)ival->: 4.0ms (0% of total)ival-then: 1.0ms (0% of total)Compiled 17 045 914 to 1 599 527 computations (90.6% saved)
510 calls:
| 10.8s | x |
| 9.0s | y |
| 8.1s | z |
| 4.5s | t |
| 2.4s | a |
Compiled 37 150 to 56 543 computations (-52.2% saved)
| 536× | iter limit |
| 398× | saturated |
| 142× | node limit |
Compiled 296 130 to 61 290 computations (79.3% saved)
9123 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 699.0ms | y | @ | inf | ((+ (* (neg x) (* (/ (+ 1/2 y) x) (log y))) x) (- (+ (- x (* (+ y 1/2) (log y))) y) z) (+ (- x (* (+ y 1/2) (log y))) y) (- x (* (+ y 1/2) (log y))) (- (+ (- x (* (+ y 1/2) (log y))) y) z) (* (- (/ (+ (* (- (neg y) 1/2) (log y)) (+ y x)) z) 1) z) (- (/ (+ (* (- (neg y) 1/2) (log y)) (+ y x)) z) 1) (/ x z) (- (+ (- x (* (+ y 1/2) (log y))) y) z) (- (+ (* -1/2 (log y)) x) z) (+ (* -1/2 (log y)) x) (* -1/2 (log y)) (- (+ (- x (* (+ y 1/2) (log y))) y) z) (- y (+ (* (+ 1/2 y) (log y)) z)) (+ (* (+ 1/2 y) (log y)) z) (+ 1/2 y) (- (+ (- x (* (+ y 1/2) (log y))) y) z) (* (- (/ (+ (* (- (neg y) 1/2) (log y)) (+ y x)) z) 1) z) (- (/ (+ (* (- (neg y) 1/2) (log y)) (+ y x)) z) 1) (/ (- y (* (log y) y)) z) (* (/ (+ 1/2 y) x) (log y)) (/ (+ 1/2 y) x) (log y) (* (log y) y)) |
| 293.0ms | t | @ | inf | ((+ (* y (* (* -9 z) t)) (+ (* (* b 27) a) (* 2 x))) (* (* -9 z) t) (* -9 z) (+ (* (* b 27) a) (* 2 x)) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* 2 x) (* (* b a) 27)) (* (* b a) 27) (* b a) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* -9 (* (* z y) t)) (* (* b a) 27)) (* (* z y) t) (* z y) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (- (* x 2) (* (* (* y 9) z) t)) (* (* -9 (* z y)) t) (* -9 (* z y)) (+ (* (* b 27) a) (+ (* (* (* -9 y) t) z) (* 2 x))) (* b 27) (+ (* (* (* -9 y) t) z) (* 2 x)) (* (* -9 y) t) (* -9 y)) |
| 279.0ms | t | @ | inf | ((+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (+ (* (log t) (+ -1/2 a)) (log (* z y))) t) (+ (* (log t) (+ -1/2 a)) (log (* z y))) (log t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (log (pow t a)) (pow t a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (- (log (* z (* (pow t (+ -1/2 a)) y))) t) (log (* z (* (pow t (+ -1/2 a)) y))) (* z (* (pow t (+ -1/2 a)) y)) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (+ (+ (* (+ -1/2 a) (log t)) (log z)) (- (log y) t)) (+ (* (+ -1/2 a) (log t)) (log z)) (+ -1/2 a) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (+ (+ (* (+ -1/2 a) (log t)) (log (+ y x))) (log z)) (+ (* (+ -1/2 a) (log t)) (log (+ y x))) (+ -1/2 a) (log (* z y)) (* (pow t (+ -1/2 a)) y) (- (log y) t)) |
| 277.0ms | z | @ | 0 | ((+ (+ (- (log z) t) (log (+ y x))) (* (- a 1/2) (log t))) (+ (- (log z) t) (log (+ y x))) (- (log z) t) (log z) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (neg t) (+ (- (+ (log (+ x y)) (log z)) t) (* (- a 1/2) (log t))) (+ (+ (* (+ -1/2 a) (log t)) (log z)) (- (log y) t)) (+ (* (+ -1/2 a) (log t)) (log z)) (+ -1/2 a) (+ (- (+ (log (+ x y)) (log z)) t) (/ (* (- (* a a) 1/4) (log t)) (+ 1/2 a))) (- (+ (log (+ x y)) (log z)) t) (+ (log (+ x y)) (log z)) (log (+ x y)) (- (/ (pow (log (+ y x)) 2) (- (log (+ y x)) (- (log z) t))) (/ (pow (- (log z) t) 2) (- (log (+ y x)) (- (log z) t)))) (+ (- (/ (pow (log (+ y x)) 2) (- (log (+ y x)) (- (log z) t))) (/ (pow (- (log z) t) 2) (- (log (+ y x)) (- (log z) t)))) (* (- a 1/2) (log t))) (/ (pow (log (+ y x)) 2) (- (log (+ y x)) (- (log z) t))) (pow (log (+ y x)) 2) (* (- a 1/2) (log t)) (- (log y) t) (/ (* (- (* a a) 1/4) (log t)) (+ 1/2 a)) (* (- (* a a) 1/4) (log t)) (/ (pow (- (log z) t) 2) (- (log (+ y x)) (- (log z) t))) (pow (- (log z) t) 2)) |
| 250.0ms | y | @ | inf | ((* x (log (pow (* y x) (/ (log (/ x y)) (log (* y x)))))) (log (pow (* y x) (/ (log (/ x y)) (log (* y x))))) (pow (* y x) (/ (log (/ x y)) (log (* y x)))) (* y x) (/ 0 0) (* x (/ (- (pow (log x) 2) (pow (log y) 2)) (log (* y x)))) (/ (- (pow (log x) 2) (pow (log y) 2)) (log (* y x))) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) (* x (/ (- (* (pow (log (neg x)) 2) (log (* (neg y) (neg x)))) (* (log (* (neg y) (neg x))) (pow (log (neg y)) 2))) (pow (log (* (neg y) (neg x))) 2))) (/ (- (* (pow (log (neg x)) 2) (log (* (neg y) (neg x)))) (* (log (* (neg y) (neg x))) (pow (log (neg y)) 2))) (pow (log (* (neg y) (neg x))) 2)) (- (* (pow (log (neg x)) 2) (log (* (neg y) (neg x)))) (* (log (* (neg y) (neg x))) (pow (log (neg y)) 2))) (* (pow (log (neg x)) 2) (log (* (neg y) (neg x)))) (/ (+ (* (* (* (+ (log (neg y)) (log (neg x))) (log (/ x y))) x) (* (log (* (neg y) (neg x))) 2)) (* (* (log (* (neg y) (neg x))) 2) (* (* (log (* (neg y) (neg x))) (log (/ x y))) x))) (* (* (log (* (neg y) (neg x))) 2) (* (log (* (neg y) (neg x))) 2))) (+ (* (* (* (+ (log (neg y)) (log (neg x))) (log (/ x y))) x) (* (log (* (neg y) (neg x))) 2)) (* (* (log (* (neg y) (neg x))) 2) (* (* (log (* (neg y) (neg x))) (log (/ x y))) x))) (* (* (+ (log (neg y)) (log (neg x))) (log (/ x y))) x) (* (+ (log (neg y)) (log (neg x))) (log (/ x y))) (log (* y x)) (log (/ x y)) (log x) (log y) (log (neg x)) (log (neg y)) (log (* (neg y) (neg x))) (neg x)) |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
log.f64 | #f | sensitivity | 1571 | 2 |
/.f64 | #f | o/n | 1217 | 0 |
sqrt.f64 | #f | oflow-rescue | 741 | 0 |
-.f64 | #f | cancellation | 600 | 5 |
/.f64 | #f | o/o | 577 | 0 |
*.f64 | #f | n*o | 526 | 0 |
+.f64 | #f | nan-rescue | 477 | 0 |
-.f64 | #f | nan-rescue | 447 | 0 |
cos.f64 | #f | sensitivity | 356 | 0 |
+.f64 | #f | cancellation | 344 | 0 |
/.f64 | #f | n/o | 332 | 0 |
/.f64 | #f | u/n | 248 | 0 |
sin.f64 | #f | sensitivity | 231 | 0 |
*.f64 | #f | n*u | 189 | 0 |
cos.f64 | #f | oflow-rescue | 149 | 0 |
/.f64 | #f | n/u | 144 | 0 |
/.f64 | #f | u/u | 104 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | sensitivity | 93 | 0 |
log.f64 | #f | oflow-rescue | 91 | 0 |
log.f64 | #f | uflow-rescue | 80 | 0 |
sqrt.f64 | #f | uflow-rescue | 45 | 0 |
*.f64 | #f | o*u | 34 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 27 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 27 | |
sin.f64 | (sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 27 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 27 | |
exp.f64 | #f | sensitivity | 24 | 4 |
*.f64 | (*.f64 (*.f64 (-.f64 (*.f64 x #s(literal 1/2 binary64)) y) (sqrt.f64 (*.f64 z #s(literal 2 binary64)))) (exp.f64 (/.f64 (*.f64 t t) #s(literal 2 binary64)))) | u*o | 1 | 0 |
| ↳ | (*.f64 (-.f64 (*.f64 x #s(literal 1/2 binary64)) y) (sqrt.f64 (*.f64 z #s(literal 2 binary64)))) | underflow | 1 | |
| ↳ | (exp.f64 (/.f64 (*.f64 t t) #s(literal 2 binary64))) | overflow | 129 | |
| ↳ | (/.f64 (*.f64 t t) #s(literal 2 binary64)) | overflow | 63 | |
| ↳ | (*.f64 t t) | overflow | 63 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 6093 | 198 |
| - | 1696 | 60877 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 6093 | 3 | 195 |
| - | 1696 | 9 | 60868 |
| number | freq |
|---|---|
| 0 | 61075 |
| 1 | 7005 |
| 2 | 707 |
| 3 | 59 |
| 4 | 12 |
| 5 | 5 |
| 6 | 1 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 136 | 0 | 0 |
| - | 2 | 0 | 131 |
| 13.9s | 130 346× | 0 | valid |
| 2.4s | 6 012× | 1 | valid |
| 755.0ms | 1 286× | 2 | valid |
| 29.0ms | 82× | 3 | valid |
| 1.0ms | 2× | 4 | valid |
Compiled 24 442 to 8 402 computations (65.6% saved)
ival-mult: 3.0s (32.4% of total)ival-add: 1.4s (14.6% of total)ival-sub: 1.2s (13.3% of total)ival-div: 920.0ms (9.8% of total)ival-log: 787.0ms (8.4% of total)adjust: 606.0ms (6.4% of total)ival-cos: 312.0ms (3.3% of total)const: 302.0ms (3.2% of total)ival-sin: 224.0ms (2.4% of total)ival-sqrt: 206.0ms (2.2% of total)ival-true: 112.0ms (1.2% of total)ival-exp: 81.0ms (0.9% of total)exact: 67.0ms (0.7% of total)ival-assert: 56.0ms (0.6% of total)ival-cosh: 12.0ms (0.1% of total)ival-tan: 11.0ms (0.1% of total)ival-fabs: 11.0ms (0.1% of total)ival-sinh: 10.0ms (0.1% of total)ival-hypot: 9.0ms (0.1% of total)ival-tanh: 7.0ms (0.1% of total)ival-acos: 4.0ms (0% of total)Compiled 820 020 to 438 905 computations (46.5% saved)
| 1 573× | binary-search |
| 995× | left-value |
| 1 546× | narrow-enough |
| 27× | predicate-same |
| 18.2s | 126 422× | 0 | valid |
| 1.5s | 4 310× | 1 | valid |
| 408.0ms | 3 498× | 0 | invalid |
| 30.0ms | 128× | 2 | valid |
| 27.0ms | 44× | 1 | invalid |
| 1.0ms | 4× | 3 | valid |
Compiled 830 133 to 604 173 computations (27.2% saved)
ival-mult: 5.2s (38.9% of total)ival-sub: 2.4s (17.8% of total)ival-add: 1.5s (11.3% of total)ival-div: 1.3s (9.8% of total)const: 598.0ms (4.5% of total)ival-log: 573.0ms (4.3% of total)ival-sqrt: 529.0ms (4% of total)adjust: 339.0ms (2.5% of total)ival-sin: 310.0ms (2.3% of total)ival-cos: 221.0ms (1.7% of total)ival-exp: 146.0ms (1.1% of total)ival-true: 95.0ms (0.7% of total)ival-assert: 52.0ms (0.4% of total)exact: 52.0ms (0.4% of total)ival-tanh: 29.0ms (0.2% of total)ival-sinh: 11.0ms (0.1% of total)ival-cosh: 8.0ms (0.1% of total)ival-fabs: 4.0ms (0% of total)| 269× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 99.9% | 0.1% | 0% | 0% | 0% | 0 |
| 46.8% | 46.8% | 53.1% | 0.1% | 0% | 0% | 0% | 1 |
| 50.5% | 50.1% | 49.2% | 0.1% | 0% | 0.6% | 0% | 2 |
| 58.6% | 57% | 40.3% | 0.1% | 0% | 2.6% | 0% | 3 |
| 65.2% | 62.7% | 33.5% | 0.1% | 0% | 3.6% | 0% | 4 |
| 71.2% | 68.2% | 27.5% | 0.1% | 0% | 4.1% | 0% | 5 |
| 75.9% | 72.3% | 23% | 0.1% | 0% | 4.6% | 0% | 6 |
| 79.8% | 75.6% | 19.1% | 0.1% | 0% | 5.1% | 0% | 7 |
| 81.7% | 77% | 17.3% | 0.1% | 0% | 5.6% | 0% | 8 |
| 84.3% | 79.3% | 14.7% | 0.1% | 0% | 5.9% | 0% | 9 |
| 85.9% | 80.5% | 13.2% | 0.1% | 0% | 6.2% | 0% | 10 |
| 88.5% | 82.8% | 10.8% | 0.1% | 0% | 6.2% | 0% | 11 |
| 89.6% | 83.6% | 9.8% | 0.1% | 0% | 6.5% | 0% | 12 |
Compiled 3 462 to 2 977 computations (14% saved)
Loading profile data...