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.