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