



Bits error versus n
Results
| Original | 63.0 |
|---|---|
| Target | 0 |
| Herbie | 0 |
Initial program 63.0
Taylor expanded around inf 0.0
Simplified0.0
Taylor expanded around inf 0.0
Simplified0
Final simplification0
herbie shell --seed 1137770271
(FPCore (n)
:name "logs (example 3.8)"
:pre (> n 6.8e+15)
:herbie-target
(- (log (+ n 1)) (- (/ 1 (* 2 n)) (- (/ 1 (* 3 (* n n))) (/ 4 (pow n 3)))))
(- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1))
Time bar (total: 23.3s)Debug log
| 106× | 125.0ms | (body real 1280) |
| 83× | 69.0ms | (body real 640) |
| 53× | 53.0ms | (body real 320) |
| 256× | 9.0ms | (pre true 80) |
| 14× | 5.0ms | (body real 160) |
| 307.0ms | (- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 63.0b
Found 3 expressions with local error:
| 5.1b | (- (* (+ n 1) (log (+ n 1))) (* n (log n))) |
| 0.3b | (* (+ n 1) (log (+ n 1))) |
| 0.3b | (* n (log n)) |
| 12× | log-prod |
| 10× | add-cube-cbrt |
| 10× | *-un-lft-identity |
| 10× | add-sqr-sqrt |
| 7× | associate-*r* |
| 6× | associate--l+ |
| 6× | distribute-lft-in |
| 6× | pow1 |
| 6× | distribute-rgt-in |
| 5× | add-log-exp |
| 5× | add-exp-log |
| 5× | add-cbrt-cube |
| 3× | associate-*l* |
| 2× | *-commutative |
| 2× | associate-*l/ |
| 1× | flip-- |
| 1× | flip-+ |
| 1× | cbrt-unprod |
| 1× | log-pow |
| 1× | prod-exp |
| 1× | pow-prod-down |
| 1× | diff-log |
| 1× | flip3-- |
| 1× | flip3-+ |
| 1× | sub-neg |
| 17.0ms | (- (* (+ n 1) (log (+ n 1))) (* n (log n))) |
| 11.0ms | (* (+ n 1) (log (+ n 1))) |
| 7.0ms | (* n (log n)) |
| 350.0ms | (* n (log n)) |
| 195.0ms | (- (* (+ n 1) (log (+ n 1))) (* n (log n))) |
| 60.0ms | (* (+ n 1) (log (+ n 1))) |
| 1.2s | (- (+ 1 (* 1/2 (/ 1 n))) (+ (* n (log (/ 1 n))) (log (/ 1 n)))) |
| 1.0s | (- (+ (* n (log -1)) (+ 1 (+ (log -1) (* 1/2 (/ 1 n))))) (+ (* n (log (/ -1 n))) (log (/ -1 n)))) |
| 907.0ms | (- (+ 1 (* 1/2 (/ 1 n))) (+ (* 1/6 (/ 1 (pow n 2))) (log (/ 1 n)))) |
| 624.0ms | (* (log (* (cbrt (+ n 1)) (cbrt (+ n 1)))) (+ n 1)) |
| 564.0ms | (- (+ n (* 1/2 (pow n 2))) (+ (* n (log n)) (* 1/6 (pow n 3)))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.0b
Found 3 expressions with local error:
| 0.5b | (/ 1/6 (* n n)) |
| 0.0b | (- (+ (+ 1 (log n)) (- (/ 1/2 n) (/ 1/6 (* n n)))) 1) |
| 0.0b | (+ 1 (log n)) |
| 4× | add-sqr-sqrt |
| 3× | add-log-exp |
| 3× | add-cube-cbrt |
| 3× | add-exp-log |
| 3× | add-cbrt-cube |
| 3× | *-un-lft-identity |
| 3× | pow1 |
| 1× | flip-- |
| 1× | div-inv |
| 1× | flip-+ |
| 1× | associate--l+ |
| 1× | difference-of-sqr-1 |
| 1× | flip3-- |
| 1× | flip3-+ |
| 1× | frac-2neg |
| 1× | sub-neg |
| 1× | associate-/r* |
| 1× | associate-+r- |
| 1× | clear-num |
| 1× | +-commutative |
| 1× | associate--l- |
| 293.0ms | (- (+ (+ 1 (log n)) (- (/ 1/2 n) (/ 1/6 (* n n)))) 1) |
| 4.0ms | (+ 1 (log n)) |
| 1.0ms | (/ 1/6 (* n n)) |
| 452.0ms | (+ 1 (log n)) |
| 61.0ms | (- (+ (+ 1 (log n)) (- (/ 1/2 n) (/ 1/6 (* n n)))) 1) |
| 39.0ms | (/ 1/6 (* n n)) |
| 492.0ms | (- (+ (log -1) (* 1/2 (/ 1 n))) (+ (* 1/6 (/ 1 (pow n 2))) (log (/ -1 n)))) |
| 294.0ms | (+ (sqrt (+ (+ 1 (log n)) (- (/ 1/2 n) (/ 1/6 (* n n))))) 1) |
| 254.0ms | (- (* 1/2 (/ 1 n)) (+ (* 1/6 (/ 1 (pow n 2))) (log (/ 1 n)))) |
| 153.0ms | (- (+ (log n) (* 1/2 (/ 1 n))) (* 1/6 (/ 1 (pow n 2)))) |
| 127.0ms | (- (+ (log -1) 1) (log (/ -1 n))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0b
Found 1 expressions with local error:
| 0.5b | (/ 1/6 (* n n)) |
| 1× | add-log-exp |
| 1× | div-inv |
| 1× | add-cube-cbrt |
| 1× | add-exp-log |
| 1× | add-cbrt-cube |
| 1× | *-un-lft-identity |
| 1× | frac-2neg |
| 1× | associate-/r* |
| 1× | clear-num |
| 1× | pow1 |
| 1× | add-sqr-sqrt |
| 2.0ms | (/ 1/6 (* n n)) |
| 28.0ms | (/ 1/6 (* n n)) |
| 8.0ms | (/ 1/6 (pow n 2)) |
| 7.0ms | (/ 1/6 (pow n 2)) |
| 7.0ms | (/ 1/6 (pow n 2)) |
1 alts after pruning (0 fresh and 1 done)
Merged error: 0b
| 3542× | 5.4s | (body real 1280) |
| 2639× | 2.7s | (body real 640) |
| 1399× | 993.0ms | (body real 320) |
| 8000× | 369.0ms | (pre true 80) |
| 420× | 182.0ms | (body real 160) |