Herbie run
| Date: | Sunday, March 2nd, 2025 |
|---|---|
| Commit: | 141e80a8 on main |
| Seed: | 2025061 |
| 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: | 157 592.3 MB |
Time bar (total: 3.0min)
| 28.6s | 43 543× | 2 | valid |
| 20.2s | 97 142× | 1 | valid |
| 20.2s | 146 077× | 0 | invalid |
| 16.8s | 7 200× | 5 | exit |
| 7.9s | 87 105× | 0 | valid |
| 2.4s | 3 371× | 3 | valid |
| 351.0ms | 4 219× | 0 | exit |
| 8.0ms | 7× | 4 | valid |
ival-pow: 16.3s (20.1% of total)ival-tan: 12.2s (15.1% of total)adjust: 9.4s (11.6% of total)ival-mult: 6.3s (7.8% of total)ival-cos: 4.5s (5.6% of total)ival-log: 4.0s (5% of total)ival-div: 3.9s (4.8% of total)ival-sin: 3.7s (4.5% of total)ival-add: 3.7s (4.5% of total)ival-sub: 3.5s (4.3% of total)const: 2.7s (3.4% of total)ival-exp: 1.9s (2.3% of total)ival-expm1: 1.8s (2.2% of total)ival-fabs: 1.4s (1.8% of total)ival-sqrt: 1.3s (1.6% of total)ival-log1p: 1.2s (1.4% of total)ival-neg: 817.0ms (1% of total)ival-<: 522.0ms (0.6% of total)ival-and: 401.0ms (0.5% of total)ival-<=: 369.0ms (0.5% of total)ival-atan: 348.0ms (0.4% of total)ival-cbrt: 329.0ms (0.4% of total)exact: 165.0ms (0.2% of total)ival-assert: 138.0ms (0.2% of total)ival-fmin: 85.0ms (0.1% of total)ival->: 2.0ms (0% of total)| 264× | iter limit |
| 109× | node limit |
| 56× | iter limit |
| 51× | node limit |
| 5× | saturated |
Compiled 17 652 to 4 987 computations (71.7% saved)
Compiled 1 538 018 to 177 417 computations (88.5% saved)
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 4165 | 28 |
log.f64 | #f | sensitivity | 764 | 0 |
/.f64 | #f | u/u | 453 | 0 |
sqrt.f64 | #f | oflow-rescue | 438 | 0 |
+.f64 | #f | cancellation | 338 | 0 |
/.f64 | #f | u/n | 106 | 0 |
pow.f64 | (pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n)) | sensitivity | 58 | 0 |
sqrt.f64 | #f | uflow-rescue | 30 | 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 | 22 | 0 |
| ↳ | (*.f64 b eps) | underflow | 142 | |
| ↳ | (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) | underflow | 140 | |
| ↳ | (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) | underflow | 142 | |
| ↳ | (*.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 | 140 | |
-.f64 | #f | nan-rescue | 22 | 0 |
/.f64 | (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x)) | n/o | 6 | 0 |
| ↳ | (*.f64 x x) | overflow | 67 | |
exp.f64 | #f | sensitivity | 4 | 1 |
cos.f64 | (cos.f64 (+.f64 x eps)) | sensitivity | 1 | 1 |
/.f64 | (/.f64 (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) (-.f64 (exp.f64 x) #s(literal 1 binary64))) | o/o | 1 | 0 |
| ↳ | (exp.f64 (*.f64 #s(literal 2 binary64) x)) | overflow | 1 | |
| ↳ | (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) | overflow | 1 | |
| ↳ | (exp.f64 x) | overflow | 1 | |
| ↳ | (-.f64 (exp.f64 x) #s(literal 1 binary64)) | overflow | 1 |
| Predicted + | Predicted - | |
|---|---|---|
| + | 5234 | 17 |
| - | 152 | 1765 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5234 | 11 | 6 |
| - | 152 | 18 | 1747 |
| number | freq |
|---|---|
| 0 | 1782 |
| 1 | 4575 |
| 2 | 646 |
| 3 | 119 |
| 4 | 46 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 28 | 0 | 0 |
| - | 0 | 0 | 0 |
| 1.9s | 2 736× | 2 | valid |
| 1.2s | 6 066× | 1 | valid |
| 484.0ms | 5 286× | 0 | valid |
| 187.0ms | 248× | 3 | valid |
Compiled 2 154 to 763 computations (64.6% saved)
ival-tan: 903.0ms (28.9% of total)adjust: 462.0ms (14.8% of total)ival-sin: 256.0ms (8.2% of total)ival-log: 205.0ms (6.6% of total)ival-cos: 190.0ms (6.1% of total)ival-div: 162.0ms (5.2% of total)ival-sub: 157.0ms (5% of total)ival-exp: 142.0ms (4.5% of total)ival-mult: 133.0ms (4.3% of total)ival-pow: 131.0ms (4.2% of total)ival-add: 108.0ms (3.5% of total)ival-sqrt: 98.0ms (3.1% of total)ival-log1p: 71.0ms (2.3% of total)ival-expm1: 28.0ms (0.9% of total)ival-atan: 20.0ms (0.6% of total)ival-cbrt: 17.0ms (0.5% of total)ival-true: 13.0ms (0.4% of total)ival-neg: 12.0ms (0.4% of total)exact: 9.0ms (0.3% of total)ival-assert: 7.0ms (0.2% of total)| 25× | fuel |
| 3× | done |
Compiled 7 621 to 1 774 computations (76.7% saved)
507 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 71.0ms | N | @ | 0 | ((log (+ 1 (pow N -1))) (pow N -1) N -1 (- (log (+ N 1)) (log N)) (/ (- 1 (/ 1/2 N)) N) (- 1 (/ 1/2 N)) 1 (/ 1/2 N) 1/2 (- (log (+ N 1)) (log N)) (/ (+ (/ (- (/ 1/3 N) 1/2) N) 1) N) (+ (/ (- (/ 1/3 N) 1/2) N) 1) (/ (- (/ 1/3 N) 1/2) N) (- (/ 1/3 N) 1/2) (/ 1/3 N) 1/3 (- (log (+ N 1)) (log N)) (/ (+ (* (/ (+ (* (/ (- (/ 1/4 N) 1/3) N) -1) -1/2) N) -1) -1) (neg N)) (+ (* (/ (+ (* (/ (- (/ 1/4 N) 1/3) N) -1) -1/2) N) -1) -1) (/ (+ (* (/ (- (/ 1/4 N) 1/3) N) -1) -1/2) N) (+ (* (/ (- (/ 1/4 N) 1/3) N) -1) -1/2) (/ (- (/ 1/4 N) 1/3) N) (- (/ 1/4 N) 1/3) (/ 1/4 N) 1/4 -1/2 (neg N) (log (/ (- N -1) N)) (/ (- N -1) N) (- N -1)) |
| 67.0ms | x | @ | 0 | ((- (/ 1 x) (/ 1 (tan x))) (* (+ (* (* x x) 1/45) 1/3) x) (+ (* (* x x) 1/45) 1/3) (* (+ (* (pow x -2) 1/3) 1/45) (* x x)) (+ (* (pow x -2) 1/3) 1/45) (pow x -2) x -2 1/3 1/45 (* x x) (- (/ 1 x) (/ 1 (tan x))) (/ (* (- (pow (* (* x x) 1/45) 2) 1/9) x) (+ (* (* x x) 1/45) -1/3)) (* (- (pow (* (* x x) 1/45) 2) 1/9) x) (- (pow (* (* x x) 1/45) 2) 1/9) (pow (* (* x x) 1/45) 2) (* (* x x) 1/45) 2 1/9 (+ (* (* x x) 1/45) -1/3) -1/3 (- (/ 1 x) (/ 1 (tan x))) (/ (* (+ (* (pow (* x x) 3) 1/91125) 1/27) x) (+ (* (* (* x x) 1/45) (+ (* (* x x) 1/45) -1/3)) 1/9)) (* (+ (* (pow (* x x) 3) 1/91125) 1/27) x) (+ (* (pow (* x x) 3) 1/91125) 1/27) (pow (* x x) 3) 3 1/91125 1/27 (+ (* (* (* x x) 1/45) (+ (* (* x x) 1/45) -1/3)) 1/9) (- (/ 1 x) (/ 1 (tan x))) (+ (* (* (* x x) 1/45) x) (* 1/3 x)) (* 1/3 x)) |
| 59.0ms | n | @ | 0 | ((- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1) (- (* (+ n 1) (log (+ n 1))) (* n (log n))) (* (+ n 1) (log (+ n 1))) (+ n 1) n 1 (log (+ n 1)) (* n (log n)) (log n)) |
| 59.0ms | c | @ | 0 | ((/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (neg (/ (+ (* a (/ (* c c) (* b b))) c) b)) (/ (+ (* a (/ (* c c) (* b b))) c) b) (+ (* a (/ (* c c) (* b b))) c) a (/ (* c c) (* b b)) (* c c) c (* b b) b (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* (- (/ (neg b) c) (sqrt (* (/ a c) -4))) c) (neg b) (* 2 a) 2 (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (sqrt (* (/ c a) -1)) (neg (sqrt (neg (/ c a)))) (sqrt (neg (/ c a))) (neg (/ c a)) (/ c a) (/ (- (neg b) (sqrt (+ (* (* c a) -4) (* b b)))) (+ a a)) (- (neg b) (sqrt (+ (* (* c a) -4) (* b b)))) (sqrt (+ (* (* c a) -4) (* b b))) (+ (* (* c a) -4) (* b b)) (* (* a c) -4) (* a c) -4 (+ a a) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (+ a a)) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (neg (/ (+ (* (/ (pow (* a c) 2) (* b b)) 2) (* 2 (* a c))) b)) (/ (+ (* (/ (pow (* a c) 2) (* b b)) 2) (* 2 (* a c))) b) (+ (* (/ (pow (* a c) 2) (* b b)) 2) (* 2 (* a c))) (/ (pow (* a c) 2) (* b b)) (pow (* a c) 2) (* 2 (* a c))) |
| 49.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (neg (/ (+ (* -1 (+ (log (+ 1 x)) (/ (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) n))) (log x)) n)) (/ (+ (* -1 (+ (log (+ 1 x)) (/ (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) n))) (log x)) n) (+ (* -1 (+ (log (+ 1 x)) (/ (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) n))) (log x)) -1 (+ (log (+ 1 x)) (/ (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) n)) (log (+ 1 x)) x (/ (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) n) (+ (* (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) -1) (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2)))) (/ (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) n) (+ (* (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) -1) (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)))) (/ (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) n) (* 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4))) 1/24 (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (pow (log (+ 1 x)) 4) 4 (pow (log x) 4) (log x) n (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (pow (log (+ 1 x)) 3) 3 (pow (log x) 3) (* 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) (- (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))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (exp (/ (log (+ 1 x)) n)) (/ (log (+ 1 x)) n)) |
Compiled 86 728 to 45 204 computations (47.9% saved)
43 calls:
| 849.0ms | x |
| 246.0ms | eps |
| 95.0ms | (-.f64 (/.f64 #s(literal 1 binary64) (sqrt.f64 x)) (/.f64 #s(literal 1 binary64) (sqrt.f64 (+.f64 x #s(literal 1 binary64))))) |
| 85.0ms | b_2 |
| 83.0ms | a |
Compiled 1 919 to 1 822 computations (5.1% 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)
| 76× | binary-search |
| 25× | left-value |
| 74× | narrow-enough |
| 2× | predicate-same |
| 507.0ms | 5 485× | 0 | valid |
| 146.0ms | 1 721× | 0 | invalid |
| 95.0ms | 300× | 2 | valid |
| 68.0ms | 441× | 1 | valid |
| 4.0ms | 14× | 3 | valid |
| 2.0ms | 18× | 0 | exit |
Compiled 30 487 to 22 097 computations (27.5% saved)
ival-mult: 145.0ms (28.2% of total)ival-div: 78.0ms (15.2% of total)ival-sub: 72.0ms (14% of total)ival-sqrt: 45.0ms (8.7% of total)ival-pow: 36.0ms (7% of total)adjust: 33.0ms (6.4% of total)ival-neg: 32.0ms (6.2% of total)ival-add: 23.0ms (4.5% of total)ival-cos: 17.0ms (3.3% of total)ival-exp: 10.0ms (1.9% of total)ival-expm1: 8.0ms (1.6% of total)ival-true: 6.0ms (1.2% of total)ival-assert: 4.0ms (0.8% of total)exact: 4.0ms (0.8% of total)ival-cbrt: 1.0ms (0.2% of total)| 28× | node limit |
Loading profile data...