-------- Original Message -------- Subject: Re: [PPL-devel] floating point behaviour Date: Tue, 15 Jun 2010 17:30:12 -0400 From: piotrm piotrm@cs.umd.edu To: Roberto Bagnara bagnara@cs.unipr.it

That explains most of it. Thanks!

The man page suggest that the restore and set rounding mode are to be used merely if one relies on some rounding mode. I'm not interested in particular rounding modes. I am, however, interested in floats printed in such a way that they can be scanned back in as floats, and "0.:00000" is not an example of such a float. I did notice that restoring rounding mode lets one print floats "correctly" but I'm skeptical that restore/set rounding mode before / after printing things is the intended usage of ppl.

Thanks for the help,

Piotr

On Jun 15, 2010, at 16:48, Roberto Bagnara wrote:

On 06/15/2010 09:36 PM, piotrm wrote:

...

Apologies if this is not the right place to inquire about this, cannot seem to find any other outlet:

Hi piotrm,

you should check out the library documentation.

...

Is it correct behavior for floating point calculations to be done differently once ppl.hh is included in a c++ program as well as the printing of floats? Here is an example of what I'm referring to:

#include <cstdio>

int main() { double a = 0.50000000000000011102230246251565404236316680908203125; double b = 0.5f / a; printf("%0.60f %f %0.60f %f\n", a, a, b, b); return 0; }

This prints (for me)

0.500000000000000111022302462515654042363166809082031250000000 0.500000 0.999999999999999777955395074968691915273666381835937500000000 1.000000

If I include ppl, as in below:

#include <cstdio> #include "ppl.hh"

int main() { double a = 0.50000000000000011102230246251565404236316680908203125; double b = 0.5f / a; printf("%0.60f %f %0.60f %f\n", a, a, b, b); return 0; }

I get the following

0.500000000000000111022302462515654042363166809082031250000000 0.500000 0.999999999999999888977697537484345957636833190917968750000000 0.:00000

Notice the strange way the b is printed the second time. I also found instances where numbers that are close to 0.01 get printed as 0.00:000

Is this perhaps an installation issue on my part? I noticed this using the OCaml interface, that is, use of ppl changed the behavior of the float types in OCaml in the same way the behavior is changed in C++ above.

See the documentation of

void Parma_Polyhedra_Library::set_rounding_for_PPL() void Parma_Polyhedra_Library::restore_pre_PPL_rounding() void Parma_Polyhedra_Library::initialize() void Parma_Polyhedra_Library::finalize()

Use also `man libppl' to see the role played by the PPL_NO_AUTOMATIC_INITIALIZATION macro. All the best,

Roberto

-- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it