[PPL-devel] Re: Convex hull

[Enrico Oliosi]

>
> I don't have the 1978 paper by Cousot & Halbwachs at hand.
> However, if I interpret correctly what you write, P-true is the
> entry condition to the true branch and P-false is the entry
> condition to the false branch.  So up to here we all agree.
>
> Where we disagree is that your annotations p1 and p2 still
> have the constraint `j = 0', which is wrong.  I don't know
> what you are doing.  What you should do is, I believe, to compute
> p1 as the affine image of P-true with respect to j = i+2 and
> p2 as the affine image of P-false with respect to j = i.
> These images would not have the constraints `j = 0' that
> you have.
>
> To summarize, here is what you should have and what I obtain
> with the PPL:
>
> *** P_true ***
> j = 0,
> i >= 0.
> *** P_false ***
> j = 0,
> -i > 0.
> *** After P_true.affine_image(j, i+2), call this p1 ***
> i - j = -2,
> j >= 2.
> *** After P_false.affine_image(j, i), call this p2 ***
> i - j = 0,
> -i > 0.
> *** After p1.poly_hull_assign_and_minimize(p2) ***
> i - j >= -2,
> -i + j >= 0.
>
> Please, let us know if this clarifies things enough.
> Ciao,
>
>      Roberto
>

Ok, I found the error. When I have a linear non invertible assign (like 
j:=i+2) I call 'ph.add_constraint(j == i+2)' in order to insert
a new constraint (I don't remember because I have done it.
Problably I though that an assignment introduced always a new constraint
to my polyhedra). I use 'affine_image' for linear invertible assign only
(for ex: i:=i+2).

Thanks Roberto, your help is more and more useful.

   Enrico.