
| Date: | Wednesday, March 26th, 2025 |
|---|---|
| Commit: | a931ba94 on hardware-accelerators |
| Seed: | 2025085 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs default |
| Memory: | 987 657.9 MB |
Time bar (total: 15.2min)
| 2.6min | 2 144 737× | 0 | valid |
| 18.8s | 69 547× | 1 | valid |
| 9.6s | 63 484× | 0 | invalid |
| 1.9s | 5 919× | 2 | valid |
| 875.0ms | 1 235× | 5 | exit |
| 500.0ms | 1 852× | 1 | invalid |
| 261.0ms | 381× | 4 | exit |
| 180.0ms | 660× | 3 | valid |
| 3.0ms | 24× | 1 | exit |
| 0.0ms | 1× | 4 | valid |
ival-mult!: 37.5s (38.2% of total)ival-div!: 11.1s (11.3% of total)ival-sub!: 11.0s (11.3% of total)ival-add!: 9.5s (9.7% of total)ival-log: 9.0s (9.2% of total)ival-sqrt: 4.7s (4.8% of total)ival-sin: 4.2s (4.3% of total)adjust: 3.8s (3.9% of total)ival-cos: 3.4s (3.4% of total)ival-exp: 2.1s (2.1% of total)ival-cosh: 420.0ms (0.4% of total)ival-hypot: 291.0ms (0.3% of total)ival-tan: 276.0ms (0.3% of total)ival-fabs: 263.0ms (0.3% of total)ival-acos: 259.0ms (0.3% of total)ival-sinh: 187.0ms (0.2% of total)ival-tanh: 132.0ms (0.1% of total)const: 0.0ms (0% of total)| 2 225× | iter limit |
| 851× | node limit |
| 69× | unsound |
| 13× | saturated |
| 538× | iter limit |
| 341× | node limit |
| 197× | saturated |
Compiled 314 164 to 56 390 computations (82.1% saved)
| 148× | fuel |
| 121× | done |
Compiled 143 073 to 19 157 computations (86.6% saved)
512 calls:
| 9.7s | x |
| 8.9s | y |
| 8.0s | z |
| 4.2s | t |
| 2.9s | a |
Compiled 37 067 to 55 614 computations (-50% saved)
8880 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 3.4s | x | @ | -inf | ((- (- (* x (log y)) z) y) (- (* x (log y)) z) (* (+ (* (/ (log y) z) x) -1) z) (+ (* (/ (log y) z) x) -1) (/ (log y) z) (log y) y z x -1 (- (- (* x (+ (log (pow y 1/2)) (log (pow y 1/2)))) z) y) (neg z) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (neg z) x) (- (- (* x (log y)) z) y) (* (log y) x) (- (- (* x (log y)) z) y) (* (- (log y) (/ (+ z y) x)) x) (- (log y) (/ (+ z y) x)) (/ (+ z y) x) (+ z y)) |
| 697.0ms | y | @ | 0 | ((/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (* (/ (- 1 y) z) x) (/ (- 1 y) z) (/ (neg y) z) (neg y) y z x (/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (/ (* (- 1 (* y y)) x) (* (+ 1 y) z)) (* (- 1 (* y y)) x) (- 1 (* y y)) 1 (* y y) (* (+ 1 y) z) (+ 1 y) (/ (+ x (* y (- z x))) z) (+ (* (- 1 y) (/ x z)) y) (/ (* (- 1 (pow y 3)) x) (* (+ 1 (+ (* y y) (* 1 y))) z)) (* (- 1 (pow y 3)) x) (- 1 (pow y 3)) (pow y 3) 3 (* (+ 1 (+ (* y y) (* 1 y))) z) (+ 1 (+ (* y y) (* 1 y))) (+ (* y y) (* 1 y)) (* 1 y) (/ (+ x (* y (- z x))) z) (+ x (* y (- z x))) (+ (* (neg y) x) x)) |
| 297.0ms | y | @ | -inf | ((* x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))))) x (/ (- 0 (pow (log (/ y x)) 3)) (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))))) (- 0 (pow (log (/ y x)) 3)) 0 (pow (log (/ y x)) 3) (log (/ y x)) (/ y x) y 3 (+ 0 (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x))))) (+ (* (log (/ y x)) (log (/ y x))) (* 0 (log (/ y x)))) (* 0 (log (/ y x))) (* (- (log (neg x)) (log (neg y))) x) (- (log (neg x)) (log (neg y))) (log (neg x)) (neg x) (log (neg y)) (neg y) (+ (* (log (neg x)) x) (* (/ 1 (pow (log (/ -1 y)) -1)) x)) (* (/ 1 (pow (log (/ -1 y)) -1)) x) (/ 1 (pow (log (/ -1 y)) -1)) 1 (pow (log (/ -1 y)) -1) (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) (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 (neg x)) 2) (log (* x y))) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y))))) (- (/ (pow (log (neg x)) 2) (log (* x y))) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y)))) (/ (pow (log (neg x)) 2) (log (* x y))) (log (* x y)) (* x y) (/ (pow (exp (log (log (/ -1 y)))) 2) (log (* x y))) (pow (exp (log (log (/ -1 y)))) 2) (exp (log (log (/ -1 y)))) (log (log (/ -1 y)))) |
| 272.0ms | x | @ | 0 | ((* (/ (neg (pow (log (/ y x)) 3)) (- (pow (log (/ y x)) 2) 0)) x) (/ (neg (pow (log (/ y x)) 3)) (- (pow (log (/ y x)) 2) 0)) (neg (pow (log (/ y x)) 3)) (pow (log (/ y x)) 3) (log (/ y x)) (/ y x) y x 3 (- (pow (log (/ y x)) 2) 0) (pow (log (/ y x)) 2) 2 0 (- (* (log x) x) (* (log y) x)) (* (log x) x) (log x) (* (log y) x) (log y) (+ (* (log (neg x)) x) (/ (* 1 x) (pow (log (/ -1 y)) -1))) (log (neg x)) (neg x) (/ (* 1 x) (pow (log (/ -1 y)) -1)) (* 1 x) 1 (pow (log (/ -1 y)) -1) (log (/ -1 y)) (/ -1 y) -1 (* (/ (- (pow (log y) 2) (pow (log x) 2)) -1) (/ x (log (* y x)))) (/ (- (pow (log y) 2) (pow (log x) 2)) -1) (- (pow (log y) 2) (pow (log x) 2)) (pow (log y) 2) (pow (log x) 2) (/ x (log (* y x))) (log (* y x)) (* y x) (/ (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (+ (* (log (* y x)) (log (neg x))) (pow (log (neg y)) 2))) (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) (pow (log (neg x)) 3) (pow (log (neg y)) 3) (log (neg y)) (neg y) (+ (* (log (* y x)) (log (neg x))) (pow (log (neg y)) 2)) (pow (log (neg y)) 2)) |
| 228.0ms | a | @ | 0 | ((* x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))))) x (exp (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b)))) (+ (* y (- (log z) t)) (* a (- (log (- 1 z)) b))) (* y (- (log z) t)) y (- (log z) t) (log z) z t (* a (- (log (- 1 z)) b)) a (- (log (- 1 z)) b) (log (- 1 z)) (- 1 z) 1 b) |
| 590.0ms | 7 037× | 0 | valid |
| 486.0ms | 5 429× | 0 | invalid |
| 3.0ms | 39× | 1 | valid |
| 3.0ms | 23× | 3 | valid |
| 2.0ms | 16× | 2 | valid |
Compiled 8 997 102 to 975 051 computations (89.2% saved)
ival-mult!: 331.0ms (54.9% of total)ival-add!: 268.0ms (44.4% of total)adjust: 4.0ms (0.7% of total)| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
log.f64 | #f | sensitivity | 1565 | 6 |
/.f64 | #f | o/n | 1230 | 0 |
sqrt.f64 | #f | oflow-rescue | 795 | 0 |
-.f64 | #f | cancellation | 591 | 4 |
/.f64 | #f | o/o | 562 | 0 |
*.f64 | #f | n*o | 516 | 0 |
-.f64 | #f | nan-rescue | 460 | 0 |
+.f64 | #f | nan-rescue | 436 | 0 |
cos.f64 | #f | sensitivity | 364 | 1 |
+.f64 | #f | cancellation | 363 | 1 |
/.f64 | #f | n/o | 343 | 0 |
/.f64 | #f | u/n | 239 | 0 |
sin.f64 | #f | sensitivity | 226 | 1 |
*.f64 | #f | n*u | 180 | 0 |
cos.f64 | #f | oflow-rescue | 143 | 0 |
/.f64 | #f | n/u | 136 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | sensitivity | 100 | 1 |
/.f64 | #f | u/u | 98 | 0 |
log.f64 | #f | oflow-rescue | 79 | 0 |
log.f64 | #f | uflow-rescue | 71 | 0 |
sqrt.f64 | #f | uflow-rescue | 42 | 0 |
*.f64 | #f | o*u | 35 | 0 |
tan.f64 | (tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 34 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 34 | |
sin.f64 | (sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64)))) | oflow-rescue | 34 | 0 |
| ↳ | (/.f64 x (*.f64 y #s(literal 2 binary64))) | overflow | 34 | |
exp.f64 | (exp.f64 (-.f64 (+.f64 (*.f64 y (log.f64 z)) (*.f64 (-.f64 t #s(literal 1 binary64)) (log.f64 a))) b)) | sensitivity | 24 | 4 |
*.f64 | #f | u*o | 3 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 6014 | 186 |
| - | 1698 | 60966 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 6014 | 0 | 186 |
| - | 1698 | 20 | 60946 |
| number | freq |
|---|---|
| 0 | 61152 |
| 1 | 6863 |
| 2 | 762 |
| 3 | 72 |
| 4 | 9 |
| 5 | 6 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 137 | 0 | 1 |
| - | 1 | 2 | 128 |
| 9.5s | 130 334× | 0 | valid |
| 1.9s | 6 038× | 1 | valid |
| 453.0ms | 1 234× | 2 | valid |
| 31.0ms | 110× | 3 | valid |
| 3.0ms | 10× | 4 | valid |
| 0.0ms | 2× | 5 | exit |
Compiled 24 442 to 8 402 computations (65.6% saved)
ival-mult!: 2.0s (34.1% of total)ival-log: 856.0ms (14.3% of total)ival-div!: 696.0ms (11.6% of total)ival-add!: 586.0ms (9.8% of total)ival-sub!: 568.0ms (9.5% of total)ival-cos: 333.0ms (5.6% of total)adjust: 311.0ms (5.2% of total)ival-sqrt: 235.0ms (3.9% of total)ival-sin: 212.0ms (3.5% of total)ival-exp: 86.0ms (1.4% of total)ival-fabs: 17.0ms (0.3% of total)ival-tan: 12.0ms (0.2% of total)ival-cosh: 12.0ms (0.2% of total)ival-sinh: 10.0ms (0.2% of total)ival-hypot: 9.0ms (0.2% of total)ival-tanh: 7.0ms (0.1% of total)ival-acos: 5.0ms (0.1% of total)const: 0.0ms (0% of total)| 1 767× | binary-search |
| 1 092× | left-value |
| 1 733× | narrow-enough |
| 34× | predicate-same |
| 14.2s | 144 536× | 0 | valid |
| 942.0ms | 4 300× | 1 | valid |
| 246.0ms | 2 971× | 0 | invalid |
| 26.0ms | 174× | 2 | valid |
| 11.0ms | 30× | 1 | invalid |
| 6.0ms | 30× | 3 | valid |
Compiled 918 373 to 658 654 computations (28.3% saved)
ival-mult!: 4.8s (52.3% of total)ival-sub!: 1.2s (13% of total)ival-add!: 905.0ms (9.8% of total)ival-div!: 740.0ms (8% of total)ival-log: 528.0ms (5.7% of total)ival-sin: 413.0ms (4.5% of total)ival-cos: 198.0ms (2.1% of total)adjust: 185.0ms (2% of total)ival-exp: 87.0ms (0.9% of total)ival-sqrt: 73.0ms (0.8% of total)ival-sinh: 44.0ms (0.5% of total)ival-tanh: 30.0ms (0.3% of total)ival-cosh: 10.0ms (0.1% of total)ival-fabs: 7.0ms (0.1% of total)| 63.0ms | 480× | 0 | invalid |
| 27.0ms | 288× | 0 | valid |
Compiled 765 137 to 420 976 computations (45% saved)
ival-mult!: 57.0ms (93% of total)ival-add!: 5.0ms (8.2% of total)adjust: 0.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)
| 205× | node limit |
| 64× | saturated |
Loading profile data...