Herbie run
| Date: | Friday, April 11th, 2025 |
|---|---|
| Commit: | ccb5c8ad on chassis-platforms-cleanup |
| Seed: | 2025101 |
| Parameters: | 256 points for 4 iterations |
| Flags: | reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs default |
| Memory: | 138 998.8 MB |
Time bar (total: 2.3min)
| 25.8s | 44 550× | 2 | valid |
| 16.5s | 96 775× | 1 | valid |
| 13.8s | 145 970× | 0 | invalid |
| 9.8s | 5 785× | 5 | exit |
| 7.7s | 86 244× | 0 | valid |
| 2.5s | 3 595× | 3 | valid |
| 680.0ms | 1 106× | 1 | exit |
| 362.0ms | 4 047× | 0 | exit |
| 132.0ms | 137× | 4 | exit |
| 5.0ms | 4× | 4 | valid |
| 4.0ms | 2× | 2 | exit |
ival-tan: 11.7s (18.6% of total)ival-pow: 9.8s (15.5% of total)adjust: 6.3s (10% of total)ival-cos: 4.3s (6.8% of total)ival-mult!: 3.9s (6.2% of total)ival-log: 3.8s (5.9% of total)ival-div!: 3.7s (5.8% of total)ival-add!: 3.3s (5.2% of total)ival-sin: 3.2s (5% of total)ival-exp: 2.3s (3.7% of total)ival-sub!: 2.2s (3.4% of total)ival-expm1: 2.1s (3.3% of total)ival-fabs: 1.4s (2.2% of total)ival-log1p: 1.2s (2% of total)ival-sqrt: 1.1s (1.8% of total)ival-neg: 785.0ms (1.2% of total)ival-<: 579.0ms (0.9% of total)ival-<=: 441.0ms (0.7% of total)ival-atan: 334.0ms (0.5% of total)ival-and: 333.0ms (0.5% of total)ival-cbrt: 315.0ms (0.5% of total)ival-assert: 69.0ms (0.1% of total)ival-fmin: 62.0ms (0.1% of total)ival->: 1.0ms (0% of total)exact: 0.0ms (0% of total)| 244× | iter-limit |
| 98× | node-limit |
| Operator | Subexpression | Explanation | Count | |
|---|---|---|---|---|
-.f64 | #f | cancellation | 4253 | 30 |
log.f64 | #f | sensitivity | 768 | 0 |
/.f64 | #f | u/u | 419 | 0 |
sqrt.f64 | #f | oflow-rescue | 414 | 0 |
+.f64 | #f | cancellation | 333 | 0 |
/.f64 | #f | u/n | 114 | 0 |
pow.f64 | (pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n)) | sensitivity | 57 | 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 | 28 | 0 |
| ↳ | (*.f64 b eps) | underflow | 125 | |
| ↳ | (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) | underflow | 130 | |
| ↳ | (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)) | underflow | 125 | |
| ↳ | (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))) | underflow | 232 | |
| ↳ | (*.f64 a eps) | underflow | 130 | |
sqrt.f64 | #f | uflow-rescue | 26 | 0 |
-.f64 | #f | nan-rescue | 15 | 0 |
/.f64 | (/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x)) | n/o | 4 | 0 |
| ↳ | (*.f64 x x) | overflow | 57 | |
exp.f64 | #f | sensitivity | 2 | 1 |
cos.f64 | (cos.f64 (+.f64 x eps)) | sensitivity | 1 | 0 |
/.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 - | |
|---|---|---|
| + | 5225 | 15 |
| - | 153 | 1775 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 5225 | 13 | 2 |
| - | 153 | 17 | 1758 |
| number | freq |
|---|---|
| 0 | 1790 |
| 1 | 4560 |
| 2 | 643 |
| 3 | 111 |
| 4 | 64 |
| Predicted + | Predicted Maybe | Predicted - | |
|---|---|---|---|
| + | 28 | 0 | 0 |
| - | 0 | 0 | 0 |
| 1.6s | 2 834× | 2 | valid |
| 909.0ms | 6 060× | 1 | valid |
| 384.0ms | 5 232× | 0 | valid |
| 117.0ms | 210× | 3 | valid |
Compiled 2 154 to 763 computations (64.6% saved)
ival-tan: 626.0ms (26.9% of total)adjust: 309.0ms (13.3% of total)ival-cos: 228.0ms (9.8% of total)ival-div!: 190.0ms (8.2% of total)ival-log: 180.0ms (7.7% of total)ival-exp: 135.0ms (5.8% of total)ival-sin: 126.0ms (5.4% of total)ival-pow: 116.0ms (5% of total)ival-mult!: 84.0ms (3.6% of total)ival-sub!: 78.0ms (3.4% of total)ival-log1p: 69.0ms (3% of total)ival-sqrt: 66.0ms (2.8% of total)ival-add!: 47.0ms (2% of total)ival-expm1: 23.0ms (1% of total)ival-atan: 20.0ms (0.9% of total)ival-cbrt: 16.0ms (0.7% of total)ival-neg: 14.0ms (0.6% of total)Compiled 1 240 858 to 139 441 computations (88.8% saved)
| 18× | fuel |
| 10× | done |
Compiled 8 438 to 1 641 computations (80.6% saved)
468 calls:
| Time | Variable | Point | Expression | |
|---|---|---|---|---|
| 94.0ms | x | @ | -inf | ((- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* (pow x 4/3) 1/3) (* -1/9 (cbrt x))) (* x x)) (+ (* (pow x -5/3) -1/9) (* (* (pow (cbrt x) -1) (pow (cbrt x) -1)) 1/3)) (pow x -5/3) x -5/3 -1/9 (* (* (pow (cbrt x) -1) (pow (cbrt x) -1)) 1/3) (* (pow (cbrt x) -1) (pow (cbrt x) -1)) (pow (cbrt x) -1) (cbrt x) -1 1/3 (- (cbrt (+ x 1)) (cbrt x)) (* (exp (* (log x) -2/3)) 1/3) (exp (* (log x) -2/3)) (* (log x) -2/3) (log x) -2/3 (- (cbrt (+ x 1)) (cbrt x)) (* (pow (pow (cbrt x) 2) -1) 1/3) (pow (pow (cbrt x) 2) -1) (pow (cbrt x) 2) 2 (- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* (pow x 4/3) 1/3) (* -1/9 (cbrt x))) (* x x)) (+ (* (pow x -2/3) 1/3) (* (pow x -5/3) -1/9)) (pow x -2/3) (* (pow x -5/3) -1/9) (- (cbrt (+ x 1)) (cbrt x)) (/ (+ (* (pow x 4/3) 1/3) (* -1/9 (cbrt x))) (* x x)) (+ (* (pow x -5/3) -1/9) (* (* (cbrt (pow x -1)) (cbrt (pow x -1))) 1/3)) (* (* (cbrt (pow x -1)) (cbrt (pow x -1))) 1/3) (* (cbrt (pow x -1)) (cbrt (pow x -1))) (cbrt (pow x -1)) (pow x -1)) |
| 65.0ms | n | @ | 0 | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) n) (- (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (/ (pow (log (+ 1 x)) 2) n) (pow (log (+ 1 x)) 2) (log (+ 1 x)) x 2 n 1/2 (+ (* (/ (pow (log x) 2) n) 1/2) (log x)) (/ (pow (log x) 2) n) (pow (log x) 2) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (pow (* n x) -1) (* n x) -1 (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (+ 1 x) 1 (- (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)) (/ (exp (neg (/ (neg (log x)) n))) n) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (- (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)) (+ (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)) (+ (* -1 (/ (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) (* n n))) (* -1/2 (/ (pow (log x) 2) n))) (/ (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) (* n n)) (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) 1/24 (/ (pow (log x) 4) n) (pow (log x) 4) 4 (* 1/6 (pow (log x) 3)) 1/6 (pow (log x) 3) 3 (* n n) (* -1/2 (/ (pow (log x) 2) n)) -1/2) |
| 61.0ms | n | @ | inf | ((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) n) (- (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) (+ (* (/ (pow (log (+ 1 x)) 2) n) 1/2) (log (+ 1 x))) (/ (pow (log (+ 1 x)) 2) n) (pow (log (+ 1 x)) 2) (log (+ 1 x)) x 2 n 1/2 (+ (* (/ (pow (log x) 2) n) 1/2) (log x)) (/ (pow (log x) 2) n) (pow (log x) 2) (log x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (pow (* n x) -1) (* n x) -1 (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (+ 1 x) 1 (- (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)) (/ (exp (neg (/ (neg (log x)) n))) n) (exp (neg (/ (neg (log x)) n))) (neg (/ (neg (log x)) n)) (/ (neg (log x)) n) (neg (log x)) (- (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)) (+ (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)) (+ (* -1 (/ (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) (* n n))) (* -1/2 (/ (pow (log x) 2) n))) (/ (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) (* n n)) (+ (* 1/24 (/ (pow (log x) 4) n)) (* 1/6 (pow (log x) 3))) 1/24 (/ (pow (log x) 4) n) (pow (log x) 4) 4 (* 1/6 (pow (log x) 3)) 1/6 (pow (log x) 3) 3 (* n n) (* -1/2 (/ (pow (log x) 2) n)) -1/2) |
| 51.0ms | N | @ | inf | ((- (log (+ 1 (pow N -3))) (log (+ 1 (- (pow N -2) (pow N -1))))) (log (+ 1 (pow N -3))) (pow N -3) N -3 (log (+ 1 (- (pow N -2) (pow N -1)))) (- (pow N -2) (pow N -1)) (/ (- (exp (neg (log N))) 1) N) (- (exp (neg (log N))) 1) (neg (log N)) (log N) (log (+ 1 (exp (neg (log N))))) (exp (neg (log N))) (log (+ 1 (pow (pow N -1/2) 2))) (pow (pow N -1/2) 2) (pow N -1/2) -1/2 2 (- (log (+ N 1)) (log N)) (/ (+ (/ (- (/ 1/3 N) 1/2) N) 1) N) (/ (+ (* (- N 1/2) N) 1/3) (pow N 3)) (+ (* (- N 1/2) N) 1/3) (- N 1/2) 1/2 1/3 (pow N 3) 3 (- (log (+ N 1)) (log N)) (/ (+ 1 (/ (+ (* (+ (* -1/2 N) 1/3) N) -1/4) (pow N 3))) N) (+ 1 (/ (+ (* (+ (* -1/2 N) 1/3) N) -1/4) (pow N 3))) 1 (/ (+ (* (+ (* -1/2 N) 1/3) N) -1/4) (pow N 3)) (+ (* (+ (* -1/2 N) 1/3) N) -1/4) (+ (* -1/2 N) 1/3) -1/4) |
| 48.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)) |
| 26× | node-limit |
| 2× | saturated |
Compiled 19 254 to 4 980 computations (74.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)
43 calls:
| 479.0ms | x |
| 280.0ms | eps |
| 120.0ms | b_2 |
| 104.0ms | a |
| 103.0ms | b |
Compiled 1 748 to 1 671 computations (4.4% saved)
Compiled 74 603 to 37 550 computations (49.7% saved)
| 91× | binary-search |
| 21× | left-value |
| 91× | narrow-enough |
| 388.0ms | 4 397× | 0 | valid |
| 135.0ms | 656× | 2 | valid |
| 133.0ms | 1 238× | 1 | valid |
| 68.0ms | 1 067× | 0 | invalid |
| 13.0ms | 29× | 3 | valid |
| 3.0ms | 44× | 0 | exit |
| 0.0ms | 2× | 1 | exit |
Compiled 34 396 to 26 164 computations (23.9% saved)
ival-mult!: 141.0ms (29.1% of total)ival-sqrt: 71.0ms (14.7% of total)ival-pow: 70.0ms (14.5% of total)ival-div!: 54.0ms (11.1% of total)adjust: 52.0ms (10.7% of total)ival-neg: 32.0ms (6.6% of total)ival-sub!: 30.0ms (6.2% of total)ival-add!: 15.0ms (3.1% of total)ival-exp: 5.0ms (1% of total)ival-cos: 5.0ms (1% of total)ival-atan: 4.0ms (0.8% of total)ival-cbrt: 3.0ms (0.6% of total)ival-expm1: 2.0ms (0.4% of total)Loading profile data...