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@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel