


Bits error versus t
Results
Initial program 0.0
rmApplied add-log-exp0.0
rmApplied add-log-exp0.0
Final simplification0.0
herbie shell --seed 2019016
(FPCore (t)
:name "Kahan p13 Example 1"
(/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))))
Time bar (total: 1.7m)Debug log
| 256× | (pre true 80) |
| 256× | (body real 80) |
| 517.0ms | (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
1 alts after pruning (1 fresh and 0 done)
Merged error: 0.0b
Found 4 expressions with local error:
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 0.0b | (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 0.0b | (/ (* 2 t) (+ 1 t)) |
| 32× | add-exp-log |
| 32× | add-cbrt-cube |
| 24× | times-frac |
| 22× | add-cube-cbrt |
| 22× | *-un-lft-identity |
| 22× | add-sqr-sqrt |
| 18× | associate-*l* |
| 18× | associate-*r* |
| 14× | pow1 |
| 12× | associate-/r/ |
| 10× | div-exp |
| 10× | cbrt-undiv |
| 8× | cbrt-unprod |
| 8× | prod-exp |
| 7× | flip-+ |
| 7× | flip3-+ |
| 6× | div-inv |
| 6× | associate-/r* |
| 4× | add-log-exp |
| 4× | associate-/l* |
| 2× | associate-/l/ |
| 2× | pow-prod-up |
| 2× | *-commutative |
| 2× | associate-*r/ |
| 2× | associate-*l/ |
| 2× | pow-prod-down |
| 2× | pow-plus |
| 2× | frac-2neg |
| 2× | clear-num |
| 2× | frac-times |
| 2× | pow2 |
| 24.0ms | (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 12.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 8.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 6.0ms | (/ (* 2 t) (+ 1 t)) |
| 31.0ms | (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 20.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 13.0ms | (/ (* 2 t) (+ 1 t)) |
| 12.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 874.0ms | (* (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) |
| 794.0ms | (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (cbrt (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))))) |
| 734.0ms | (* (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) |
| 719.0ms | (+ (* 2 2) (- (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (* 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))))) |
| 602.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
3 alts after pruning (3 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 1.6b | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 0.0b | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 28× | add-exp-log |
| 28× | add-cbrt-cube |
| 18× | associate-*l* |
| 18× | associate-*r* |
| 15× | pow1 |
| 13× | add-cube-cbrt |
| 13× | *-un-lft-identity |
| 13× | add-sqr-sqrt |
| 12× | times-frac |
| 8× | cbrt-unprod |
| 8× | associate-/r/ |
| 8× | prod-exp |
| 8× | div-exp |
| 8× | cbrt-undiv |
| 7× | add-log-exp |
| 4× | div-inv |
| 4× | flip-+ |
| 4× | flip3-+ |
| 3× | log-pow |
| 3× | log-prod |
| 2× | pow-prod-up |
| 2× | *-commutative |
| 2× | associate-*r/ |
| 2× | associate-*l/ |
| 2× | pow-prod-down |
| 2× | exp-to-pow |
| 2× | pow-plus |
| 2× | exp-prod |
| 2× | frac-times |
| 2× | pow2 |
| 1× | rem-exp-log |
| 1× | rem-log-exp |
| 15.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 8.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 6.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 5.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 32.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 18.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 13.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 12.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 748.0ms | (* (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) |
| 710.0ms | (* (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) |
| 545.0ms | (log (sqrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))))) |
| 531.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 523.0ms | (+ (log (/ (* 2 t) (+ 1 t))) (- (log (* 2 t)) (log (+ 1 t)))) |
2 alts after pruning (2 fresh and 0 done)
Merged error: 0b
Found 4 expressions with local error:
| 1.6b | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 1.6b | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 0.0b | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 0.0b | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 10× | add-log-exp |
| 6× | add-cube-cbrt |
| 6× | log-pow |
| 6× | *-un-lft-identity |
| 6× | log-prod |
| 6× | pow1 |
| 6× | add-sqr-sqrt |
| 4× | add-exp-log |
| 4× | exp-to-pow |
| 4× | add-cbrt-cube |
| 4× | exp-prod |
| 2× | rem-exp-log |
| 2× | rem-log-exp |
| 3.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 3.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 3.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 3.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 42.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 40.0ms | (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 25.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 18.0ms | (log (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) |
| 584.0ms | (log (* (cbrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (cbrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))))) |
| 563.0ms | (log (sqrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))))) |
| 544.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 527.0ms | (log (* (cbrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (cbrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))))) |
| 518.0ms | (log (sqrt (exp (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))))) |
2 alts after pruning (1 fresh and 1 done)
Merged error: 0b
Found 4 expressions with local error:
| 0.1b | (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 0.0b | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 170× | add-exp-log |
| 170× | add-cbrt-cube |
| 77× | cbrt-unprod |
| 77× | prod-exp |
| 76× | pow1 |
| 52× | div-exp |
| 52× | cbrt-undiv |
| 28× | associate-*l* |
| 28× | associate-*r* |
| 26× | pow-prod-up |
| 21× | pow-prod-down |
| 20× | frac-times |
| 18× | times-frac |
| 16× | add-cube-cbrt |
| 16× | *-un-lft-identity |
| 16× | add-sqr-sqrt |
| 15× | pow-plus |
| 14× | associate-*r/ |
| 14× | associate-*l/ |
| 12× | associate-/r/ |
| 12× | pow2 |
| 6× | div-inv |
| 6× | flip-+ |
| 6× | flip3-+ |
| 4× | add-log-exp |
| 4× | *-commutative |
| 30.0ms | (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 14.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 13.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 9.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 28.0ms | (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 22.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 21.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 21.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 1.2s | (* (* (+ 1 t) (+ 1 t)) (* (+ 1 t) (+ 1 t))) |
| 1.1s | (* (* (/ (* (* (* 2 t) (* 2 t)) (* 2 t)) (* (* (+ 1 t) (+ 1 t)) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) (* (/ (* (* (* 2 t) (* 2 t)) (* 2 t)) (* (* (+ 1 t) (+ 1 t)) (+ 1 t))) (/ (* (* (* 2 t) (* 2 t)) (* 2 t)) (* (* (+ 1 t) (+ 1 t)) (+ 1 t))))) |
| 906.0ms | (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) |
| 845.0ms | (* (* (* 2 t) (/ (* 2 t) (+ 1 t))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) |
| 830.0ms | (* (* (/ (* (* (* 2 t) (* 2 t)) (* 2 t)) (* (* (+ 1 t) (+ 1 t)) (+ 1 t))) (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)))) (* (* (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t))) (/ (* (* (* 2 t) (* 2 t)) (* 2 t)) (* (* (+ 1 t) (+ 1 t)) (+ 1 t))))) |
2 alts after pruning (0 fresh and 2 done)
Merged error: 0b
0% (0.0b remaining)
Error of 0.0b against oracle of 0.0b and baseline of 0.0b
| 8000× | (pre true 80) |
| 8000× | (body real 80) |