
| Date: | Wednesday, January 15th, 2025 |
|---|---|
| Commit: | d270acbc on main |
| Seed: | 2025015 |
| 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 615 150.0 MB |
Time bar (total: 24.6min)
| 3.8min | 2 144 715× | 0 | valid |
| 25.2s | 69 517× | 1 | valid |
| 10.9s | 64 308× | 0 | invalid |
| 4.7s | 5 938× | 2 | valid |
| 1.3s | 1 547× | 5 | exit |
| 621.0ms | 1 881× | 1 | invalid |
| 228.0ms | 693× | 3 | valid |
| 0.0ms | 1× | 4 | valid |
ival-mult: 57.8s (34.9% of total)ival-sub: 23.1s (13.9% of total)ival-add: 20.7s (12.5% of total)ival-div: 20.6s (12.4% of total)ival-log: 9.2s (5.6% of total)adjust: 7.2s (4.3% of total)const: 6.4s (3.9% of total)ival-sqrt: 5.3s (3.2% of total)ival-sin: 4.7s (2.8% of total)ival-cos: 3.2s (1.9% of total)ival-exp: 1.9s (1.2% of total)ival-true: 1.6s (1% of total)exact: 1.1s (0.7% of total)ival-assert: 876.0ms (0.5% of total)ival-tan: 381.0ms (0.2% of total)ival-cosh: 369.0ms (0.2% of total)ival-fabs: 326.0ms (0.2% of total)ival-hypot: 307.0ms (0.2% of total)ival-sinh: 256.0ms (0.2% of total)ival-acos: 250.0ms (0.2% of total)ival-tanh: 97.0ms (0.1% of total)| 2 860× | iter limit |
| 1 858× | node limit |
| 302× | saturated |
| 6× | unsound |
| 2 741× | iter limit |
| 750× | node limit |
| 185× | unsound |
| 13× | saturated |
| 59.4s | 221 213× | 0 | valid |
| 11.5s | 11 582× | 1 | valid |
| 6.9s | 3 296× | 2 | valid |
| 2.1s | 4 191× | 0 | invalid |
| 1.3s | 554× | 5 | exit |
| 551.0ms | 291× | 3 | valid |
| 116.0ms | 275× | 0 | exit |
| 6.0ms | 6× | 4 | valid |
Compiled 145 950 to 23 187 computations (84.1% saved)
ival-mult: 18.8s (33.9% of total)ival-div: 7.9s (14.3% of total)ival-add: 7.4s (13.3% of total)ival-sub: 4.1s (7.4% of total)adjust: 3.7s (6.7% of total)const: 3.0s (5.3% of total)ival-sin: 2.7s (4.8% of total)ival-log: 1.8s (3.2% of total)ival-pow: 1.3s (2.3% of total)ival-cos: 1.2s (2.1% of total)ival-neg: 1.1s (2% of total)ival-sqrt: 789.0ms (1.4% of total)ival-pow2: 419.0ms (0.8% of total)ival-exp: 256.0ms (0.5% of total)exact: 234.0ms (0.4% of total)ival-true: 183.0ms (0.3% of total)ival-tan: 134.0ms (0.2% of total)ival-hypot: 103.0ms (0.2% of total)ival-assert: 99.0ms (0.2% of total)ival-log1p: 75.0ms (0.1% of total)ival-fabs: 49.0ms (0.1% of total)ival-tanh: 44.0ms (0.1% of total)ival-sinu: 38.0ms (0.1% of total)ival-cosh: 25.0ms (0% of total)ival-expm1: 25.0ms (0% of total)ival-pi: 22.0ms (0% of total)ival-sinh: 21.0ms (0% of total)ival-acos: 19.0ms (0% of total)ival-cosu: 10.0ms (0% of total)ival-asin: 7.0ms (0% of total)ival->: 1.0ms (0% of total)ival-then: 0.0ms (0% of total)| 157× | fuel |
| 112× | done |
Compiled 143 568 to 19 235 computations (86.6% saved)
509 calls:
| 12.7s | x |
| 9.6s | y |
| 7.5s | z |
| 4.3s | t |
| 3.3s | a |
Compiled 38 366 to 58 018 computations (-51.2% saved)
| 538× | iter limit |
| 341× | node limit |
| 197× | saturated |
Compiled 321 522 to 60 626 computations (81.1% saved)
Compiled 10 979 100 to 1 063 782 computations (90.3% saved)
9033 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 1.6s | t | @ | 0 | ((+ (* (* (* (/ x (+ (* x (log y)) y)) x) (log y)) (log y)) (- (* (/ y (+ (* x (log y)) y)) (neg y)) (- z (log t)))) (- (* (/ y (+ (* x (log y)) y)) (neg y)) (- z (log t))) (* (* (/ x (+ (* x (log y)) y)) x) (log y)) (* (/ x (+ (* x (log y)) y)) x) (+ (- (- (* x (log y)) y) z) (log t)) (* (- (/ (- (+ (* (log y) x) (log t)) y) z) 1) z) (- (/ (- (+ (* (log y) x) (log t)) y) z) 1) (/ (neg y) z) (+ (- (- (* x (log y)) y) z) (log t)) (- (log (* (pow y x) t)) z) (log (* (pow y x) t)) (* (pow y x) t) (- (* (/ x y) (log y)) 1) (+ (- (- (* x (log y)) y) z) (log t)) (- (- (* x (log y)) y) z) (- (* x (log y)) y) (/ (+ (* (neg y) y) (* (* (pow (log y) 2) x) x)) (+ (* (log y) x) y)) (+ (- (+ (* (pow (log y) 2) (/ (* x x) (+ (* (log y) x) y))) (/ (* (neg y) y) (+ (* (log y) x) y))) z) (log t)) (- (+ (* (pow (log y) 2) (/ (* x x) (+ (* (log y) x) y))) (/ (* (neg y) y) (+ (* (log y) x) y))) z) (+ (* (neg y) y) (* (* (pow (log y) 2) x) x)) (/ y (+ (* x (log y)) y)) (+ (* x (log y)) y) (neg y) (* (/ x y) (log y)) (* (- (* (/ x y) (log y)) 1) y) (pow (log y) 2) (* (pow (log y) 2) x)) |
| 304.0ms | x | @ | 0 | ((* (log (* y x)) (/ (log (/ x y)) (log (* y x)))) (* x (* (log (* y x)) (/ (log (/ x y)) (log (* y x))))) (log (* y x)) (* y x) (- (log x) (log y)) (* x (- (log x) (log y))) (log x) (log y) (exp (log x)) (exp (log y)) (* x (log (/ (exp (log x)) (exp (log y))))) (log (/ (exp (log x)) (exp (log y)))) (* x (/ (- (pow (log x) 3) (pow (log y) 3)) (+ (* (log (* y x)) (log y)) (pow (log x) 2)))) (/ (- (pow (log x) 3) (pow (log y) 3)) (+ (* (log (* y x)) (log y)) (pow (log x) 2))) (- (pow (log x) 3) (pow (log y) 3)) (pow (log x) 3) (* (neg x) (neg y)) (/ (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (+ (* (log (neg y)) (log (* (neg x) (neg y)))) (pow (log (neg x)) 2))) (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) (log (/ x y)) (log (neg x)) (log (neg y)) (log (* (neg x) (neg y))) (neg x)) |
| 215.0ms | x | @ | 0 | ((+ (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (* y i)) (+ (+ (+ (+ (* x (log y)) z) t) a) (* (- b 1/2) (log c))) (+ (* x (log y)) z) (+ (+ (+ (* x (log y)) z) t) a) (* x (log y)) (* (- b 1/2) (log c)) (+ (+ (* x (log y)) z) t)) |
| 183.0ms | x | @ | 0 | ((/ (* (* (log (* (neg x) (neg y))) (log (/ x y))) x) (log (* (neg x) (neg y)))) (* (neg x) (neg y)) (* (* (log (* (neg x) (neg y))) (log (/ x y))) x) (* (log (* (neg x) (neg y))) (log (/ x y))) (* (/ x 2) (log (pow (/ x y) 2))) (/ x 2) (log (pow (/ x y) 2)) (pow (/ x y) 2) (* (* x (/ (- (log (neg x)) (log (neg y))) (log (* x y)))) (log (* x y))) (* x (/ (- (log (neg x)) (log (neg y))) (log (* x y)))) (/ (- (log (neg x)) (log (neg y))) (log (* x y))) (- (log (neg x)) (log (neg y))) (* (- (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)) (pow (log x) 3) (log x) (* (+ (* (log (* (neg y) (neg x))) (log (neg y))) (pow (log (neg x)) 2)) (* (log (/ x y)) (/ x (+ (* (log (* (neg y) (neg x))) (log (neg y))) (pow (log (neg x)) 2))))) (* (neg y) (neg x)) (+ (* (log (* (neg y) (neg x))) (log (neg y))) (pow (log (neg x)) 2)) (log (* (neg y) (neg x))) (log (* (neg x) (neg y))) (log (/ x y)) (neg x) (neg y) (/ x y) (log (neg x)) (log (neg y)) (log (* x y)) (log y) (log (* y x)) (* y x)) |
| 166.0ms | z | @ | -inf | ((+ 1 (/ (* 4 (- (+ x (* y 3/4)) z)) y)) (/ (* 4 (- (+ x (* y 3/4)) z)) y) (+ x (* y 3/4)) (* 4 (- (+ x (* y 3/4)) z)) (- (+ x (* y 3/4)) z)) |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
log.f64 | #f | sensitivity | 1587 | 1 |
/.f64 | #f | o/n | 1199 | 0 |
sqrt.f64 | #f | oflow-rescue | 772 | 0 |
-.f64 | #f | cancellation | 612 | 11 |
/.f64 | #f | o/o | 606 | 0 |
*.f64 | #f | n*o | 527 | 0 |
-.f64 | #f | nan-rescue | 447 | 0 |
+.f64 | #f | nan-rescue | 430 | 0 |
cos.f64 | #f | sensitivity | 361 | 0 |
/.f64 | #f | n/o | 347 | 0 |
+.f64 | #f | cancellation | 332 | 3 |
/.f64 | #f | u/n | 265 | 0 |
sin.f64 | #f | sensitivity | 216 | 0 |
*.f64 | #f | n*u | 203 | 0 |
cos.f64 | #f | oflow-rescue | 141 | 0 |
/.f64 | #f | n/u | 124 | 0 |
log.f64 | #f | oflow-rescue | 102 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | sensitivity | 91 | 0 |
/.f64 | #f | u/u | 90 | 0 |
log.f64 | #f | uflow-rescue | 77 | 0 |
sqrt.f64 | #f | uflow-rescue | 65 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 42 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 42 | |
sin.f64 | (sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 42 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 42 | |
*.f64 | #f | o*u | 35 | 0 |
exp.f64 | #f | sensitivity | 28 | 4 |
*.f64 | #f | u*o | 3 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 6093 | 170 |
| - | 1755 | 60846 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 6093 | 2 | 168 |
| - | 1755 | 17 | 60829 |
| number | freq |
|---|---|
| 0 | 61016 |
| 1 | 7055 |
| 2 | 714 |
| 3 | 60 |
| 4 | 15 |
| 5 | 3 |
| 6 | 1 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 134 | 0 | 0 |
| - | 1 | 2 | 132 |
| 16.9s | 130 290× | 0 | valid |
| 3.0s | 6 036× | 1 | valid |
| 888.0ms | 1 312× | 2 | valid |
| 31.0ms | 88× | 3 | valid |
| 1.0ms | 2× | 5 | exit |
Compiled 24 442 to 8 402 computations (65.6% saved)
ival-mult: 3.6s (33.5% of total)ival-add: 1.7s (16.5% of total)ival-sub: 1.2s (11% of total)ival-div: 1.2s (11% of total)ival-log: 768.0ms (7.2% of total)adjust: 552.0ms (5.2% of total)const: 353.0ms (3.3% of total)ival-cos: 309.0ms (2.9% of total)ival-sin: 240.0ms (2.3% of total)ival-sqrt: 239.0ms (2.3% of total)ival-exp: 145.0ms (1.4% of total)ival-true: 109.0ms (1% of total)exact: 63.0ms (0.6% of total)ival-assert: 54.0ms (0.5% of total)ival-fabs: 53.0ms (0.5% of total)ival-sinh: 31.0ms (0.3% of total)ival-tan: 23.0ms (0.2% of total)ival-hypot: 16.0ms (0.2% of total)ival-cosh: 12.0ms (0.1% of total)ival-tanh: 7.0ms (0.1% of total)ival-acos: 4.0ms (0% of total)| 1 622× | binary-search |
| 1 043× | left-value |
| 1 590× | narrow-enough |
| 32× | predicate-same |
| 20.0s | 128 751× | 0 | valid |
| 1.1s | 3 437× | 1 | valid |
| 205.0ms | 1 978× | 0 | invalid |
| 35.0ms | 167× | 2 | valid |
| 3.0ms | 13× | 3 | valid |
Compiled 946 521 to 675 731 computations (28.6% saved)
ival-mult: 5.4s (35.9% of total)ival-add: 3.8s (25.3% of total)ival-sub: 2.4s (16.1% of total)ival-div: 795.0ms (5.3% of total)const: 667.0ms (4.5% of total)ival-log: 550.0ms (3.7% of total)ival-sin: 418.0ms (2.8% of total)adjust: 322.0ms (2.2% of total)ival-cos: 244.0ms (1.6% of total)ival-true: 94.0ms (0.6% of total)ival-exp: 64.0ms (0.4% of total)ival-sqrt: 62.0ms (0.4% of total)ival-assert: 52.0ms (0.3% of total)exact: 51.0ms (0.3% of total)ival-cosh: 42.0ms (0.3% of total)ival-sinh: 14.0ms (0.1% of total)ival-tanh: 8.0ms (0.1% of total)ival-fabs: 7.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)
Compiled 793 062 to 427 616 computations (46.1% saved)
Loading profile data...