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

[Roberto Bagnara]

On 08/12/11 13:53, Benjamin Hiller wrote:
> Hello PPL developers,
>
> continuing a discussion I had with Prof. Bagnara:
>
> Am 10.08.2011 21:38, schrieb Roberto Bagnara:
>>> Am 10.08.2011 18:38, schrieb Roberto Bagnara:
>>>> 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.
>>>
>>> Our data should be such that each polyhedron is far from being
>>> degenerated so I don't think they will become empty due to rounding.
>>>
>>>> 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.
>
> Where in the documentation can I find the information which
> classes/operations are safe to use (ie not based on floats) without
> rounding and which not? I skimmed the online docs and was not able to
> figure this out myself.

Hi Benjamin.

The templatic abstractions (such as Box, BD_Shape, Octagonal_Shape)
instantiated with floating point types (float, double, long double)
are based on floats.  And so are all the abstractions that contain
the above (such as powersets and products).  All the other abstractions
are not based on floats.
Cheers,

    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