
| Date: | Thursday, February 13th, 2025 |
|---|---|
| Commit: | 0e88e39c on custom-lifting-lowering |
| Seed: | 2025044 |
| 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: | 196 302.7 MB |
Time bar (total: 2.7min)
| 29.4s | 284 791× | 0 | valid |
| 13.8s | 44 151× | 1 | valid |
| 8.3s | 17 360× | 2 | valid |
| 344.0ms | 450× | 3 | valid |
| 315.0ms | 4 110× | 0 | invalid |
| 189.0ms | 202× | 5 | exit |
| 148.0ms | 956× | 0 | exit |
ival-mult: 9.1s (23.4% of total)ival-pow: 5.8s (14.9% of total)ival-add: 5.0s (12.8% of total)adjust: 4.9s (12.7% of total)ival-div: 3.4s (8.7% of total)ival-sub: 3.1s (8.1% of total)ival-sin: 1.9s (4.9% of total)ival-cos: 1.8s (4.6% of total)const: 933.0ms (2.4% of total)ival-exp: 579.0ms (1.5% of total)ival-pow2: 515.0ms (1.3% of total)ival-sqrt: 495.0ms (1.3% of total)ival-neg: 474.0ms (1.2% of total)exact: 277.0ms (0.7% of total)ival-tan: 124.0ms (0.3% of total)ival-assert: 119.0ms (0.3% of total)ival-log1p: 98.0ms (0.3% of total)ival-expm1: 80.0ms (0.2% of total)ival-atan: 72.0ms (0.2% of total)ival-pi: 43.0ms (0.1% of total)ival-hypot: 29.0ms (0.1% of total)ival-<=: 12.0ms (0% of total)ival-true: 10.0ms (0% of total)ival-and: 9.0ms (0% of total)ival-if: 6.0ms (0% of total)ival-fabs: 5.0ms (0% of total)ival-==: 3.0ms (0% of total)ival-<: 1.0ms (0% of total)| 213× | iter limit |
| 142× | node limit |
| 5× | saturated |
| 5× | unsound |
| 84× | iter limit |
| 64× | node limit |
| 20× | saturated |
Compiled 54 099 to 8 456 computations (84.4% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 1318 | 0 |
+.f64 | #f | cancellation | 366 | 91 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 219 | 0 |
sqrt.f64 | #f | oflow-rescue | 196 | 0 |
log.f64 | (log.f64 (+.f64 #s(literal 1 binary64) x)) | sensitivity | 172 | 1 |
/.f64 | #f | n/o | 163 | 0 |
/.f64 | #f | o/o | 162 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | sensitivity | 130 | 1 |
-.f64 | #f | nan-rescue | 113 | 0 |
/.f64 | #f | u/n | 92 | 0 |
/.f64 | #f | u/u | 53 | 0 |
/.f64 | #f | n/u | 48 | 0 |
+.f64 | #f | nan-rescue | 47 | 0 |
/.f64 | #f | o/n | 47 | 0 |
*.f64 | #f | n*u | 39 | 0 |
*.f64 | #f | n*o | 25 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | oflow-rescue | 17 | 0 |
| ↳ | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | overflow | 25 | |
| ↳ | (/.f64 i n) | overflow | 17 | |
| ↳ | (+.f64 #s(literal 1 binary64) (/.f64 i n)) | overflow | 17 | |
sqrt.f64 | #f | uflow-rescue | 12 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3907 | 241 |
| - | 106 | 6498 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3907 | 174 | 67 |
| - | 106 | 174 | 6324 |
| number | freq |
|---|---|
| 0 | 6739 |
| 1 | 3575 |
| 2 | 395 |
| 3 | 43 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 30 | 1 | 0 |
| - | 2 | 0 | 9 |
| 1.6s | 16 276× | 0 | valid |
| 1.4s | 3 764× | 1 | valid |
| 643.0ms | 1 416× | 2 | valid |
| 32.0ms | 48× | 3 | valid |
Compiled 7 535 to 1 486 computations (80.3% saved)
ival-mult: 583.0ms (23.2% of total)adjust: 456.0ms (18.2% of total)ival-add: 328.0ms (13.1% of total)ival-pow: 265.0ms (10.6% of total)ival-div: 240.0ms (9.6% of total)ival-sub: 200.0ms (8% of total)ival-sin: 110.0ms (4.4% of total)const: 109.0ms (4.3% of total)ival-cos: 71.0ms (2.8% of total)ival-exp: 30.0ms (1.2% of total)ival-sqrt: 24.0ms (1% of total)ival-true: 19.0ms (0.8% of total)exact: 19.0ms (0.8% of total)ival-neg: 15.0ms (0.6% of total)ival-pow2: 14.0ms (0.6% of total)ival-assert: 9.0ms (0.4% of total)ival-atan: 5.0ms (0.2% of total)ival-tan: 4.0ms (0.2% of total)ival-log1p: 4.0ms (0.2% of total)ival-expm1: 3.0ms (0.1% of total)ival-pi: 2.0ms (0.1% of total)Compiled 2 249 751 to 196 362 computations (91.3% saved)
| 25× | fuel |
| 17× | done |
Compiled 24 172 to 2 560 computations (89.4% saved)
Compiled 144 407 to 63 919 computations (55.7% saved)
879 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 153.0ms | c | @ | 0 | ((* (+ a (+ b (+ c d))) 2) (* 2 (+ b (+ (+ d c) a))) 2 (+ b (+ (+ d c) a)) b (+ (+ d c) a) (* c (+ 1 (/ (+ a d) c))) c (+ 1 (/ (+ a d) c)) 1 (/ (+ a d) c) (+ a d) a d (* (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) 2) (- (/ (* a a) (- a (+ (+ d c) b))) (/ (pow (+ (+ d c) b) 2) (- a (+ (+ d c) b)))) (* (+ a (+ b (+ c d))) 2) (+ a (+ b (+ c d))) (+ b (+ c d)) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ c b) a) d) 2) 2) d) (+ (* (/ (+ (+ c b) a) d) 2) 2) (/ (+ (+ c b) a) d) (+ (+ c b) a) (+ c b) (* (+ a (+ b (+ c d))) 2) (* (+ (* (/ (+ (+ d c) b) a) 2) 2) a) (+ (* (/ (+ (+ d c) b) a) 2) 2) (/ (+ (+ d c) b) a) (+ (+ d c) b) (+ d c)) |
| 66.0ms | y | @ | inf | ((/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (+ (* 0 (/ x y)) (pow (/ x y) 2)) (/ (- 1 (pow (/ x y) 4)) (+ 1 (pow (/ x y) 2)))) (+ (* 0 (/ x y)) (pow (/ x y) 2)) 0 (/ x y) x y (pow (/ x y) 2) 2 (/ (- 1 (pow (/ x y) 4)) (+ 1 (pow (/ x y) 2))) (- 1 (pow (/ x y) 4)) 1 (+ 1 (pow (/ x y) 2)) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (+ (* (/ (* y y) (* x x)) -2) 1) (/ (* y y) (* x x)) (* y y) (* x x) -2 (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (+ (* (/ x y) (/ x y)) 0) (- 1 (exp (- (* (log x) 2) (* (log y) 2))))) (+ (* (/ x y) (/ x y)) 0) (- 1 (exp (- (* (log x) 2) (* (log y) 2)))) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (* (pow (/ x y) 2) 2) 1) (* (pow (/ x y) 2) 2) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (+ (* (exp (- (* (log y) 2) (* (log x) 2))) -2) 1) (exp (- (* (log y) 2) (* (log x) 2))) (- (* (log y) 2) (* (log x) 2)) (* (log y) 2) (log y) (* (log x) 2) (log x)) |
| 62.0ms | r | @ | inf | ((- (- (+ 3 (/ 2 (* r r))) (* (* (+ (* -2 v) 3) 1/8) (* w (/ (* (* w r) r) (- 1 v))))) 9/2) (- (+ 3 (/ 2 (* r r))) (* (* (+ (* -2 v) 3) 1/8) (* w (/ (* (* w r) r) (- 1 v))))) (+ 3 (/ 2 (* r r))) 3 (/ 2 (* r r)) 2 (* r r) r (* (* (+ (* -2 v) 3) 1/8) (* w (/ (* (* w r) r) (- 1 v)))) (* (+ (* -2 v) 3) 1/8) (+ (* -2 v) 3) -2 v 1/8 (* w (/ (* (* w r) r) (- 1 v))) w (/ (* (* w r) r) (- 1 v)) (* (* w r) r) (* w r) (- 1 v) 1 9/2 (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (/ (+ (* -3/2 (* r r)) 2) (* r r)) (+ (* -3/2 (* r r)) 2) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) (/ (+ (* (* r r) 3) 2) (* r r)) (+ (* (* r r) 3) 2) (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)) (* (* 1/4 (* r r)) (* w w)) (* 1/4 (* r r)) 1/4 (* w w) (- (- (+ 3 (/ (/ 2 r) r)) (* (* (+ (* -2 v) 3) 1/8) (/ (* w (* (* w r) r)) (- 1 v)))) 9/2) (- (+ 3 (/ (/ 2 r) r)) (* (* (+ (* -2 v) 3) 1/8) (/ (* w (* (* w r) r)) (- 1 v)))) (+ 3 (/ (/ 2 r) r)) (/ (/ 2 r) r) (/ 2 r) (* (* (+ (* -2 v) 3) 1/8) (/ (* w (* (* w r) r)) (- 1 v))) (/ (* w (* (* w r) r)) (- 1 v)) (* w (* (* w r) r))) |
| 60.0ms | y | @ | 0 | ((+ (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (* (/ x y) 1/2) (/ x y) x y 1/2 (+ (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (/ x (* 2 y))) (+ (+ (* 1335/4 (pow y 6)) (* (* x x) (- (- (- (* (* (* (* 11 x) x) y) y) (pow y 6)) (* 121 (pow y 4))) 2))) (* 11/2 (pow y 8))) (* -2 (* x x)) -2 (* x x) (/ x (* 2 y)) (* 2 y) 2) |
| 56.0ms | x | @ | 0 | ((/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (+ (* 0 (/ x y)) (pow (/ x y) 2)) (- 1 (exp (- (* (log x) 2) (* (log y) 2))))) (+ (* 0 (/ x y)) (pow (/ x y) 2)) 0 (/ x y) x y (pow (/ x y) 2) 2 (- 1 (exp (- (* (log x) 2) (* (log y) 2)))) 1 (exp (- (* (log x) 2) (* (log y) 2))) (- (* (log x) 2) (* (log y) 2)) (* (log x) 2) (log x) (* (log y) 2) (log y) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (+ (* (pow (/ y x) 2) -2) 1) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (+ (* (* (/ y x) (/ y x)) -2) 1) (* (/ y x) (/ y x)) (/ y x) -2 (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (+ (* (/ x y) (/ x y)) 0) (- 1 (pow (/ x y) 2))) (+ (* (/ x y) (/ x y)) 0) (- 1 (pow (/ x y) 2)) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (+ (* 0 (/ x y)) (pow (/ x y) 2)) (/ (- 1 (pow (/ x y) 4)) (+ 1 (pow (/ x y) 2)))) (/ (- 1 (pow (/ x y) 4)) (+ 1 (pow (/ x y) 2))) (- 1 (pow (/ x y) 4)) (pow (/ x y) 4) 4 (+ 1 (pow (/ x y) 2))) |
96 calls:
| 730.0ms | x |
| 264.0ms | (*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x)))) |
| 242.0ms | b |
| 203.0ms | c |
| 193.0ms | a |
Compiled 7 939 to 5 165 computations (34.9% saved)
| 43× | search |
| 2× | random |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 54.5% | 45.5% | 0% | 0% | 0% | 0 |
| 21.4% | 11.7% | 42.9% | 45.5% | 0% | 0% | 0% | 1 |
| 37.4% | 20.4% | 34.1% | 45.5% | 0% | 0% | 0% | 2 |
| 48.7% | 26.2% | 27.7% | 45.5% | 0% | 0.6% | 0% | 3 |
| 57.7% | 30.7% | 22.6% | 45.5% | 0% | 1.2% | 0% | 4 |
| 71.2% | 37.7% | 15.3% | 45.5% | 0% | 1.6% | 0% | 5 |
| 72.9% | 38.4% | 14.3% | 45.5% | 0% | 1.8% | 0% | 6 |
| 77.9% | 40.7% | 11.6% | 45.5% | 0% | 2.2% | 0% | 7 |
| 81.5% | 42.6% | 9.7% | 45.5% | 0% | 2.3% | 0% | 8 |
| 84.1% | 43.8% | 8.3% | 45.5% | 0% | 2.5% | 0% | 9 |
| 86.2% | 44.6% | 7.2% | 45.5% | 0% | 2.7% | 0% | 10 |
| 88.2% | 45.6% | 6.1% | 45.5% | 0% | 2.8% | 0% | 11 |
| 89.1% | 45.9% | 5.6% | 45.5% | 0% | 2.9% | 0% | 12 |
Compiled 1 402 to 721 computations (48.6% saved)
| 149× | binary-search |
| 89× | left-value |
| 140× | narrow-enough |
| 8× | predicate-same |
| 1× | predicate-failed |
| 958.0ms | 9 770× | 0 | valid |
| 494.0ms | 1 224× | 1 | valid |
| 145.0ms | 395× | 2 | valid |
| 95.0ms | 1 260× | 0 | invalid |
| 14.0ms | 19× | 3 | valid |
| 9.0ms | 72× | 0 | exit |
Compiled 109 205 to 60 877 computations (44.3% saved)
ival-mult: 382.0ms (30.3% of total)ival-div: 143.0ms (11.4% of total)ival-pow: 142.0ms (11.3% of total)ival-sub: 128.0ms (10.2% of total)ival-exp: 124.0ms (9.8% of total)ival-add: 114.0ms (9.1% of total)ival-neg: 87.0ms (6.9% of total)adjust: 82.0ms (6.5% of total)ival-sqrt: 26.0ms (2.1% of total)exact: 10.0ms (0.8% of total)ival-true: 9.0ms (0.7% of total)ival-assert: 5.0ms (0.4% of total)ival-expm1: 4.0ms (0.3% of total)const: 3.0ms (0.2% of total)ival-pi: 2.0ms (0.2% of total)| 32× | node limit |
| 10× | saturated |
Loading profile data...