[PPL-devel] Re: A question on powerset operations

[Roberto Bagnara]

Hosung Song wrote:
> Would you verify the execution result of the following simple program?
> 
> ----
> #include	<ppl.hh>
> #include	<iostream>
> 
> using namespace Parma_Polyhedra_Library;
> using namespace IO_Operators;
> using namespace std;
> 
> int
> main(void)
> {
> 		Variable x(0);
> 
> 		ConSys cs1, cs2, cs3, cs4;
> 		cs1.insert(x >= 0);
> 		cs1.insert(x <= 4);
> 		cs2.insert(x >= 2);
> 		cs2.insert(x <= 6);
> 		cs3.insert(x >= 1);
> 		cs3.insert(x <= 5);
> 
> 		NNC_Polyhedron ph1(cs1), ph2(cs2), ph3(cs3);
> 		cout << "ph1 : " << ph1 << endl;
> 		cout << "ph2 : " << ph2 << endl;
> 		cout << "ph3 : " << ph3 << endl;
> 
> 		Polyhedra_PowerSet<NNC_Polyhedron> ps12(2,
> Polyhedron::EMPTY);
> 		ps12.add_disjunct(ph1);
> 		ps12.add_disjunct(ph2);
> 		cout << "ps12 : " << ps12 << endl;
> 
> 		if (check_containment(ph3, ps12))
> 				cout << "ph3 is contained in ps12..." <<
> endl;
> 		else
> 				cout << "ph3 is not contained in ps12..."
> << endl;
> }
> -------
> What I'm interested in is to check whether a polyhedron is contained by
> the union of a set of polyhedrons. So I played around with just
> Polyhedra_PowerSet class, by converting the single polyhedron to a
> set of a single polyhedron. I got some unexpected results, so I looked
> into the codes Polyhedra_PowerSet... and it seems like check_containment()
> is just the function I needed. I tried that and my result is still a
> little unexpected. Well, that's maybe only from my understanding, and that
> might be quite wrong. In the above example, ph1 is 0 <= x <= 4, and ph2 is
> 2 <= x <= 6. ps12 is the union of ph1 and ph2. ph3 is 1 <= x <= 5. So, it
> looks like ph3 is contained in ps12. However, my execution result is the
> other way. I used "g++ test.cc -lppl -lgmpxx -lgmp" and the running result
> is "ph3 is not contained in ps12..." Am I missing some basic understanding
> here? I suppose my understanding of the geometrical inclusion
> (containment or covering, whatever) might be seriously flawed. I'd try to
> trace the execution to understand the function
> completely, but I would greatly appreciate your quick insightful
> advice. Thanks always.

Dear Hosung,

you have indeed been bitten by a bug in PPL 0.6.1.  This was fixed on
September 15th, 2004, but we forgot to add a mention of it to our bugs
page (http://www.cs.unipr.it/ppl/Bugs/).  I have done it now, and there
you will also find a patch you can apply to PPL 0.6.1.  Sorry about that.

By the way, with lots of interesting new features and bug fixes, the
forthcoming release (0.7) contains several changes to the
Polyhedra_PowerSet template class (starting from its name, where the
's' is now lowercase).
All the best,

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it