
| Date: | Sunday, March 30th, 2025 |
|---|---|
| Commit: | 2100b191 on main |
| Seed: | 2025089 |
| 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: | 165 844.9 MB |
Time bar (total: 2.3min)
| 21.1s | 293 077× | 0 | valid |
| 7.8s | 17 744× | 2 | valid |
| 7.1s | 35 467× | 1 | valid |
| 272.0ms | 4 191× | 0 | invalid |
| 175.0ms | 464× | 3 | valid |
| 118.0ms | 968× | 0 | exit |
| 78.0ms | 101× | 4 | exit |
| 58.0ms | 101× | 3 | exit |
| 3.0ms | 28× | 1 | exit |
ival-mult!: 6.9s (27.1% of total)ival-pow: 3.3s (13% of total)ival-div!: 2.9s (11.4% of total)ival-add!: 2.4s (9.3% of total)adjust: 2.1s (8.2% of total)ival-sin: 2.0s (7.7% of total)ival-cos: 1.9s (7.4% of total)ival-sub!: 1.3s (5.2% of total)ival-exp: 797.0ms (3.1% of total)ival-sqrt: 708.0ms (2.8% of total)ival-pow2: 488.0ms (1.9% of total)ival-neg: 393.0ms (1.5% of total)ival-log1p: 102.0ms (0.4% of total)ival-atan: 78.0ms (0.3% of total)ival-expm1: 75.0ms (0.3% of total)ival-tan: 52.0ms (0.2% of total)ival-hypot: 16.0ms (0.1% of total)ival-<=: 12.0ms (0% of total)ival-==: 11.0ms (0% of total)ival-and: 7.0ms (0% of total)ival-if: 4.0ms (0% of total)ival-fabs: 4.0ms (0% of total)ival-assert: 1.0ms (0% of total)ival-<: 1.0ms (0% of total)const: 0.0ms (0% of total)| 363× | iter-limit |
| 148× | node-limit |
| 9× | saturated |
| 2× | unsound |
| 84× | iter-limit |
| 64× | node-limit |
| 20× | saturated |
Compiled 73 367 to 14 994 computations (79.6% saved)
| 26× | fuel |
| 16× | done |
Compiled 27 067 to 2 679 computations (90.1% saved)
Compiled 2 325 306 to 208 079 computations (91.1% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 1350 | 1 |
+.f64 | #f | cancellation | 372 | 97 |
sqrt.f64 | #f | oflow-rescue | 228 | 0 |
-.f64 | (-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64)) | oflow-left | 220 | 0 |
/.f64 | #f | n/o | 180 | 0 |
/.f64 | #f | o/o | 177 | 0 |
log.f64 | (log.f64 (+.f64 #s(literal 1 binary64) x)) | sensitivity | 175 | 0 |
-.f64 | #f | nan-rescue | 129 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | sensitivity | 109 | 0 |
/.f64 | #f | u/n | 78 | 0 |
/.f64 | #f | n/u | 63 | 0 |
/.f64 | #f | u/u | 52 | 0 |
+.f64 | #f | nan-rescue | 47 | 0 |
/.f64 | #f | o/n | 39 | 0 |
*.f64 | #f | n*u | 39 | 0 |
*.f64 | #f | n*o | 30 | 0 |
pow.f64 | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | oflow-rescue | 23 | 0 |
| ↳ | (pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n) | overflow | 36 | |
| ↳ | (/.f64 i n) | overflow | 23 | |
| ↳ | (+.f64 #s(literal 1 binary64) (/.f64 i n)) | overflow | 23 | |
sqrt.f64 | #f | uflow-rescue | 12 | 0 |
exp.f64 | #f | sensitivity | 2 | 0 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 3990 | 250 |
| - | 127 | 6385 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 3990 | 176 | 74 |
| - | 127 | 179 | 6206 |
| number | freq |
|---|---|
| 0 | 6635 |
| 1 | 3679 |
| 2 | 393 |
| 3 | 45 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 30 | 1 | 0 |
| - | 2 | 0 | 9 |
| 1.3s | 16 778× | 0 | valid |
| 778.0ms | 3 214× | 1 | valid |
| 589.0ms | 1 476× | 2 | valid |
| 23.0ms | 36× | 3 | valid |
Compiled 7 535 to 1 486 computations (80.3% saved)
ival-mult!: 497.0ms (28% of total)ival-div!: 247.0ms (13.9% of total)adjust: 238.0ms (13.4% of total)ival-pow: 204.0ms (11.5% of total)ival-sub!: 170.0ms (9.6% of total)ival-add!: 120.0ms (6.8% of total)ival-sin: 98.0ms (5.5% of total)ival-cos: 62.0ms (3.5% of total)ival-exp: 56.0ms (3.2% of total)ival-sqrt: 26.0ms (1.5% of total)ival-neg: 16.0ms (0.9% of total)ival-pow2: 15.0ms (0.8% of total)ival-log1p: 11.0ms (0.6% of total)ival-atan: 5.0ms (0.3% of total)ival-tan: 4.0ms (0.2% of total)ival-expm1: 3.0ms (0.2% of total)const: 0.0ms (0% of total)96 calls:
| 609.0ms | x |
| 354.0ms | b |
| 273.0ms | (*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x)))) |
| 182.0ms | d |
| 179.0ms | c |
Compiled 8 926 to 5 620 computations (37% saved)
891 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 433.0ms | a | @ | inf | ((* a (+ (+ b c) d)) a (+ (+ b c) d) d (* a (+ (+ b c) d)) (+ (+ b c) d) (+ b c) c (+ (* (+ d b) a) (* c a)) (+ d b) b (* c a)) |
| 143.0ms | x | @ | 0 | ((/ (- x (sin x)) (tan x)) (* (* (+ (* -23/360 (* x x)) 1/6) x) x) (* (+ (* -23/360 (* x x)) 1/6) x) (+ (* -23/360 (* x x)) 1/6) -23/360 (* x x) x 1/6 (/ (- x (sin x)) (tan x)) (* (* x x) 1/6) (/ (- x (sin x)) (tan x)) (* (+ (* (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* x x)) 1/6) (* x x)) (+ (* (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* x x)) 1/6) (- (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) 23/360) (* (* (- (* -143/604800 (* x x)) 11/15120) x) x) (* (- (* -143/604800 (* x x)) 11/15120) x) (- (* -143/604800 (* x x)) 11/15120) (* -143/604800 (* x x)) -143/604800 11/15120 23/360 (/ (- x (sin x)) (tan x)) (- x (sin x)) (* (pow x 3) 1/6) (pow x 3) 3 (tan x) (/ (- x (sin x)) (tan x)) (- x (sin x)) (* (+ (* -1/120 (* x x)) 1/6) (pow x 3)) (+ (* -1/120 (* x x)) 1/6) -1/120) |
| 79.0ms | x | @ | 0 | ((/ (* (- x y) (+ x y)) (+ (* y y) (* x x))) (- (/ (+ (* 0 x) (* x (/ x y))) y) (- 1 (pow (/ x y) 2))) (/ (+ (* 0 x) (* x (/ x y))) y) (+ (* 0 x) (* x (/ x y))) 0 x (* x (/ x y)) (/ x y) y (- 1 (pow (/ x y) 2)) 1 (pow (/ x y) 2) 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 x) 2) (* y y)) 1) (/ (* (* x x) 2) (* y y)) (* (* x x) 2) (/ (* (- x y) (+ x y)) (+ (* y y) (* x x))) (- (+ (- 1 (/ y x)) (+ (* (pow (/ y x) 2) -1) (/ y x))) (pow (/ y x) 2)) (+ (- 1 (/ y x)) (+ (* (pow (/ y x) 2) -1) (/ y x))) (- 1 (pow (/ y x) 2)) (pow (/ y x) 2) (/ y x) (/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) (- (* (+ (cosh (* (log (/ x y)) 2)) (sinh (* (log (/ x y)) 2))) 2) 1) (* (+ (cosh (* (log (/ x y)) 2)) (sinh (* (log (/ x y)) 2))) 2) (+ (cosh (* (log (/ x y)) 2)) (sinh (* (log (/ x y)) 2))) (cosh (* (log (/ x y)) 2)) (* (log (/ x y)) 2) (log (/ x y)) (sinh (* (log (/ x y)) 2))) |
| 79.0ms | t | @ | inf | ((/ (+ 1 (* (/ (+ t t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ (* (* 2 (/ t (+ t 1))) (* 2 (/ t (+ t 1)))) 2)) (+ 1 (* (/ (+ t t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) 1 (* (/ (+ t t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (+ t t) (+ 1 t)) (+ t t) t (+ 1 t) (/ (* 2 t) (+ 1 t)) (* 2 t) 2 (+ (* (* 2 (/ t (+ t 1))) (* 2 (/ t (+ t 1)))) 2) (* 2 (/ t (+ t 1))) (/ t (+ t 1)) (+ t 1) (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (- 5/6 (/ 2/9 t)) 5/6 (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (+ (* (+ (* -2 t) 1) (* t t)) 1/2) (+ (* -2 t) 1) -2 (* t t) 1/2 (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (+ (* (+ (* (- t 2) t) 1) (* t t)) 1/2) (+ (* (- t 2) t) 1) (- t 2) (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (+ (* (/ (- 2/9 (/ 1/27 t)) t) -1) 5/6) (/ (- 2/9 (/ 1/27 t)) t) (/ (- (* 2/9 t) 1/27) (* t t)) (- (* 2/9 t) 1/27) (* 2/9 t) 2/9 1/27 -1) |
| 66.0ms | x | @ | -inf | ((/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (* (- (pow (exp -1) (* x (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) 1/2) (- (pow (exp -1) (* x (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) (pow (exp -1) (* x (- 1 eps))) (exp -1) -1 (* x (- 1 eps)) x (- 1 eps) 1 eps (neg (exp (neg (+ (* x eps) x)))) (exp (neg (+ (* x eps) x))) (neg (+ (* x eps) x)) (+ (* x eps) x) (* x eps) 1/2 (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (* (- (exp (* (neg x) (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) 1/2) (- (exp (* (neg x) (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) (+ (* (+ (* -1 (+ eps 1)) (neg (- 1 eps))) x) 2) (+ (* -1 (+ eps 1)) (neg (- 1 eps))) -2 2 (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (* (- (exp (* (neg x) (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) 1/2) (- (exp (* (neg x) (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) (+ (* (+ (* -1 (/ (- (* eps eps) 1) (- eps 1))) (neg (- 1 eps))) x) 2) (+ (* -1 (/ (- (* eps eps) 1) (- eps 1))) (neg (- 1 eps))) (/ (- (* eps eps) 1) (- eps 1)) (- (* eps eps) 1) (* eps eps) (- eps 1) (neg (- 1 eps)) (/ (- (* (+ 1 (/ 1 eps)) (- (cosh (* (- 1 eps) x)) (sinh (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (- (cosh (* (- 1 eps) x)) (sinh (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (- (cosh (* (- 1 eps) x)) (sinh (* (- 1 eps) x)))) (+ 1 (/ 1 eps)) (/ 1 eps) (- (cosh (* (- 1 eps) x)) (sinh (* (- 1 eps) x))) (+ (* (- eps 1) x) 1) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x)))) (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))) (/ (- (* (* x (- -1 eps)) (* x (- -1 eps))) 1) (- (* x (- -1 eps)) 1)) (- (* (* x (- -1 eps)) (* x (- -1 eps))) 1) (* (* x (- -1 eps)) (* x (- -1 eps))) (* x (- -1 eps)) (- -1 eps) (- (* x (- -1 eps)) 1) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (* (- (pow (exp -1) (* x (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) 1/2) (- (pow (exp -1) (* x (- 1 eps))) (neg (exp (neg (+ (* x eps) x))))) (pow (exp -1) (* x (- 1 eps))) (neg (exp (neg (+ (* x eps) x)))) (exp (neg (+ (* x eps) x))) (neg (+ (* x eps) x)) (+ (* x eps) x)) |
Compiled 147 421 to 63 855 computations (56.7% 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)
| 184× | binary-search |
| 94× | left-value |
| 173× | narrow-enough |
| 10× | predicate-same |
| 1× | predicate-failed |
| 1.2s | 10 782× | 0 | valid |
| 279.0ms | 661× | 2 | valid |
| 265.0ms | 1 163× | 1 | valid |
| 91.0ms | 1 346× | 0 | invalid |
| 16.0ms | 126× | 0 | exit |
| 1.0ms | 2× | 3 | valid |
Compiled 135 397 to 73 103 computations (46% saved)
ival-mult!: 350.0ms (29.5% of total)ival-pow: 252.0ms (21.2% of total)ival-div!: 213.0ms (18% of total)ival-sub!: 103.0ms (8.7% of total)ival-add!: 78.0ms (6.6% of total)adjust: 67.0ms (5.6% of total)ival-exp: 52.0ms (4.4% of total)ival-neg: 35.0ms (3% of total)ival-sqrt: 30.0ms (2.5% of total)ival-expm1: 6.0ms (0.5% of total)Loading profile data...