
| Date: | Wednesday, April 16th, 2025 |
|---|---|
| Commit: | 5565a39e on main |
| Seed: | 2025106 |
| 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: | 999 626.3 MB |
Time bar (total: 13.5min)
| 2.7min | 2 144 638× | 0 | valid |
| 17.5s | 69 527× | 1 | valid |
| 7.2s | 64 681× | 0 | invalid |
| 1.3s | 5 999× | 2 | valid |
| 719.0ms | 1 205× | 5 | exit |
| 315.0ms | 1 705× | 1 | invalid |
| 202.0ms | 382× | 4 | exit |
| 182.0ms | 696× | 3 | valid |
| 3.0ms | 26× | 1 | exit |
| 1.0ms | 4× | 4 | valid |
ival-mult!: 38.9s (40% of total)ival-div!: 10.8s (11.1% of total)ival-add!: 9.7s (10% of total)ival-sub!: 9.6s (9.9% of total)ival-log: 8.6s (8.8% of total)adjust: 4.6s (4.8% of total)ival-sqrt: 4.6s (4.7% of total)ival-sin: 3.9s (4.1% of total)ival-cos: 3.0s (3.1% of total)ival-exp: 1.8s (1.9% of total)ival-fabs: 287.0ms (0.3% of total)ival-sinh: 280.0ms (0.3% of total)ival-cosh: 266.0ms (0.3% of total)ival-acos: 238.0ms (0.2% of total)ival-hypot: 213.0ms (0.2% of total)ival-tan: 212.0ms (0.2% of total)ival-tanh: 108.0ms (0.1% of total)| 2 241× | iter-limit |
| 853× | node-limit |
| 72× | unsound |
| 12× | saturated |
512 calls:
| 9.1s | x |
| 8.2s | y |
| 5.9s | z |
| 5.4s | (+.f64 (*.f64 x y) (*.f64 z t)) |
| 4.0s | t |
Compiled 36 898 to 55 797 computations (-51.2% saved)
| 147× | fuel |
| 122× | done |
Compiled 143 175 to 17 757 computations (87.6% saved)
8925 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 826.0ms | a | @ | 0 | ((+ (+ (+ x (* y z)) (* t a)) (* (* a z) b)) (+ (+ x (* y z)) (* t a)) (+ x (* y z)) x (* y z) y z (* t a) t a (* (* a z) b) (* a z) b) |
| 740.0ms | x | @ | inf | ((+ (* (log y) x) (- (* z (log (- 1 y))) t)) (log y) y x (- (* z (log (- 1 y))) t) (* z (log (- 1 y))) (* (+ (* (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) y) (neg z)) y) (+ (* (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) y) (neg z)) (+ (* (+ (* -1/4 (* z y)) (* -1/3 z)) y) (* -1/2 z)) (* (+ (* (+ (* 1/4 y) 1/3) y) 1/2) (neg z)) (+ (* (+ (* 1/4 y) 1/3) y) 1/2) (+ (* 1/4 y) 1/3) 1/4 1/3 1/2 (neg z) z t (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (+ (* -1/2 (* z y)) (neg z)) y) (* (log y) x)) (* (+ (* -1/2 z) (/ (neg z) y)) (* y y)) (* (neg y) z) (neg y) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (+ (* -1/2 (* z y)) (neg z)) y) (* (log y) x)) (* (+ (* -1/2 z) (/ (neg z) y)) (* y y)) (+ (* -1/2 z) (/ (neg z) y)) (/ (neg z) y) (* y y) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (* (log y) x) (- (+ (* x (log y)) (* z (log (- 1 y)))) t) (+ (* x (log y)) (* z (log (- 1 y)))) (+ (* (neg y) z) (* (log y) x)) (* (+ (* (* x (/ (neg (log y)) y)) -1) (neg z)) y) (+ (* (* x (/ (neg (log y)) y)) -1) (neg z)) (* x (/ (neg (log y)) y)) (/ (neg (log y)) y) (neg (log y)) -1) |
| 247.0ms | y | @ | -inf | ((+ (* (log x) x) (* (neg x) (log y))) (log x) x (* (neg x) (log y)) (neg x) (log y) y (* x (- (log (neg x)) (log (neg y)))) (- (log (neg x)) (log (neg y))) (log (neg x)) (log (neg y)) (neg y) (+ (* (log (neg x)) x) (* (exp (* (log (log (/ -1 y))) 1)) x)) (* (exp (* (log (log (/ -1 y))) 1)) x) (exp (* (log (log (/ -1 y))) 1)) (* (log (log (/ -1 y))) 1) (log (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 1 (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y)))) (/ (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (+ (* (log (/ -1 x)) -1) (log (neg y)))) (- (pow (log (neg x)) 2) (pow (log (neg y)) 2)) (pow (log (neg x)) 2) 2 (pow (log (neg y)) 2) (+ (* (log (/ -1 x)) -1) (log (neg y))) (log (/ -1 x)) (/ -1 x) (* x (/ (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (log (* x y)) (log (* x y))))) (/ (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (log (* x y)) (log (* x y)))) (- (* (pow (log x) 2) (log (* x y))) (* (log (* x y)) (pow (log y) 2))) (* (pow (log x) 2) (log (* x y))) (pow (log x) 2) (log (* x y)) (* x y) (* (log (* x y)) (pow (log y) 2)) (pow (log y) 2) (* (log (* x y)) (log (* x y)))) |
| 211.0ms | x | @ | 0 | ((* (neg x) (log (/ y x))) (neg x) x (log (/ y x)) (/ y x) y (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (+ (* (log (neg x)) x) (* (neg (neg (log (/ -1 y)))) x)) (log (neg x)) (* (neg (neg (log (/ -1 y)))) x) (neg (neg (log (/ -1 y)))) (neg (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 (* x (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (log (/ -1 y)) 2) (log (* x y)))) (/ (pow (log (neg x)) 2) (log (* x y))) (pow (log (neg x)) 2) 2 (log (* x y)) (* x y) (/ (pow (log (/ -1 y)) 2) (log (* x y))) (pow (log (/ -1 y)) 2) (/ (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (* (log (/ -1 y)) (neg (log (* y x)))) (pow (log (neg x)) 2))) (* (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) x) (+ (pow (log (neg x)) 3) (pow (log (/ -1 y)) 3)) (pow (log (neg x)) 3) 3 (pow (log (/ -1 y)) 3) (+ (* (log (/ -1 y)) (neg (log (* y x)))) (pow (log (neg x)) 2)) (neg (log (* y x))) (log (* y x)) (* y x)) |
| 205.0ms | x | @ | 0 | ((- (* x (log (/ x y))) z) (* x (log (/ x y))) x (log (/ x y)) (/ x y) y z) |
Compiled 8 533 755 to 986 104 computations (88.4% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
log.f64 | #f | sensitivity | 1571 | 0 |
/.f64 | #f | o/n | 1171 | 0 |
sqrt.f64 | #f | oflow-rescue | 735 | 0 |
-.f64 | #f | cancellation | 596 | 9 |
/.f64 | #f | o/o | 541 | 0 |
*.f64 | #f | n*o | 506 | 0 |
+.f64 | #f | nan-rescue | 498 | 0 |
-.f64 | #f | nan-rescue | 401 | 0 |
+.f64 | #f | cancellation | 377 | 0 |
cos.f64 | #f | sensitivity | 352 | 3 |
/.f64 | #f | n/o | 328 | 0 |
sin.f64 | #f | sensitivity | 230 | 0 |
/.f64 | #f | u/n | 225 | 0 |
*.f64 | #f | n*u | 172 | 0 |
/.f64 | #f | n/u | 156 | 0 |
cos.f64 | #f | oflow-rescue | 117 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | sensitivity | 108 | 0 |
/.f64 | #f | u/u | 103 | 0 |
log.f64 | #f | oflow-rescue | 83 | 0 |
log.f64 | #f | uflow-rescue | 59 | 0 |
sqrt.f64 | #f | uflow-rescue | 43 | 0 |
exp.f64 | #f | sensitivity | 28 | 5 |
sin.f64 | (sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 25 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 25 | |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 25 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 25 | |
*.f64 | #f | o*u | 23 | 0 |
*.f64 | #f | u*o | 5 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 5887 | 192 |
| - | 1728 | 61057 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5887 | 1 | 191 |
| - | 1728 | 15 | 61042 |
| number | freq |
|---|---|
| 0 | 61249 |
| 1 | 6842 |
| 2 | 706 |
| 3 | 49 |
| 4 | 15 |
| 5 | 1 |
| 6 | 2 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 136 | 0 | 0 |
| - | 2 | 0 | 131 |
| 10.4s | 130 332× | 0 | valid |
| 1.7s | 1 328× | 2 | valid |
| 1.6s | 5 970× | 1 | valid |
| 62.0ms | 98× | 3 | valid |
Compiled 24 442 to 8 402 computations (65.6% saved)
ival-mult!: 2.4s (36.4% of total)ival-log: 1.5s (22.2% of total)ival-sub!: 539.0ms (8.2% of total)ival-div!: 535.0ms (8.1% of total)ival-add!: 441.0ms (6.7% of total)adjust: 349.0ms (5.3% of total)ival-sqrt: 229.0ms (3.5% of total)ival-sin: 225.0ms (3.4% of total)ival-cos: 211.0ms (3.2% of total)ival-exp: 101.0ms (1.5% of total)ival-hypot: 28.0ms (0.4% of total)ival-tan: 17.0ms (0.3% of total)ival-fabs: 16.0ms (0.2% of total)ival-cosh: 13.0ms (0.2% of total)ival-sinh: 10.0ms (0.2% of total)ival-acos: 9.0ms (0.1% of total)ival-tanh: 7.0ms (0.1% of total)| 174× | node-limit |
| 95× | saturated |
Compiled 479 870 to 129 956 computations (72.9% saved)
| 1 637× | binary-search |
| 969× | left-value |
| 1 604× | narrow-enough |
| 33× | predicate-same |
| 12.8s | 132 619× | 0 | valid |
| 943.0ms | 4 095× | 1 | valid |
| 199.0ms | 2 510× | 0 | invalid |
| 23.0ms | 92× | 1 | invalid |
| 17.0ms | 132× | 2 | valid |
| 3.0ms | 18× | 3 | valid |
Compiled 859 359 to 619 151 computations (28% saved)
ival-mult!: 3.3s (40.5% of total)ival-sub!: 2.1s (25.3% of total)ival-add!: 692.0ms (8.4% of total)ival-div!: 538.0ms (6.6% of total)ival-log: 389.0ms (4.7% of total)ival-cos: 364.0ms (4.4% of total)ival-sin: 309.0ms (3.8% of total)adjust: 207.0ms (2.5% of total)ival-exp: 145.0ms (1.8% of total)ival-sqrt: 119.0ms (1.5% of total)ival-tanh: 13.0ms (0.2% of total)ival-fabs: 9.0ms (0.1% of total)ival-sinh: 9.0ms (0.1% of total)ival-cosh: 6.0ms (0.1% of total)Compiled 783 911 to 426 024 computations (45.7% saved)
| 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...