



Bits error versus a




Bits error versus b




Bits error versus eps
Results
| Original | 58.7 |
|---|---|
| Target | 14.4 |
| Herbie | 3.7 |
if b < -1.003997533940732e+224Initial program 49.3
Taylor expanded around 0 61.8
Simplified55.1
Taylor expanded around 0 12.3
rmApplied frac-add20.7
Simplified20.7
if -1.003997533940732e+224 < b Initial program 59.2
Taylor expanded around 0 56.1
Simplified54.8
Taylor expanded around 0 2.8
Final simplification3.7
herbie shell --seed 323378853
(FPCore (a b eps)
:name "expq3 (problem 3.4.2)"
:pre (and (< -1 eps) (< eps 1))
:herbie-target
(/ (+ a b) (* a b))
(/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))))
Time bar (total: 58.8s)Debug log
| 254.0ms | 80× | body | 2560 | valid |
| 236.0ms | 64× | body | 10240 | exit |
| 229.0ms | 112× | body | 1280 | valid |
| 51.0ms | 38× | body | 640 | valid |
| 16.0ms | 322× | pre | 80 | true |
| 8.0ms | 8× | body | 320 | valid |
| 6.0ms | 19× | body | 80 | valid |
| 1.0ms | 1× | body | 160 | valid |
| 322.0ms | (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 57.8b
Found 4 expressions with local error:
| 5.3b | (- (exp (* (+ a b) eps)) 1) |
| 3.2b | (- (exp (* b eps)) 1) |
| 2.5b | (- (exp (* a eps)) 1) |
| 0.2b | (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)) |
| 11× | add-sqr-sqrt |
| 9× | flip-- |
| 9× | flip3-- |
| 6× | add-cube-cbrt |
| 6× | add-exp-log |
| 6× | add-cbrt-cube |
| 6× | *-un-lft-identity |
| 6× | pow1 |
| 5× | difference-of-sqr-1 |
| 5× | sub-neg |
| 4× | add-log-exp |
| 4× | associate-*l* |
| 4× | associate-*r* |
| 4× | frac-times |
| 2× | associate-*r/ |
| 2× | associate-*l/ |
| 2× | distribute-lft-in |
| 2× | distribute-rgt-in |
| 1× | cbrt-unprod |
| 1× | *-commutative |
| 1× | prod-exp |
| 1× | pow-prod-down |
| 44.0ms | (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)) |
| 14.0ms | (- (exp (* (+ a b) eps)) 1) |
| 10.0ms | (- (exp (* a eps)) 1) |
| 10.0ms | (- (exp (* b eps)) 1) |
| 76.0ms | (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1)) |
| 76.0ms | (- (exp (* (+ a b) eps)) 1) |
| 51.0ms | (- (exp (* a eps)) 1) |
| 47.0ms | (- (exp (* b eps)) 1) |
| 796.0ms | (* (* (* (- (exp (* a eps)) 1) (- (exp (* a eps)) 1)) (- (exp (* a eps)) 1)) (* (* (- (exp (* b eps)) 1) (- (exp (* b eps)) 1)) (- (exp (* b eps)) 1))) |
| 730.0ms | (* (+ (exp (* a eps)) 1) (+ (* (exp (* b eps)) (exp (* b eps))) (+ (* 1 1) (* (exp (* b eps)) 1)))) |
| 470.0ms | (+ (* eps b) (+ (* 1/2 (* (pow eps 2) (pow b 2))) (* 1/6 (* (pow eps 3) (pow b 3))))) |
| 466.0ms | (+ (* 1/2 (* (pow a 2) (pow eps 2))) (+ (* 1/6 (* (pow a 3) (pow eps 3))) (* a eps))) |
| 415.0ms | (* (- (* (exp (* a eps)) (exp (* a eps))) (* 1 1)) (- (exp (* b eps)) 1)) |
4 alts after pruning (4 fresh and 0 done)
Merged error: 45.5b
Found 4 expressions with local error:
| 5.3b | (- (exp (* (+ a b) eps)) 1) |
| 2.9b | (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))))) |
| 2.5b | (- (exp (* a eps)) 1) |
| 2.5b | (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))) |
| 11× | add-exp-log |
| 11× | add-cbrt-cube |
| 9× | flip-- |
| 9× | flip3-- |
| 9× | add-sqr-sqrt |
| 8× | associate-/r/ |
| 8× | frac-times |
| 6× | flip-+ |
| 6× | add-cube-cbrt |
| 6× | associate-*r/ |
| 6× | flip3-+ |
| 6× | *-un-lft-identity |
| 6× | pow1 |
| 4× | add-log-exp |
| 4× | associate-*l/ |
| 4× | associate-*l* |
| 3× | associate-*r* |
| 3× | difference-of-sqr-1 |
| 2× | associate-/l/ |
| 2× | cbrt-unprod |
| 2× | prod-exp |
| 2× | div-exp |
| 2× | sub-neg |
| 2× | cbrt-undiv |
| 1× | associate-/l* |
| 1× | div-inv |
| 1× | *-commutative |
| 1× | pow-prod-down |
| 1× | times-frac |
| 1× | distribute-lft-in |
| 1× | frac-2neg |
| 1× | associate-/r* |
| 1× | clear-num |
| 1× | distribute-rgt-in |
| 41.0ms | (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))))) |
| 32.0ms | (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))) |
| 19.0ms | (- (exp (* (+ a b) eps)) 1) |
| 10.0ms | (- (exp (* a eps)) 1) |
| 2.2s | (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))))) |
| 252.0ms | (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))) |
| 72.0ms | (- (exp (* (+ a b) eps)) 1) |
| 49.0ms | (- (exp (* a eps)) 1) |
| 892.0ms | (* (+ (exp (* a eps)) 1) (+ (* (* eps b) (* eps b)) (- (* (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))) (* (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))))) |
| 778.0ms | (/ (* (* (* eps (- (exp (* (+ a b) eps)) 1)) (* eps (- (exp (* (+ a b) eps)) 1))) (* eps (- (exp (* (+ a b) eps)) 1))) (* (* (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))) (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))))) (* (- (exp (* a eps)) 1) (+ (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))))) |
| 700.0ms | (- (+ (/ (exp (* (+ a b) eps)) (* (- (* 1/6 (exp (* a eps))) 1/6) (* (pow b 3) (pow eps 2)))) (+ (* 1/2 (/ (exp (* a eps)) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow b 4) (pow eps 3))))) (* 1/2 (/ (exp (* (+ a b) eps)) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow b 4) (pow eps 3))))))) (+ (* 1/2 (/ (* (exp (* (+ a b) eps)) (exp (* a eps))) (* (pow eps 3) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (pow b 4))))) (+ (/ 1 (* (- (* 1/6 (exp (* a eps))) 1/6) (* (pow eps 2) (pow b 3)))) (* 1/2 (/ 1 (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow eps 3) (pow b 4)))))))) |
| 692.0ms | (- (+ (/ (exp (* (+ a b) eps)) (* (- (* 1/6 (exp (* a eps))) 1/6) (* (pow b 3) (pow eps 2)))) (+ (* 1/2 (/ (exp (* a eps)) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow b 4) (pow eps 3))))) (* 1/2 (/ (exp (* (+ a b) eps)) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow b 4) (pow eps 3))))))) (+ (* 1/2 (/ (* (exp (* (+ a b) eps)) (exp (* a eps))) (* (pow eps 3) (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (pow b 4))))) (+ (/ 1 (* (- (* 1/6 (exp (* a eps))) 1/6) (* (pow eps 2) (pow b 3)))) (* 1/2 (/ 1 (* (pow (- (* 1/6 (exp (* a eps))) 1/6) 2) (* (pow eps 3) (pow b 4)))))))) |
| 592.0ms | (* (+ (* (exp (* a eps)) (exp (* a eps))) (+ (* 1 1) (* (exp (* a eps)) 1))) (+ (* (* eps b) (* eps b)) (- (* (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2))) (* (* eps b) (* (* (* eps b) (* eps b)) (+ (* b (* 1/6 eps)) 1/2)))))) |
4 alts after pruning (4 fresh and 0 done)
Merged error: 0.0b
Found 1 expressions with local error:
| 0.0b | (+ (/ 1 a) (/ 1 b)) |
| 5× | *-un-lft-identity |
| 4× | distribute-lft-out |
| 4× | div-inv |
| 3× | add-log-exp |
| 1× | flip-+ |
| 1× | add-cube-cbrt |
| 1× | add-exp-log |
| 1× | frac-add |
| 1× | add-cbrt-cube |
| 1× | flip3-+ |
| 1× | sum-log |
| 1× | +-commutative |
| 1× | pow1 |
| 1× | add-sqr-sqrt |
| 8.0ms | (+ (/ 1 a) (/ 1 b)) |
| 14.0ms | (+ (/ 1 a) (/ 1 b)) |
| 11.0ms | (* (exp (/ 1 a)) (exp (/ 1 b))) |
| 5.0ms | (+ (/ 1 a) (/ 1 b)) |
| 5.0ms | (+ (/ 1 b) (/ 1 a)) |
| 5.0ms | (+ (/ 1 a) (/ 1 b)) |
| 5.0ms | (+ (/ 1 a) (/ 1 b)) |
5 alts after pruning (4 fresh and 1 done)
Merged error: 0.0b
Found 1 expressions with local error:
| 15.8b | (/ (+ b a) (* a b)) |
| 3× | associate-/l* |
| 3× | add-cube-cbrt |
| 3× | add-exp-log |
| 3× | add-cbrt-cube |
| 3× | times-frac |
| 3× | *-un-lft-identity |
| 3× | add-sqr-sqrt |
| 2× | associate-/l/ |
| 1× | add-log-exp |
| 1× | div-inv |
| 1× | flip-+ |
| 1× | div-exp |
| 1× | flip3-+ |
| 1× | frac-2neg |
| 1× | associate-/r* |
| 1× | clear-num |
| 1× | cbrt-undiv |
| 1× | pow1 |
| 7.0ms | (/ (+ b a) (* a b)) |
| 40.0ms | (/ (+ b a) (* a b)) |
| 126.0ms | (/ (* (* (+ b a) (+ b a)) (+ b a)) (* (* (* a b) (* a b)) (* a b))) |
| 34.0ms | (- (log (+ b a)) (log (* a b))) |
| 24.0ms | (- (* b b) (* a a)) |
| 13.0ms | (/ (* (cbrt (+ b a)) (cbrt (+ b a))) a) |
| 7.0ms | (+ (/ 1 a) (/ 1 b)) |
5 alts after pruning (3 fresh and 2 done)
Merged error: 0.0b
-13.1% (3.6b remaining)
Error of 3.7b against oracle of 0.1b and baseline of 3.2b
| 8.8s | 2595× | body | 2560 | valid |
| 7.7s | 3423× | body | 1280 | valid |
| 7.3s | 2006× | body | 10240 | exit |
| 1.7s | 1052× | body | 640 | valid |
| 819.0ms | 355× | body | 320 | valid |
| 647.0ms | 10009× | pre | 80 | true |
| 170.0ms | 433× | body | 80 | valid |
| 123.0ms | 145× | body | 160 | valid |