
| Date: | Wednesday, January 22nd, 2025 |
|---|---|
| Commit: | 68e0d036 on no-localize |
| Seed: | 2025022 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs default |
| Memory: | 1 510 137.9 MB |
Time bar (total: 21.3min)
| 3.8min | 2 144 465× | 0 | valid |
| 28.5s | 69 818× | 1 | valid |
| 10.2s | 63 848× | 0 | invalid |
| 3.0s | 5 951× | 2 | valid |
| 1.5s | 1 542× | 5 | exit |
| 482.0ms | 1 829× | 1 | invalid |
| 264.0ms | 630× | 3 | valid |
ival-mult: 59.0s (34% of total)ival-add: 22.9s (13.2% of total)ival-div: 22.1s (12.8% of total)ival-sub: 20.8s (12% of total)ival-log: 11.1s (6.4% of total)adjust: 10.1s (5.8% of total)const: 6.4s (3.7% of total)ival-sqrt: 5.9s (3.4% of total)ival-sin: 4.3s (2.5% of total)ival-cos: 3.5s (2% of total)ival-exp: 2.0s (1.1% of total)ival-true: 1.6s (0.9% of total)exact: 1.1s (0.6% of total)ival-assert: 880.0ms (0.5% of total)ival-acos: 351.0ms (0.2% of total)ival-cosh: 295.0ms (0.2% of total)ival-tan: 241.0ms (0.1% of total)ival-fabs: 236.0ms (0.1% of total)ival-sinh: 228.0ms (0.1% of total)ival-hypot: 165.0ms (0.1% of total)ival-tanh: 100.0ms (0.1% of total)| 1 126× | node limit |
| 970× | iter limit |
| 79× | saturated |
| 3× | unsound |
| 2 731× | iter limit |
| 747× | node limit |
| 185× | unsound |
| 10× | saturated |
| 164× | fuel |
| 105× | done |
Compiled 157 520 to 19 825 computations (87.4% saved)
511 calls:
| 13.4s | y |
| 12.0s | z |
| 11.5s | x |
| 4.7s | t |
| 2.8s | a |
Compiled 38 180 to 58 414 computations (-53% saved)
Compiled 13 843 419 to 1 306 720 computations (90.6% saved)
| 538× | iter limit |
| 341× | node limit |
| 197× | saturated |
Compiled 352 500 to 63 598 computations (82% saved)
9003 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 4.3s | x | @ | 0 | ((* x (* (log (* y x)) (/ (log (/ x y)) (log (* y x))))) x (* (log (* y x)) (/ (log (/ x y)) (log (* y x)))) (log (* y x)) (* y x) y (/ (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) (* x (- (log x) (log y))) (- (log x) (log y)) (log x) (log y) (* (- (pow (log x) 2) (pow (log y) 2)) (/ x (log (* y x)))) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) 2 (pow (log y) 2) (/ x (log (* y x))) (/ (* (- (pow (log x) 3) (pow (log y) 3)) x) (+ (* (log (* y x)) (log y)) (pow (log x) 2))) (* (- (pow (log x) 3) (pow (log y) 3)) x) (- (pow (log x) 3) (pow (log y) 3)) (pow (log x) 3) 3 (pow (log y) 3) (+ (* (log (* y x)) (log y)) (pow (log x) 2)) (* x (/ (- (pow (log x) 6) (pow (log y) 6)) (* (+ (pow (log y) 3) (pow (log x) 3)) (+ (* (log (* y x)) (log y)) (pow (log x) 2))))) (/ (- (pow (log x) 6) (pow (log y) 6)) (* (+ (pow (log y) 3) (pow (log x) 3)) (+ (* (log (* y x)) (log y)) (pow (log x) 2)))) (- (pow (log x) 6) (pow (log y) 6)) (pow (log x) 6) 6 (pow (log y) 6) (* (+ (pow (log y) 3) (pow (log x) 3)) (+ (* (log (* y x)) (log y)) (pow (log x) 2))) (+ (pow (log y) 3) (pow (log x) 3))) |
| 2.7s | z | @ | -inf | ((+ (* (+ (* x y) z) y) t) (/ (* (- (pow (* x y) 2) (* z z)) y) (- (* x y) z)) (* (- (pow (* x y) 2) (* z z)) y) (- (pow (* x y) 2) (* z z)) (pow (* x y) 2) (* x y) x y 2 (* z z) z (- (* x y) z) (+ (* (+ (* y x) z) y) t) (* (* x y) y) (+ (* (+ (* (pow (* y x) 3/2) (/ (pow (* y x) 3/2) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) (/ (pow z 3) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) y) t) (* (+ (* (pow (* y x) 3/2) (/ (pow (* y x) 3/2) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) (/ (pow z 3) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) y) (+ (* (pow (* y x) 3/2) (/ (pow (* y x) 3/2) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) (/ (pow z 3) (+ (* (- z (* y x)) z) (pow (* y x) 2)))) (* (+ (* x (/ y z)) 1) z) (+ (* x (/ y z)) 1) (/ y z) 1 t (+ (* (* y y) x) (+ (* z y) t)) (* y y) (+ (* z y) t)) |
| 1.7s | x | @ | 0 | ((+ (- (- (* x (log y)) y) z) (log t)) (- (- (* x (log y)) y) z) (- (* x (log y)) y) (* x (log y)) x (log y) y z (log t) t) |
| 442.0ms | t | @ | -inf | ((+ (* (/ (- y x) (- a t)) (- z t)) x) (/ (- y x) (- a t)) (- y x) y x (- a t) a t (- z t) z (+ x (/ (* (- y x) (- z t)) (- a t))) (+ x (/ (* (- y x) (- z t)) (- a t))) (/ (* (- y x) (- z t)) (- a t)) (/ (* (- y x) z) a) (* (- y x) z) (+ x (/ (* (- y x) (- z t)) (- a t))) (/ (* (- y x) (- z t)) (- a t)) (* (- y x) (- z t)) (- y x) (neg x) (+ x (/ (* (- y x) (- z t)) (- a t))) (- y (/ (+ (* (* (/ (- y x) t) (- z a)) a) (* (- z a) (- y x))) t)) (/ (+ (* (* (/ (- y x) t) (- z a)) a) (* (- z a) (- y x))) t) (+ (* (* (/ (- y x) t) (- z a)) a) (* (- z a) (- y x))) (* (/ (- y x) t) (- z a)) (/ (- y x) t) (- z a) (* (- z a) (- y x))) |
| 375.0ms | x | @ | inf | ((* (* (log (/ x y)) (log (* y x))) (/ x (log (* y x)))) (* (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) x y (log (* y x)) (* y x) (/ x (log (* y x))) (log (pow (/ x y) x)) (pow (/ x y) x) 1 (* x (* (log (* y x)) (/ (log (/ x y)) (+ (log y) (log x))))) (* (log (* y x)) (/ (log (/ x y)) (+ (log y) (log x)))) (/ (log (/ x y)) (+ (log y) (log x))) (+ (log y) (log x)) (log y) (log x) (* x (* (log (* y x)) (/ (log (/ x y)) (log (* y x))))) (* (log (* y x)) (/ (log (/ x y)) (log (* y x)))) (/ (log (/ x y)) (log (* y x))) (/ (+ (log (neg x)) (neg (log (neg y)))) (- (log (neg x)) (log (/ -1 y)))) (+ (log (neg x)) (neg (log (neg y)))) (log (neg x)) (neg x) (neg (log (neg y))) (log (neg y)) (neg y) (- (log (neg x)) (log (/ -1 y))) (log (/ -1 y)) (/ -1 y) -1 (* (- (pow (log x) 2) (pow (log y) 2)) (/ x (+ (* (pow (log y) 1/2) (pow (log y) 1/2)) (log x)))) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) 2 (pow (log y) 2) (/ x (+ (* (pow (log y) 1/2) (pow (log y) 1/2)) (log x))) (+ (* (pow (log y) 1/2) (pow (log y) 1/2)) (log x)) (pow (log y) 1/2) 1/2) |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
log.f64 | #f | sensitivity | 1562 | 4 |
/.f64 | #f | o/n | 1190 | 0 |
sqrt.f64 | #f | oflow-rescue | 807 | 0 |
-.f64 | #f | cancellation | 579 | 7 |
/.f64 | #f | o/o | 569 | 0 |
*.f64 | #f | n*o | 508 | 0 |
-.f64 | #f | nan-rescue | 473 | 0 |
+.f64 | #f | nan-rescue | 466 | 0 |
cos.f64 | #f | sensitivity | 364 | 1 |
/.f64 | #f | n/o | 330 | 0 |
+.f64 | #f | cancellation | 322 | 1 |
/.f64 | #f | u/n | 237 | 0 |
sin.f64 | #f | sensitivity | 227 | 0 |
*.f64 | #f | n*u | 204 | 0 |
/.f64 | #f | n/u | 160 | 0 |
cos.f64 | #f | oflow-rescue | 128 | 0 |
/.f64 | #f | u/u | 86 | 0 |
log.f64 | #f | uflow-rescue | 85 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | sensitivity | 85 | 0 |
log.f64 | #f | oflow-rescue | 76 | 0 |
sqrt.f64 | #f | uflow-rescue | 45 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 38 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 38 | |
sin.f64 | (sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 38 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 38 | |
exp.f64 | #f | sensitivity | 26 | 3 |
*.f64 | #f | o*u | 24 | 0 |
*.f64 | #f | u*o | 2 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 6028 | 180 |
| - | 1699 | 60957 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 6028 | 3 | 177 |
| - | 1699 | 15 | 60942 |
| number | freq |
|---|---|
| 0 | 61137 |
| 1 | 6929 |
| 2 | 714 |
| 3 | 65 |
| 4 | 16 |
| 5 | 3 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 137 | 0 | 0 |
| - | 1 | 1 | 130 |
| 13.9s | 130 390× | 0 | valid |
| 2.5s | 6 002× | 1 | valid |
| 745.0ms | 1 260× | 2 | valid |
| 30.0ms | 72× | 3 | valid |
| 1.0ms | 2× | 4 | valid |
| 1.0ms | 2× | 5 | exit |
Compiled 24 442 to 8 402 computations (65.6% saved)
ival-mult: 3.1s (31.6% of total)ival-sub: 1.3s (13.4% of total)ival-div: 1.2s (12% of total)ival-add: 1.1s (11.6% of total)ival-log: 933.0ms (9.5% of total)adjust: 517.0ms (5.3% of total)const: 357.0ms (3.7% of total)ival-sin: 347.0ms (3.6% of total)ival-cos: 265.0ms (2.7% of total)ival-sqrt: 157.0ms (1.6% of total)ival-exp: 127.0ms (1.3% of total)ival-true: 114.0ms (1.2% of total)exact: 66.0ms (0.7% of total)ival-assert: 55.0ms (0.6% of total)ival-fabs: 38.0ms (0.4% of total)ival-tan: 34.0ms (0.3% of total)ival-cosh: 20.0ms (0.2% of total)ival-sinh: 20.0ms (0.2% of total)ival-hypot: 9.0ms (0.1% of total)ival-tanh: 6.0ms (0.1% of total)ival-acos: 5.0ms (0.1% of total)| 1 911× | binary-search |
| 1 128× | left-value |
| 1 878× | narrow-enough |
| 33× | predicate-same |
| 21.6s | 151 019× | 0 | valid |
| 1.3s | 4 250× | 1 | valid |
| 278.0ms | 3 056× | 0 | invalid |
| 48.0ms | 154× | 2 | valid |
| 31.0ms | 17× | 3 | valid |
| 31.0ms | 88× | 1 | invalid |
Compiled 1 101 469 to 784 356 computations (28.8% saved)
ival-mult: 6.8s (44.5% of total)ival-sub: 3.0s (19.4% of total)ival-add: 1.7s (11.4% of total)ival-div: 996.0ms (6.5% of total)const: 659.0ms (4.3% of total)ival-log: 556.0ms (3.6% of total)ival-sin: 368.0ms (2.4% of total)adjust: 310.0ms (2% of total)ival-cos: 308.0ms (2% of total)ival-sqrt: 154.0ms (1% of total)ival-exp: 116.0ms (0.8% of total)ival-true: 114.0ms (0.7% of total)exact: 67.0ms (0.4% of total)ival-assert: 63.0ms (0.4% of total)ival-cosh: 13.0ms (0.1% of total)ival-sinh: 11.0ms (0.1% of total)ival-fabs: 9.0ms (0.1% of total)ival-tanh: 8.0ms (0.1% of total)Compiled 839 280 to 453 389 computations (46% 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...