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

[Étienne André]

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. 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