[PPL-devel] Octagonal_Shape::affine_image too imprecise?

[Enea Zaffanella]

Il 18/10/2010 15:22, FABIO BOSSI ha scritto:
> Octagonal_Shape::affine_image seems a bit too imprecise when treating
> assignments of the form Y = -Y + c.

[...]

> This approach that discards all old binary constraints on the assigned
> variable looks a little too naive to me. Consider for instance this
> assigment sequence:
> 
> X = Y;
> Y = -Y;
> 
> The octagonal domain will not be able to deduce X + Y = 0 as I would
> expect.

Right, we had a useless precision loss.
I have just committed in an improved version.

> A similar problem probably exists for BD Shapes.

I don't think BD shapes are affected.
Sign-symmetry ( + translation ) maps sum constraints into difference
constraints and difference constraints into sum constraints; in either
case, the source constraint or the destination constraint can not be
encoded in a BD_Shape.

Enea.