[PPL-devel] Fwd: PPL and FPU rounding mode

[Roberto Bagnara]

-------- Original Message --------
Subject: PPL and FPU rounding mode
Date: Wed, 10 Aug 2011 16:12:32 +0200
From: Benjamin Hiller <hiller at zib.de>
To: bagnara at 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
-- 
Benjamin Hiller                                           hiller at zib.de
Abteilung Optimierung                            phone +49 30 84185-406

Konrad-Zuse-Zentrum für Informationstechnik Berlin (ZIB)
Takustraße 7
14195 Berlin