How to do Powerset element normalization
Hello,
I am starting to use the closed convex polyhedra powerset domain for my PhD research. Since I want to use it from Haskell, I'm extending the C and Haskell bindings (built on top of the C interface to PPL version 0.6.1). So far I have managed to get a minimal interface working -- creating powersets, adding disjuncts and constraints and outputing results.
Now the question I have is: what is the prefered way to ensure that a powerset is Omega-reduced, i.e. all its elements are maximal wrt the original partial order (in particular, removing bottom elements)? Polyhedra_PowerSet<C_Polyhedron> has a member function `omega_reduce()' that is suposed to do just this, but it is protected, so the compiler complains if I try to use in the C interface. The only solution I found is to use `pairwise_reduce()' instead. It seems to do what I want, but I am confused as to the reason for the protected function.
Please excuse me (and please tell me!) if this is not the right forum to ask these questions.
Best regards,
Pedro Vasconcelos
Pedro Vasconcelos wrote:
I am starting to use the closed convex polyhedra powerset domain for my PhD research. Since I want to use it from Haskell, I'm extending the C and Haskell bindings (built on top of the C interface to PPL version 0.6.1). So far I have managed to get a minimal interface working -- creating powersets, adding disjuncts and constraints and outputing results.
Hello Pedro,
you may want to use the work of/share your work with Hosung Song, who is reading this in CC.
By the way, we (the PPL developers) are more and more curious about these Haskell bindings we have read about in some recent messages to the mailing list. It may come as a surprise to you, but we never saw them and we have not the slightest idea about how they look like. Can you give us a pointer?
Now the question I have is: what is the prefered way to ensure that a powerset is Omega-reduced, i.e. all its elements are maximal wrt the original partial order (in particular, removing bottom elements)? Polyhedra_PowerSet<C_Polyhedron> has a member function `omega_reduce()' that is suposed to do just this, but it is protected, so the compiler complains if I try to use in the C interface.
The interface for Polyhedra_Powerset is still experimental and we are still designing it. Since the release of PPL 0.6.1 we have been very busy doing other things (a good part of them PPL-related) and this part of the library has suffered a bit. It would be nice if we could take the occasion and work with you and Hosung towards improving and finishing this part of the work. This is especially important for us also in view of the new numerical abstractions we are about to add to the library: bounding boxes, bounded differences, octagons, grids, ... all of them can be used as arguments to the powerset construction.
So, let us start with your question. Premise number 1 is that I am not against providing `omega_reduce()' to the user of Polyhedra_Powerset. Premise number 2 is that I prefer to be extra-sure providing `omega_reduce()' to the user of Polyhedra_Powerset is the right thing to do. The obvious question I have to ask you is: why would you want to have access to `omega_reduce()? What is the effect you wish to obtain? Afterall, one may say that a Polyhedra_Powerset and its omega-reduced counterparts have the same semantics. (You can of course reply, and rightly so, "Why do you provide pairwise_reduce() then?" This only shows that the interface of powersets needs more work: perhaps [I am being provocative here] `pairwise_reduce()' should not be there.)
To make a parallel with a similar situation with the C_Polyhedron and NNC_Polyhedron classes, we do not provide a method `minimize()' to the user. We rather ask the user to declare what is wanted by calling `miminized_constraints()' or `minimized_generators()' and keep polyhedra minimization as an internal business the user needs not be concerned about. Up to now, this design choice has proved its value without showing any drawback.
To come back to the point you raise: is `omega_reduction()' precisely the things you want, or is it just something that either as a by product or in combination with other techniques will give you what you really want? In the latter case, what is that you really want? Do you want reduction to economize memory? To use less space when printing? Because you think subsequent operations will be cheaper?
The only solution I found is to use `pairwise_reduce()' instead. It seems to do what I want, but I am confused as to the reason for the protected function.
The method `pairwise_reduce()' does a different thing (please consult the documentation and complain if it does not provide enough information). And moreover, it is quite expensive.
Please excuse me (and please tell me!) if this is not the right forum to ask these questions.
This is _precisely_ the right forum for these questions. All the best,
Roberto
On Tue, 09 Nov 2004 21:50:57 +0100 Roberto Bagnara bagnara@cs.unipr.it wrote:
By the way, we (the PPL developers) are more and more curious about these Haskell bindings we have read about in some recent messages to the mailing list. It may come as a surprise to you, but we never saw them and we have not the slightest idea about how they look like. Can you give us a pointer?
The bindings are just Haskell library code that calls the PPL C interface functions. It also defines Haskell wrapper types for (pointers to) the PPL data objects. So effectively the Haskell interface in built on top of the C one.
Axel Simon wrote the basic Haskell interface code and I got it from him. He didn't made publicly available because the
Now the question I have is: what is the prefered way to ensure that a powerset is Omega-reduced, i.e. all its elements are maximal wrt the original partial order (in particular, removing bottom elements)? Polyhedra_PowerSet<C_Polyhedron> has a member function `omega_reduce()' that is suposed to do just this, but it is protected, so the compiler complains if I try to use in the C interface.
The interface for Polyhedra_Powerset is still experimental and we are still designing it. Since the release of PPL 0.6.1 we have been very busy doing other things (a good part of them PPL-related) and this part of the library has suffered a bit. It would be nice if we could take the occasion and work with you and Hosung towards improving and finishing this part of the work. This is especially important for us also in view of the new numerical abstractions we are about to add to the library: bounding boxes, bounded differences, octagons, grids, ... all of them can be used as arguments to the powerset construction.
So, let us start with your question. Premise number 1 is that I am not against providing `omega_reduce()' to the user of Polyhedra_Powerset. Premise number 2 is that I prefer to be extra-sure providing `omega_reduce()' to the user of Polyhedra_Powerset is the right thing to do. The obvious question I have to ask you is: why would you want to have access to `omega_reduce()? What is the effect you wish to obtain? Afterall, one may say that a Polyhedra_Powerset and its omega-reduced counterparts have the same semantics. (You can of course reply, and rightly so, "Why do you provide pairwise_reduce() then?" This only shows that the interface of powersets needs more work: perhaps [I am being provocative here] `pairwise_reduce()' should not be there.)
To make a parallel with a similar situation with the C_Polyhedron and NNC_Polyhedron classes, we do not provide a method `minimize()' to the user. We rather ask the user to declare what is wanted by calling `miminized_constraints()' or `minimized_generators()' and keep polyhedra minimization as an internal business the user needs not be concerned about. Up to now, this design choice has proved its value without showing any drawback.
To come back to the point you raise: is `omega_reduction()' precisely the things you want, or is it just something that either as a by product or in combination with other techniques will give you what you really want? In the latter case, what is that you really want? Do you want reduction to economize memory? To use less space when printing? Because you think subsequent operations will be cheaper?
The only solution I found is to use `pairwise_reduce()' instead. It seems to do what I want, but I am confused as to the reason for the protected function.
The method `pairwise_reduce()' does a different thing (please consult the documentation and complain if it does not provide enough information). And moreover, it is quite expensive.
Please excuse me (and please tell me!) if this is not the right forum to ask these questions.
This is _precisely_ the right forum for these questions. 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@cs.unipr.it _______________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
[ Sorry about my last incomplete reply. Here it is in full ]
On Tue, 09 Nov 2004 21:50:57 +0100 Roberto Bagnara bagnara@cs.unipr.it wrote:
By the way, we (the PPL developers) are more and more curious about these Haskell bindings we have read about in some recent messages to the mailing list. It may come as a surprise to you, but we never saw them and we have not the slightest idea about how they look like. Can you give us a pointer?
The bindings are just Haskell library code that calls the PPL C interface functions. It also defines Haskell wrapper types for (pointers to) the PPL data objects. So effectively the Haskell interface in built on top of the C one and you get the same API as with C.
Axel Simon wrote the basic Haskell interface code and I got it from him. He didn't made publicly available because he came across a bug he couldn't resolve. It turned out to be of a memory allocation conflict which I managed to get around it by linking the PPL with a private version of libgmp. This is still a bit of a hack, so I don't know if Axel has made it available yet on his web page. For me, I'd much prefer to use Haskell than C/C++ or Prolog, so that's incentive enough to get it working...
So, let us start with your question. Premise number 1 is that I am not against providing `omega_reduce()' to the user of Polyhedra_Powerset. Premise number 2 is that I prefer to be extra-sure providing `omega_reduce()' to the user of Polyhedra_Powerset is the right thing to do. The obvious question I have to ask you is: why would you want to have access to `omega_reduce()? What is the effect you wish to obtain? Afterall, one may say that a Polyhedra_Powerset and its omega-reduced counterparts have the same semantics.
True, I should be more explict: I only need omega_reduce() before converting constraints to a Haskell representation after a sequence of polyhedral computations. The constraints should be simplified for pretty printing and because they will eventually get replicated. I know I could just leave them in the PPL world, but I prefer to use the PPL as a "black box" solver and get an observable value out (at least for the time being).
To make a parallel with a similar situation with the C_Polyhedron and NNC_Polyhedron classes, we do not provide a method `minimize()' to the user. We rather ask the user to declare what is wanted by calling `miminized_constraints()' or `minimized_generators()' and keep polyhedra minimization as an internal business the user needs not be concerned about. Up to now, this design choice has proved its value without showing any drawback.
Yes, but I could not find an analogous operation for Powersets. I am using minimzed_constraints() for each powerset element, but (of course) that doesn't eliminate redundant elements (for example: bottom elements).
The method `pairwise_reduce()' does a different thing (please consult the documentation and complain if it does not provide enough information). And moreover, it is quite expensive.
Yes, I thought as much!
Thanks for your thorough reply,
Pedro Vasconcelos
Pedro Vasconcelos wrote:
True, I should be more explict: I only need omega_reduce() before converting constraints to a Haskell representation after a sequence of polyhedral computations. The constraints should be simplified for pretty printing and because they will eventually get replicated. I know I could just leave them in the PPL world, but I prefer to use the PPL as a "black box" solver and get an observable value out (at least for the time being).
Dear Pedro,
you can find a snapshot of PPL 0.7 at the address
http://www.cs.unipr.it/ppl/Download/ftp/snapshots/
In that snapshot, omega_reduce() is available to the users of the Polyhedra_Powerset class. Notice that we are still discussing whether this is the right way to provide the functionality you are (quite rightly) asking for. So in future releases the same functionality may be available in other forms, but what is important now is to let you can go on with your work.
Notice that in PPL 0.7 we are renaming things in order to be consistent. Beware of the lowercase 's' in Powerset and, should you get an error because something named *_dimension* is undeclared, try *_space_dimension* instead. Please do not hesitate to come back to us if needed. All the best,
Roberto
Roberto Bagnara wrote:
you can find a snapshot of PPL 0.7 at the address
Dear Pedro,
the snapshot that was present in that location contained a giant memory leak that has now been fixed. A revised, correct snapshot is now available from there. All the best,
Roberto
participants (3)
-
Pedro Vasconcelos -
Pedro Vasconcelos -
Roberto Bagnara