



Bits error versus x




Bits error versus eps
Results
| Original | 36.6 |
|---|---|
| Target | 14.9 |
| Herbie | 15.3 |
if eps < -2.6387393587202694e-37Initial program 29.7
rmApplied tan-sum2.5
rmApplied flip3--2.5
Applied associate-/r/2.5
Simplified2.5
rmApplied add-log-exp2.7
rmApplied distribute-lft-in2.7
Applied associate--l+2.7
if -2.6387393587202694e-37 < eps < 5.782469297289403e-19Initial program 45.4
rmApplied tan-sum45.4
rmApplied flip3--45.4
Applied associate-/r/45.4
Simplified45.4
Taylor expanded around 0 31.3
Simplified31.2
if 5.782469297289403e-19 < eps Initial program 29.0
rmApplied tan-sum1.0
rmApplied flip3--1.1
Applied associate-/r/1.1
Simplified1.1
rmApplied add-cbrt-cube1.2
Applied add-cbrt-cube1.2
Applied cbrt-unprod1.2
Applied rem-cube-cbrt1.1
Simplified1.1
Final simplification15.3
herbie shell --seed 2019022
(FPCore (x eps)
:name "2tan (problem 3.3.2)"
:herbie-target
(/ (sin eps) (* (cos x) (cos (+ x eps))))
(- (tan (+ x eps)) (tan x)))
Time bar (total: 1.3m)Debug log
| 163.0ms | 97× | body | 1280 | valid |
| 105.0ms | 66× | body | 640 | valid |
| 64.0ms | 21× | body | 2560 | valid |
| 12.0ms | 19× | body | 320 | valid |
| 9.0ms | 37× | body | 80 | valid |
| 8.0ms | 16× | body | 160 | valid |
| 7.0ms | (- (tan (+ x eps)) (tan x)) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 38.3b
Found 2 expressions with local error:
| 3.9b | (tan (+ x eps)) |
| 1.3b | (- (tan (+ x eps)) (tan x)) |
| 4× | add-log-exp |
| 4× | tan-quot |
| 4× | *-un-lft-identity |
| 4× | add-sqr-sqrt |
| 2× | add-cube-cbrt |
| 2× | frac-sub |
| 2× | add-exp-log |
| 2× | add-cbrt-cube |
| 2× | tan-sum |
| 2× | pow1 |
| 1× | difference-of-squares |
| 1× | distribute-lft-out-- |
| 1× | flip-- |
| 1× | diff-log |
| 1× | flip3-- |
| 1× | sub-neg |
| 10.0ms | (- (tan (+ x eps)) (tan x)) |
| 3.0ms | (tan (+ x eps)) |
| 98.0ms | (tan (+ x eps)) |
| 98.0ms | (- (tan (+ x eps)) (tan x)) |
| 177.0ms | (- (* (+ (tan x) (tan eps)) (cos x)) (* (- 1 (* (tan x) (tan eps))) (sin x))) |
| 133.0ms | (+ (* x (pow eps 2)) (+ eps (* (pow x 2) eps))) |
| 132.0ms | (* (- 1 (* (tan x) (tan eps))) (cos x)) |
| 53.0ms | (+ x (+ (* 1/3 (pow x 3)) eps)) |
| 13.0ms | (- (* (sin (+ x eps)) (cos x)) (* (cos (+ x eps)) (sin x))) |
8 alts after pruning (8 fresh and 0 done)
Merged error: 17.4b
Found 4 expressions with local error:
| 2.9b | (- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x)) |
| 0.2b | (* (tan x) (tan eps)) |
| 0.1b | (+ (tan x) (tan eps)) |
| 0.1b | (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) |
| 27× | *-un-lft-identity |
| 20× | add-sqr-sqrt |
| 15× | add-cube-cbrt |
| 13× | times-frac |
| 9× | tan-quot |
| 8× | add-log-exp |
| 8× | add-exp-log |
| 8× | add-cbrt-cube |
| 6× | pow1 |
| 5× | distribute-lft-out |
| 4× | associate-/l* |
| 3× | associate-/l/ |
| 3× | associate-*l* |
| 3× | associate-*r* |
| 3× | associate-/r* |
| 2× | difference-of-squares |
| 2× | flip-- |
| 2× | flip-+ |
| 2× | associate-/r/ |
| 2× | frac-add |
| 2× | flip3-- |
| 2× | flip3-+ |
| 1× | distribute-lft-out-- |
| 1× | div-inv |
| 1× | cbrt-unprod |
| 1× | frac-sub |
| 1× | *-commutative |
| 1× | associate-*r/ |
| 1× | prod-exp |
| 1× | associate-*l/ |
| 1× | pow-prod-down |
| 1× | div-exp |
| 1× | diff-log |
| 1× | frac-2neg |
| 1× | sub-neg |
| 1× | sum-log |
| 1× | clear-num |
| 1× | +-commutative |
| 1× | cbrt-undiv |
| 1× | frac-times |
| 27.0ms | (- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x)) |
| 11.0ms | (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) |
| 4.0ms | (* (tan x) (tan eps)) |
| 3.0ms | (+ (tan x) (tan eps)) |
| 390.0ms | (- (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) (tan x)) |
| 235.0ms | (/ (+ (tan x) (tan eps)) (- 1 (* (tan x) (tan eps)))) |
| 128.0ms | (+ (tan x) (tan eps)) |
| 95.0ms | (* (tan x) (tan eps)) |
| 306.0ms | (/ (* (* (+ (tan x) (tan eps)) (+ (tan x) (tan eps))) (+ (tan x) (tan eps))) (* (* (- 1 (* (tan x) (tan eps))) (- 1 (* (tan x) (tan eps)))) (- 1 (* (tan x) (tan eps))))) |
| 253.0ms | (+ (* 1/3 (* (pow x 3) eps)) (+ (* 1/3 (* x (pow eps 3))) (* x eps))) |
| 226.0ms | (- (+ (/ (sin eps) (* (cos eps) (- 1 (/ (* (sin x) (sin eps)) (* (cos x) (cos eps)))))) (/ (sin x) (* (cos x) (- 1 (/ (* (sin x) (sin eps)) (* (cos x) (cos eps))))))) (/ (sin x) (cos x))) |
| 222.0ms | (- (+ (/ (sin eps) (* (cos eps) (- 1 (/ (* (sin x) (sin eps)) (* (cos x) (cos eps)))))) (/ (sin x) (* (cos x) (- 1 (/ (* (sin x) (sin eps)) (* (cos x) (cos eps))))))) (/ (sin x) (cos x))) |
| 180.0ms | (- (* (+ (tan x) (tan eps)) (cos x)) (* (- 1 (* (tan x) (tan eps))) (sin x))) |
14 alts after pruning (14 fresh and 0 done)
Merged error: 17.2b
Found 4 expressions with local error:
| 2.9b | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 0.3b | (pow (* (tan x) (tan eps)) 3) |
| 0.3b | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 0.2b | (* (tan x) (tan eps)) |
| 233× | tan-quot |
| 119× | frac-times |
| 89× | associate-*r/ |
| 65× | frac-sub |
| 60× | frac-add |
| 58× | associate-*l/ |
| 36× | pow1 |
| 32× | flip-+ |
| 32× | flip3-+ |
| 21× | add-exp-log |
| 21× | add-cbrt-cube |
| 15× | pow-prod-down |
| 10× | cbrt-unprod |
| 10× | prod-exp |
| 6× | add-log-exp |
| 6× | add-cube-cbrt |
| 6× | *-un-lft-identity |
| 6× | add-sqr-sqrt |
| 4× | pow-prod-up |
| 4× | associate-*l* |
| 4× | associate-*r* |
| 3× | cube-div |
| 2× | rem-cube-cbrt |
| 2× | *-commutative |
| 2× | associate--l+ |
| 2× | pow-exp |
| 2× | pow-plus |
| 2× | pow-pow |
| 1× | flip-- |
| 1× | cube-prod |
| 1× | unpow3 |
| 1× | diff-log |
| 1× | flip3-- |
| 1× | distribute-lft-in |
| 1× | unpow-prod-down |
| 1× | sub-neg |
| 1× | pow-to-exp |
| 1× | cube-mult |
| 1× | distribute-rgt-in |
| 1× | pow2 |
| 87.0ms | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 16.0ms | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 4.0ms | (* (tan x) (tan eps)) |
| 3.0ms | (pow (* (tan x) (tan eps)) 3) |
| 1.7s | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 132.0ms | (pow (* (tan x) (tan eps)) 3) |
| 111.0ms | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 92.0ms | (* (tan x) (tan eps)) |
| 756.0ms | (- (* (* (+ (tan x) (tan eps)) (+ (* (+ (pow 1 3) (pow (* (tan eps) (tan x)) 3)) (* (cos x) (cos x))) (* (+ (* 1 1) (- (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* 1 (* (tan eps) (tan x))))) (* (* (tan eps) (sin x)) (* (tan eps) (sin x)))))) (cos x)) (* (* (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)) (* (+ (* 1 1) (- (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* 1 (* (tan eps) (tan x))))) (* (cos x) (cos x)))) (sin x))) |
| 607.0ms | (- (* (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (* (tan x) (tan eps)) 3))) (+ (* (+ (pow 1 3) (pow (* (tan eps) (tan x)) 3)) (* (* (cos eps) (cos x)) (cos x))) (* (+ (* 1 1) (- (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* 1 (* (tan eps) (tan x))))) (* (* (sin eps) (sin x)) (* (tan eps) (sin x)))))) (cos x)) (* (* (+ (* 1 1) (- (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* 1 (* (tan eps) (tan x))))) (* (* (cos eps) (cos x)) (cos x))) (sin x))) |
| 607.0ms | (* (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))) (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x)))) |
| 554.0ms | (* (* (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)) (* (- 1 (* (tan eps) (tan x))) (* (cos x) (* (cos eps) (cos x))))) (cos x)) |
| 477.0ms | (* (* (- (pow 1 3) (pow (* (tan x) (tan eps)) 3)) (* (- 1 (* (tan eps) (tan x))) (* (cos x) (cos eps)))) (cos x)) |
17 alts after pruning (17 fresh and 0 done)
Merged error: 17.2b
Found 4 expressions with local error:
| 2.9b | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (log (exp (* (tan x) (tan eps)))) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 2.4b | (log (exp (* (tan x) (tan eps)))) |
| 0.3b | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 0.2b | (* (tan x) (tan eps)) |
| 229× | tan-quot |
| 118× | frac-times |
| 88× | associate-*r/ |
| 65× | frac-sub |
| 60× | frac-add |
| 57× | associate-*l/ |
| 34× | pow1 |
| 32× | flip-+ |
| 32× | flip3-+ |
| 18× | add-exp-log |
| 18× | add-cbrt-cube |
| 14× | pow-prod-down |
| 9× | cbrt-unprod |
| 9× | prod-exp |
| 7× | add-log-exp |
| 7× | add-cube-cbrt |
| 7× | *-un-lft-identity |
| 7× | add-sqr-sqrt |
| 4× | pow-prod-up |
| 4× | associate-*l* |
| 4× | associate-*r* |
| 3× | log-pow |
| 3× | log-prod |
| 2× | *-commutative |
| 2× | associate--l+ |
| 2× | pow-plus |
| 1× | flip-- |
| 1× | rem-log-exp |
| 1× | diff-log |
| 1× | exp-to-pow |
| 1× | flip3-- |
| 1× | distribute-lft-in |
| 1× | sub-neg |
| 1× | exp-prod |
| 1× | distribute-rgt-in |
| 1× | pow2 |
| 47.0ms | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (log (exp (* (tan x) (tan eps)))) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 15.0ms | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 4.0ms | (* (tan x) (tan eps)) |
| 2.0ms | (log (exp (* (tan x) (tan eps)))) |
| 1.1s | (- (* (/ (+ (tan x) (tan eps)) (- (pow 1 3) (pow (log (exp (* (tan x) (tan eps)))) 3))) (+ (+ 1 (* (tan eps) (tan x))) (* (* (tan eps) (tan x)) (* (tan eps) (tan x))))) (tan x)) |
| 86.0ms | (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) |
| 75.0ms | (log (exp (* (tan x) (tan eps)))) |
| 73.0ms | (* (tan x) (tan eps)) |
| 531.0ms | (* (* (- (pow 1 3) (pow (log (exp (* (tan x) (tan eps)))) 3)) (* (- 1 (* (tan eps) (tan x))) (* (cos eps) (cos x)))) (cos x)) |
| 450.0ms | (* (* (- 1 (* (tan eps) (tan x))) (* (cos x) (cos eps))) (cos x)) |
| 379.0ms | (* (* (* (* (tan eps) (tan eps)) (tan eps)) (* (* (tan x) (tan x)) (tan x))) (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x)))) |
| 357.0ms | (* (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))) (* (* (* (tan eps) (tan eps)) (tan eps)) (* (* (tan x) (tan x)) (tan x)))) |
| 345.0ms | (* (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x))) (* (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* (tan eps) (tan x)))) |
18 alts after pruning (18 fresh and 0 done)
Merged error: 17.2b
89.9% (0.7b remaining)
Error of 15.3b against oracle of 14.5b and baseline of 21.7b
| 4.5s | 3261× | body | 1280 | valid |
| 2.1s | 1824× | body | 640 | valid |
| 1.8s | 651× | body | 2560 | valid |
| 448.0ms | 790× | body | 320 | valid |
| 198.0ms | 1115× | body | 80 | valid |
| 184.0ms | 359× | body | 160 | valid |