Changes in _mpd_qexp():
-----------------------
1) Reduce the number of iterations in the Horner scheme for operands with
a negative adjusted exponent. Previously the number was overestimated
quite generously.
2) The function _mpd_get_exp_iterations() now has an ACL2 proof and
is rewritten accordingly.
3) The proof relies on abs(op) > 9 * 10**(-prec-1), so operands without
that property are now handled by the new function _mpd_qexp_check_one().
4) The error analysis for the evaluation of the truncated Taylor series
in Hull&Abrham's paper relies on the fact that the reduced operand
'r' has fewer than context.prec digits.
Since the operands may have more than context.prec digits, a new ACL2
proof covers the case that r.digits > context.prec. To facilitate the
proof, the Horner step now uses fma instead of rounding twice in
multiply/add.
Changes in mpd_qexp():
----------------------
1) Fix a bound in the correct rounding loop that was too optimistic. In
practice results were always correctly rounded, because it is unlikely
that the error in _mpd_qexp() ever reaches the theoretical maximum.
1 file changed