Herbie run
| 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: | 142 020.4 MB |
Time bar (total: 2.8min)
| 26.0s | 45 048× | 2 | valid |
| 16.9s | 96 643× | 1 | valid |
| 16.8s | 144 260× | 0 | invalid |
| 11.5s | 5 994× | 5 | exit |
| 6.7s | 85 915× | 0 | valid |
| 2.4s | 3 561× | 3 | valid |
| 312.0ms | 4 111× | 0 | exit |
| 155.0ms | 1 136× | 1 | exit |
| 15.0ms | 6× | 4 | exit |
| 12.0ms | 3× | 3 | exit |
| 1.0ms | 1× | 2 | exit |
| 1.0ms | 1× | 4 | valid |
ival-pow: 11.9s (18.2% of total)ival-tan: 11.8s (18% of total)adjust: 6.7s (10.1% of total)ival-mult!: 5.1s (7.8% of total)ival-div!: 4.0s (6.1% of total)ival-cos: 4.0s (6.1% of total)ival-log: 3.8s (5.9% of total)ival-sin: 3.4s (5.1% of total)ival-expm1: 3.1s (4.8% of total)ival-sub!: 2.1s (3.3% of total)ival-exp: 1.8s (2.8% of total)ival-fabs: 1.6s (2.5% of total)ival-add!: 1.6s (2.4% of total)ival-log1p: 1.2s (1.8% of total)ival-sqrt: 1.1s (1.7% of total)ival-<: 491.0ms (0.7% of total)ival-<=: 457.0ms (0.7% of total)ival-and: 348.0ms (0.5% of total)ival-atan: 345.0ms (0.5% of total)ival-cbrt: 275.0ms (0.4% of total)ival-neg: 263.0ms (0.4% of total)ival-assert: 63.0ms (0.1% of total)ival-fmin: 58.0ms (0.1% of total)ival->: 1.0ms (0% of total)| 262× | iter limit |
| 107× | node limit |
| 56× | iter limit |
| 51× | node limit |
| 5× | saturated |
| 2.0s | 33 024× | 0 | valid |
Compiled 16 638 to 4 361 computations (73.8% saved)
ival-mult!: 831.0ms (79.9% of total)ival-add!: 204.0ms (19.6% of total)adjust: 6.0ms (0.6% of total)| 24× | fuel |
| 4× | done |
| 55.0ms | 1 024× | 0 | valid |
Compiled 7 674 to 1 718 computations (77.6% saved)
ival-mult!: 20.0ms (71.8% of total)ival-add!: 8.0ms (28.7% of total)adjust: 0.0ms (0% of total)| 425.0ms | 4 275× | 0 | valid |
| 22.0ms | 333× | 0 | invalid |
Compiled 1 221 867 to 150 276 computations (87.7% saved)
ival-mult!: 157.0ms (62.3% of total)ival-add!: 94.0ms (37.3% of total)adjust: 1.0ms (0.4% of total)| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 4162 | 42 |
log.f64 | #f | sensitivity | 766 | 1 |
/.f64 | #f | u/u | 431 | 0 |
sqrt.f64 | #f | oflow-rescue | 382 | 0 |
+.f64 | #f | cancellation | 328 | 0 |
/.f64 | #f | u/n | 120 | 0 |
pow.f64 | (pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n)) | sensitivity | 85 | 0 |
sqrt.f64 | #f | uflow-rescue | 46 | 0 |
-.f64 | #f | nan-rescue | 24 | 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 | 17 | 0 |
| ↳ | (*.f64 b eps) | underflow | 149 | |
| ↳ | (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) | underflow | 146 | |
| ↳ | (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) | underflow | 149 | |
| ↳ | (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))) | underflow | 231 | |
| ↳ | (*.f64 a eps) | underflow | 146 | |
/.f64 | (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x)) | n/o | 5 | 0 |
| ↳ | (*.f64 x x) | overflow | 69 | |
exp.f64 | (exp.f64 (neg.f64 x)) | sensitivity | 4 | 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 - | |
|---|---|---|
| + | 5197 | 23 |
| - | 154 | 1794 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5197 | 18 | 5 |
| - | 154 | 26 | 1768 |
| number | freq |
|---|---|
| 0 | 1817 |
| 1 | 4531 |
| 2 | 664 |
| 3 | 112 |
| 4 | 44 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 28 | 0 | 0 |
| - | 0 | 0 | 0 |
| 1.6s | 2 862× | 2 | valid |
| 1.2s | 6 062× | 1 | valid |
| 393.0ms | 5 220× | 0 | valid |
| 164.0ms | 192× | 3 | valid |
Compiled 2 154 to 763 computations (64.6% saved)
ival-tan: 772.0ms (30.8% of total)adjust: 352.0ms (14% of total)ival-log: 190.0ms (7.6% of total)ival-cos: 182.0ms (7.3% of total)ival-sin: 140.0ms (5.6% of total)ival-exp: 121.0ms (4.8% of total)ival-div!: 120.0ms (4.8% of total)ival-sqrt: 117.0ms (4.7% of total)ival-pow: 116.0ms (4.6% of total)ival-sub!: 98.0ms (3.9% of total)ival-log1p: 96.0ms (3.8% of total)ival-mult!: 79.0ms (3.1% of total)ival-add!: 49.0ms (2% of total)ival-expm1: 23.0ms (0.9% of total)ival-atan: 21.0ms (0.8% of total)ival-cbrt: 16.0ms (0.6% of total)ival-neg: 14.0ms (0.6% of total)498 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 77.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (* (pow n -2) 1/2) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (* (pow n -2) 1/2) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (/ (pow (pow (exp -1) -1) (/ (log x) n)) n) (pow (pow (exp -1) -1) (/ (log x) n)) (pow (exp -1) -1) (exp -1) -1 (/ (log x) n) (log x) x n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) 1 (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (pow (* n x) -1) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (+ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (/ (log x) n)) (* n x)) (exp (/ (log x) n))) |
| 71.0ms | x | @ | inf | ((- (cbrt (+ x 1)) (cbrt x)) (* (cbrt (* (pow x -1) (pow x -1))) 1/3) (cbrt (* (pow x -1) (pow x -1))) (* (pow x -1) (pow x -1)) (pow x -1) x -1 1/3 (- (cbrt (+ x 1)) (pow x 1/3)) (cbrt (+ x 1)) 1 (pow x 1/3) (- (cbrt (+ x 1)) (pow x 1/3)) (cbrt (+ x 1)) (+ x 1) (- (cbrt (+ x 1)) (exp (* (log x) 1/3))) (cbrt (+ x 1)) (+ x 1) (exp (* (log x) 1/3)) (* (log x) 1/3) (log x) (- (cbrt (exp (* (log (cbrt (- x -1))) 3))) (cbrt x)) (cbrt (exp (* (log (cbrt (- x -1))) 3))) (exp (* (log (cbrt (- x -1))) 3)) (* (log (cbrt (- x -1))) 3) (log (cbrt (- x -1))) (cbrt (- x -1)) (- x -1) 3 (cbrt x)) |
| 64.0ms | N | @ | inf | ((log (+ 1 (/ 1 N))) (/ 1 N) 1 N (- (log (+ N 1)) (log N)) (/ (- 1 (/ 1/2 N)) N) (- 1 (/ 1/2 N)) (- (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 1/2 (- (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/3 N) 1/4) (* N N)) (+ (* -1/3 N) 1/4) -1/3 1/4 (* N N) -1 -1/2 (neg N) (log (+ 1 (exp (neg (log N))))) (exp (neg (log N))) (neg (log N)) (log N)) |
| 52.0ms | x | @ | 0 | ((* (* (cos (/ (+ (+ eps x) x) 2)) (sin (/ (- (+ eps x) x) 2))) 2) (* (cos (/ (+ (+ eps x) x) 2)) (sin (/ (- (+ eps x) x) 2))) (* (cos (* (+ (* 2 x) eps) 1/2)) (sin (* 1/2 eps))) (cos (* (+ (* 2 x) eps) 1/2)) (* (+ (* 2 x) eps) 1/2) (+ (* 1/2 eps) x) 1/2 eps x (sin (* 1/2 eps)) (* 1/2 eps) 2 (- (sin (+ x eps)) (sin x)) (* (+ (* (* (sin x) eps) -1/2) (cos x)) eps) (+ (* (* (sin x) eps) -1/2) (cos x)) (+ (* (* -1/2 (+ eps x)) x) 1) (* (* x eps) -1/2) (* x eps) -1/2 (- (sin (+ x eps)) (sin x)) (* (+ (* (* (sin x) eps) -1/2) (cos x)) eps) (+ (* (* (sin x) eps) -1/2) (cos x)) (+ (* (* -1/2 (+ eps x)) x) 1) (* -1/2 (+ eps x)) (+ eps x) 1 (- (sin (+ x eps)) (sin x)) (* (+ (* (* (sin x) eps) -1/2) (cos x)) eps) (+ (* (* (sin x) eps) -1/2) (cos x)) (+ (* (+ (* (- (* (* eps x) 1/12) 1/2) x) (* -1/2 eps)) x) 1) (+ (* (- (* (* eps x) 1/12) 1/2) x) (* -1/2 eps)) (- (* (* eps x) 1/12) 1/2) (* (* eps x) 1/12) (* eps x) 1/12 (* -1/2 eps) (- (sin (+ x eps)) (sin x)) (* (+ (* (* (sin x) eps) -1/2) (cos x)) eps) (+ (* (* (sin x) eps) -1/2) (cos x)) (* (sin x) eps) (sin x) (* (+ (* (* x x) -1/6) 1) x) (cos x)) |
| 50.0ms | n | @ | inf | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (* (pow n -2) 1/2) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) x) (+ (* (exp (neg (/ (neg (log x)) n))) (/ (- (* (pow n -2) 1/2) (/ 1/2 n)) x)) (/ (exp (neg (/ (neg (log x)) n))) n)) (/ (pow (pow (exp -1) -1) (/ (log x) n)) n) (pow (pow (exp -1) -1) (/ (log x) n)) (pow (exp -1) -1) (exp -1) -1 (/ (log x) n) (log x) x n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) 1 (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (pow (* n x) -1) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (+ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (/ (log x) n)) (* n x)) (exp (/ (log x) n))) |
| 393.0ms | 6 400× | 0 | valid |
Compiled 73 832 to 40 434 computations (45.2% saved)
ival-mult!: 143.0ms (71.8% of total)ival-add!: 55.0ms (27.6% of total)adjust: 1.0ms (0.5% of total)43 calls:
| 525.0ms | x |
| 237.0ms | b |
| 155.0ms | eps |
| 137.0ms | (-.f64 (cbrt.f64 (+.f64 x #s(literal 1 binary64))) (cbrt.f64 x)) |
| 79.0ms | a |
Compiled 1 842 to 1 723 computations (6.5% 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)
| 27× | node limit |
| 1× | saturated |
| 88× | binary-search |
| 17× | left-value |
| 81× | narrow-enough |
| 7× | predicate-same |
| 549.0ms | 5 162× | 0 | valid |
| 154.0ms | 801× | 1 | valid |
| 92.0ms | 1 329× | 0 | invalid |
| 78.0ms | 266× | 2 | valid |
| 2.0ms | 11× | 3 | valid |
| 1.0ms | 17× | 0 | exit |
Compiled 30 765 to 23 317 computations (24.2% saved)
ival-mult!: 215.0ms (33.8% of total)ival-pow: 95.0ms (14.9% of total)ival-div!: 71.0ms (11.1% of total)ival-sub!: 65.0ms (10.2% of total)adjust: 57.0ms (8.9% of total)ival-sqrt: 45.0ms (7.1% of total)ival-neg: 39.0ms (6.1% of total)ival-add!: 21.0ms (3.3% of total)ival-cos: 15.0ms (2.4% of total)ival-exp: 6.0ms (0.9% of total)ival-cbrt: 4.0ms (0.6% of total)ival-expm1: 4.0ms (0.6% of total)Loading profile data...