Herbie run
| Date: | Tuesday, March 25th, 2025 |
|---|---|
| Commit: | 481a8102 on main |
| Seed: | 2025084 |
| 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: | 149 871.4 MB |
Time bar (total: 2.6min)
| 24.9s | 44 570× | 2 | valid |
| 16.2s | 145 295× | 0 | invalid |
| 15.6s | 96 995× | 1 | valid |
| 10.6s | 6 175× | 5 | exit |
| 7.0s | 86 062× | 0 | valid |
| 2.6s | 3 539× | 3 | valid |
| 317.0ms | 4 206× | 0 | exit |
| 156.0ms | 1 092× | 1 | exit |
| 12.0ms | 6× | 4 | exit |
| 2.0ms | 1× | 2 | exit |
| 2.0ms | 2× | 4 | valid |
| 2.0ms | 1× | 3 | exit |
ival-tan: 11.9s (19.4% of total)ival-pow: 10.7s (17.4% of total)adjust: 6.6s (10.8% of total)ival-mult!: 4.4s (7.2% of total)ival-cos: 4.0s (6.5% of total)ival-log: 3.4s (5.5% of total)ival-sin: 3.3s (5.4% of total)ival-div!: 3.0s (4.9% of total)ival-fabs: 2.1s (3.4% of total)ival-exp: 1.9s (3.1% of total)ival-sub!: 1.9s (3% of total)ival-expm1: 1.8s (2.9% of total)ival-add!: 1.8s (2.9% of total)ival-sqrt: 1.5s (2.4% of total)ival-log1p: 1.0s (1.6% of total)ival-<: 504.0ms (0.8% of total)ival-<=: 364.0ms (0.6% of total)ival-atan: 340.0ms (0.6% of total)ival-and: 326.0ms (0.5% of total)ival-cbrt: 297.0ms (0.5% of total)ival-neg: 295.0ms (0.5% of total)ival-fmin: 88.0ms (0.1% of total)ival-assert: 70.0ms (0.1% of total)ival->: 1.0ms (0% of total)| 254× | iter limit |
| 106× | node limit |
| 21× | fuel |
| 7× | done |
Compiled 10 407 to 2 128 computations (79.6% saved)
| 56× | iter limit |
| 51× | node limit |
| 5× | saturated |
Compiled 25 294 to 6 863 computations (72.9% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 4143 | 36 |
log.f64 | #f | sensitivity | 768 | 0 |
/.f64 | #f | u/u | 431 | 0 |
sqrt.f64 | #f | oflow-rescue | 402 | 0 |
+.f64 | #f | cancellation | 356 | 0 |
/.f64 | #f | u/n | 117 | 0 |
pow.f64 | #f | sensitivity | 61 | 2 |
sqrt.f64 | #f | uflow-rescue | 20 | 0 |
/.f64 | (/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))) | n/u | 19 | 0 |
| ↳ | (*.f64 b eps) | underflow | 141 | |
| ↳ | (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) | underflow | 156 | |
| ↳ | (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) | underflow | 141 | |
| ↳ | (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))) | underflow | 228 | |
| ↳ | (*.f64 a eps) | underflow | 156 | |
-.f64 | #f | nan-rescue | 19 | 0 |
exp.f64 | #f | sensitivity | 3 | 0 |
/.f64 | (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x)) | n/o | 2 | 0 |
| ↳ | (*.f64 x x) | overflow | 61 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 5226 | 23 |
| - | 124 | 1795 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5226 | 16 | 7 |
| - | 124 | 19 | 1776 |
| number | freq |
|---|---|
| 0 | 1818 |
| 1 | 4553 |
| 2 | 650 |
| 3 | 100 |
| 4 | 47 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 28 | 0 | 0 |
| - | 0 | 0 | 0 |
| 2.0s | 2 820× | 2 | valid |
| 1.1s | 5 982× | 1 | valid |
| 411.0ms | 5 346× | 0 | valid |
| 209.0ms | 188× | 3 | valid |
Compiled 2 154 to 763 computations (64.6% saved)
adjust: 876.0ms (28.6% of total)ival-tan: 636.0ms (20.7% of total)ival-pow: 268.0ms (8.7% of total)ival-cos: 208.0ms (6.8% of total)ival-log: 191.0ms (6.2% of total)ival-sin: 151.0ms (4.9% of total)ival-div!: 132.0ms (4.3% of total)ival-exp: 131.0ms (4.3% of total)ival-mult!: 111.0ms (3.6% of total)ival-sub!: 76.0ms (2.5% of total)ival-sqrt: 70.0ms (2.3% of total)ival-expm1: 61.0ms (2% of total)ival-log1p: 55.0ms (1.8% of total)ival-add!: 52.0ms (1.7% of total)ival-atan: 21.0ms (0.7% of total)ival-cbrt: 16.0ms (0.5% of total)ival-neg: 12.0ms (0.4% of total)Compiled 1 479 379 to 169 875 computations (88.5% saved)
498 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 86.0ms | N | @ | 0 | ((- (log (+ N 1)) (log N)) (log (+ N 1)) (+ N 1) N 1 (log N)) |
| 84.0ms | c | @ | inf | ((/ (- (* (neg b_2) a) (* a (sqrt (+ (* b_2 b_2) (* c (neg a)))))) (* a a)) (- (* (neg b_2) a) (* a (sqrt (+ (* b_2 b_2) (* c (neg a)))))) (* (neg b_2) a) (neg b_2) b_2 a (* a (sqrt (+ (* b_2 b_2) (* c (neg a))))) (sqrt (+ (* b_2 b_2) (* c (neg a)))) (+ (* b_2 b_2) (* c (neg a))) (* c (neg a)) c (neg a) (* a a) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (* (/ b_2 a) -2) (/ b_2 a) -2 (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (neg (sqrt (* (neg a) c))) (sqrt (* (neg a) c)) (* (neg a) c) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (* (/ b_2 a) -1) (sqrt (/ (neg c) a))) -1 (sqrt (/ (neg c) a)) (/ (neg c) a) (neg c) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (* (neg c) (- (/ b_2 c) (sqrt (* (/ a c) -1)))) (- (/ b_2 c) (sqrt (* (/ a c) -1))) (/ (sqrt (neg a)) (sqrt c)) (sqrt (neg a)) (sqrt c)) |
| 62.0ms | x | @ | -inf | ((- (cbrt (+ x 1)) (cbrt x)) (cbrt (+ x 1)) (+ x 1) x 1 (cbrt x)) |
| 58.0ms | n | @ | -inf | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n)) (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n) (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) (/ (+ (* -1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (* n (+ (log x) (* -1 (log (+ 1 x)))))) n) (+ (* -1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (* n (+ (log x) (* -1 (log (+ 1 x)))))) -1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (pow (log (+ 1 x)) 2) (log (+ 1 x)) x 2 (pow (log x) 2) (log x) (* n (+ (log x) (* -1 (log (+ 1 x))))) n (+ (log x) (* -1 (log (+ 1 x)))) (* -1 (log (+ 1 x))) -1 (- (pow (+ x 1) (/ 1 n)) (pow x (pow n -1))) (pow (+ x 1) (/ 1 n)) 1 (pow x (pow n -1)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ (- (+ (/ 1/3 (* n (* x x))) (pow n -1)) (/ 1/2 (* n x))) x) (- (+ (/ 1/3 (* n (* x x))) (pow n -1)) (/ 1/2 (* n x))) (+ (/ 1/3 (* n (* x x))) (pow n -1)) (/ 1/3 (* n (* x x))) 1/3 (* n (* x x)) (* x x) (pow n -1) (/ 1/2 (* n x)) 1/2 (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n)) (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n) (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) (+ (log x) (* 1/2 (/ (pow (log x) 2) n))) (* 1/2 (/ (pow (log x) 2) n)) (/ (pow (log x) 2) n)) |
| 56.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n)) (/ (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) n) (+ (* -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n))) (log x)) -1 (+ (log (+ 1 x)) (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n)) (log (+ 1 x)) x (/ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) n) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (pow (log (+ 1 x)) 2) 2 (pow (log x) 2) (log x) n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) 1 (pow x (/ 1 n)) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (- (log (+ 1 x)) (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (exp (/ (log (+ 1 x)) n)) (/ (log (+ 1 x)) n) (/ (- (pow (pow (+ 1 x) (pow n -1)) 2) (pow (pow x (pow n -1)) 2)) (+ (pow (+ 1 x) (pow n -1)) (pow x (pow n -1)))) (- (pow (pow (+ 1 x) (pow n -1)) 2) (pow (pow x (pow n -1)) 2)) (pow (pow (+ 1 x) (pow n -1)) 2) (pow (+ 1 x) (pow n -1)) (+ 1 x) (pow n -1) (pow (pow x (pow n -1)) 2) (pow x (pow n -1)) (+ (pow (+ 1 x) (pow n -1)) (pow x (pow n -1)))) |
43 calls:
| 1.1s | x |
| 391.0ms | eps |
| 161.0ms | (-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x)) |
| 125.0ms | b |
| 104.0ms | (-.f64 (sin.f64 (+.f64 x eps)) (sin.f64 x)) |
Compiled 2 310 to 2 219 computations (3.9% saved)
Compiled 94 753 to 48 469 computations (48.8% saved)
| 28× | search |
| Probability | Valid | Unknown | Precondition | Infinite | Domain | Can't | Iter |
|---|---|---|---|---|---|---|---|
| 0% | 0% | 61.1% | 38.9% | 0% | 0% | 0% | 0 |
| 7.4% | 4.5% | 56.6% | 38.9% | 0% | 0% | 0% | 1 |
| 22.3% | 13.6% | 47.5% | 38.9% | 0% | 0% | 0% | 2 |
| 40.2% | 23.5% | 34.9% | 38.9% | 0% | 2.7% | 0% | 3 |
| 53.4% | 31.1% | 27.2% | 38.9% | 0% | 2.8% | 0% | 4 |
| 63% | 36.3% | 21.3% | 38.9% | 0% | 3.6% | 0% | 5 |
| 65.9% | 37.5% | 19.4% | 38.9% | 0% | 4.2% | 0% | 6 |
| 70.4% | 38.8% | 16.3% | 38.9% | 0% | 6% | 0% | 7 |
| 73.6% | 40.2% | 14.4% | 38.9% | 0% | 6.5% | 0% | 8 |
| 76.3% | 40.9% | 12.7% | 38.9% | 0% | 7.5% | 0% | 9 |
| 78.4% | 41.4% | 11.4% | 38.9% | 0% | 8.3% | 0% | 10 |
| 81.1% | 42.4% | 9.9% | 38.9% | 0% | 8.8% | 0% | 11 |
| 82.3% | 42.7% | 9.2% | 38.9% | 0% | 9.3% | 0% | 12 |
Compiled 483 to 337 computations (30.2% saved)
| 28× | node limit |
| 88× | binary-search |
| 26× | left-value |
| 82× | narrow-enough |
| 6× | predicate-same |
| 404.0ms | 4 585× | 0 | valid |
| 120.0ms | 436× | 2 | valid |
| 119.0ms | 1 108× | 1 | valid |
| 96.0ms | 1 276× | 0 | invalid |
| 3.0ms | 15× | 3 | valid |
| 1.0ms | 13× | 0 | exit |
Compiled 28 972 to 21 986 computations (24.1% saved)
ival-mult!: 149.0ms (31.3% of total)ival-pow: 54.0ms (11.3% of total)ival-sub!: 54.0ms (11.3% of total)ival-sqrt: 53.0ms (11.1% of total)ival-div!: 46.0ms (9.7% of total)ival-neg: 42.0ms (8.8% of total)adjust: 39.0ms (8.2% of total)ival-add!: 15.0ms (3.1% of total)ival-cos: 15.0ms (3.1% of total)ival-cbrt: 9.0ms (1.9% of total)ival-expm1: 2.0ms (0.4% of total)Loading profile data...