[PPL-devel] Equality of 2 non-convex constraints?

[Enea Zaffanella]

Hello Étienne.


On 03/21/2017 04:17 PM, Étienne André wrote:
> Dear PPL developers,
>
> I have a problem with a non-regression test in my tool IMITATOR, that
> uses PPL for polyhedra operations.
> The new version of IMITATOR does not output the same result (say k2) as
> the former (and therefore expected) result (say k1). I use non-convex
> polyhedra, using the pointset powerset implementation, in Ocaml (the
> ppl_Pointset_Powerset_NNC_Polyhedron functions).
>
> The problem is that:
> - PPL says that that k2 is not equal to k1 (using function
> ppl_Pointset_Powerset_NNC_Polyhedron_equals_Pointset_Powerset_NNC_Polyhedron)
> - PPL says that k2 is not included in k1 (using function
> ppl_Pointset_Powerset_NNC_Polyhedron_contains_Pointset_Powerset_NNC_Polyhedron)
> - PPL says that k1 is not included in k2
> - PPL says that k2 \ k1 is empty (using
> ppl_Pointset_Powerset_NNC_Polyhedron_difference_assign)
> - PPL says that k1 \ k2 is empty
> So there is clearly a mismatch somewhere.

Not necessarily so.

The functions "equals" and "contains" are meant to compare the *sets* of 
polyhedra.
For instance, for the "contains", the (C++ interface) documentation says:

     Returns <CODE>true</CODE> if and only if each disjunct
     of \p y is contained in a disjunct of \p *this.

If you want to compare the *unions* of the two powersets, then you 
should use the functions named "geometrically_covers" and 
"geometrically_equals". The documentation for geometrically_covers says:

     Returns <CODE>true</CODE> if and only if \p *this geometrically
     covers \p y, i.e., if any point (in some element) of \p y is also
     a point (of some element) of \p *this

My guess is that, in your example, the two powerset are indeed 
geometrically equivalent, but not so as powersets.

Let us know if my guess is indeed correct or whether further 
investigation is needed.

Regards,
Enea.


> It could be in PPL, or it
> could be in the functions I use on top of PPL.
> The same version of PPL (1.1) was used in both versions of the tool, so
> the problem does not come from a change in PPL.
> I also did these checks in another (very basic) tool, using PPL 1.2,
> again from Ocaml, and I obtain the same results.
>
> How could I easily test whether the 2 following polyhedra are equal? Or,
> if not, what is a valuation of the variables that belongs to one but not
> to the other? I cannot use my own tool (relying on PPL) for the reasons
> cited above…
> E.g., could you use a simple interface (e.g., in C++) to perform the
> check k1 =?= k2?
>
> k1 :
>
> p_add_sugar > 0
> & p_button > p_add_sugar
> & p_add_sugar + p_coffee > p_button
> & 15 > p_button
> OR
> p_add_sugar >= p_button
> & 2*p_button > p_add_sugar
> & p_add_sugar + p_coffee > 2*p_button
> & 15 > 2*p_button
> OR
> p_add_sugar >= 2*p_button
> & p_add_sugar + p_coffee > 3*p_button
> & 3*p_button > p_add_sugar
> & 5 > p_button
> OR
> 15 > p_add_sugar + p_coffee
> & p_coffee > 0
> & p_button > 0
> & 5 > p_button
> & p_add_sugar >= 3*p_button
>
>
> k2 :
>   p_add_sugar > 0
>      & 2*p_button > p_add_sugar
>      & p_add_sugar + p_coffee > 2*p_button
>      & 15 > 2*p_button
>      & p_add_sugar > 0
>      & p_button > 0
>      & p_coffee > 0
>      OR
>        p_add_sugar >= 2*p_button
>      & p_add_sugar + p_coffee > 3*p_button
>      & 3*p_button > p_add_sugar
>      & 5 > p_button
>      & p_add_sugar > 0
>      & p_button > 0
>      & p_coffee > 0
>      OR
>        p_add_sugar > 0
>      & 2*p_button >= 15
>      & p_add_sugar + p_coffee > 15
>      & 15 > p_button
>      & p_button > p_add_sugar
>      & p_add_sugar > 0
>      & p_button > 0
>      & p_coffee > 0
>      OR
>        2*p_button >= p_add_sugar + p_coffee
>      & p_add_sugar > 0
>      & p_add_sugar + p_coffee > p_button
>      & p_button > p_add_sugar
>      & 15 >= p_add_sugar + p_coffee
>      & p_add_sugar > 0
>      & p_button > 0
>      & p_coffee > 0
>      OR
>        15 > p_add_sugar + p_coffee
>      & p_coffee > 0
>      & p_button > 0
>      & 5 > p_button
>      & p_add_sugar >= 3*p_button
>      & p_add_sugar > 0
>      & p_button > 0
>      & p_coffee > 0
>
>
> Thank you!
>
> Best,
>
> --
> Étienne André
> Université Paris 13
> http://lipn.univ-paris13.fr/~andre
>
> _______________________________________________
> PPL-devel mailing list
> PPL-devel at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel