[PPL-devel] Fwd: Re: floating point behaviour

[Roberto Bagnara]

-------- Original Message --------
Subject: Re: [PPL-devel] floating point behaviour
Date: Tue, 15 Jun 2010 17:30:12 -0400
From: piotrm <piotrm at cs.umd.edu>
To: Roberto Bagnara <bagnara at 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 at cs.unipr.it