-------- Original Message -------- Subject: PPL and FPU rounding mode Date: Wed, 10 Aug 2011 16:12:32 +0200 From: Benjamin Hiller hiller@zib.de To: bagnara@cs.unipr.it
Dear Prof. Bagnara,
we are using your PPL in a research project and so far it perfectly suits our needs. Thank you for developing such a great piece of software and making it available for research.
There is a question I could not find enough details for on the web. I found out that using the functions restore_pre_PPL_rounding() and set_rounding_for_PPL() a user can manually decide when the conservative rounding mode assumed by PPL is in effect. The documentation states that "After calling restore_pre_PPL_rounding() it is absolutely necessary to call set_rounding_for_PPL() before using any PPL abstractions based on floating point numbers." to obtain correct results. Does this mean that if I do not set the PPL-rounding mode, all the results computed by PPL will be bogus? Or does it mean that they may be less accurate/correct approximations that are no longer suitable for proving something? (I understand that PPL has been used for verification where this issue is very important.) In our project, we use PPL to compute polyhedrons that are approximations anyway and some loss of accuracy would not hurt much. It is safe under these circumstances to just disable the rounding mode used by PPL?
Best regards,
Benjamin Hiller