On 08/10/11 16:29, Roberto Bagnara wrote:

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.

Thanks Benjamin: it is much appreciated.

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?

If you call restore_pre_PPL_rounding() reset the rounding mode to its default (typically round-to-nearest) AND you use a PPL abstraction based on floating point numbers without first calling set_rounding_for_PPL() then the result computed by PPL will be bogus. For example, you may have a non-empty box be mistaken for empty. Of course, you may be lucky, but I would not count on that.

(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?

Which PPL classes are you using? Many PPL classes are not based on floating point numbers. If you only use those, then there is no problem at all, whatever rounding mode is in effect. Cheers,

Roberto