w3ppl/htdocs/Documentation Documentation.raw f ...

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: roberto@cs.unipr.it 2001-10-18 08:32:35
Modified files: htdocs/Documentation: Documentation.raw Added files: htdocs/Documentation: fdl.raw gpl.raw
Log message: Licenses added. The documentation page is now complete.
Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/fdl.raw... http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/gpl.raw... http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/Documen...

Hi,
I wondered if there was a method for testing a given polyhedron to see if it implied that a certain constraint holds. I know I can insert the constraint and then test that the polyhedron is the same as before. That is how I have programmed this. But it seems to me that such a check would be a frequently used task - but I cannot find such a method.
BTW In Polyhedron.defs.hh, I found: //! Returns the relation between the generators of \p *this //! and the constraint \p con. GenSys_Con_Rel poly_satisfies_constraint(const Constraint& con);
but I am not sure what this is for.
ciao, Pat
PS I want to do this as I want the permute.cc program to prove that the permute does terminate - so it needs to check that the head argument is _indeed_ bigger that its recursive one in the body. This holds but it is nice to do this automatically.

On Thu, 18 Oct 2001, P M Hill wrote:
Hi,
BTW In Polyhedron.defs.hh, I found: //! Returns the relation between the generators of \p *this //! and the constraint \p con. GenSys_Con_Rel poly_satisfies_constraint(const Constraint& con);
but I am not sure what this is for.
Hi,
this method is uesd to verify if the generators of the polyhedron *this satisfy the constraint con.
Returns: - ALL_SATURATE if all generators belong to the hyper-plane defined by con (saturate con), - ALL_SATISFY if all generators satisfy con but do not belong to the hyper-plane defined by con, - NONE_SATISFIES if no generators satisfy con, - SOME_SATISFY if one or more generators do not satisfy con.
Ciao, Elisa

On Thu, 18 Oct 2001, Elisa Ricci wrote:
On Thu, 18 Oct 2001, P M Hill wrote:
Hi,
BTW In Polyhedron.defs.hh, I found: //! Returns the relation between the generators of \p *this //! and the constraint \p con. GenSys_Con_Rel poly_satisfies_constraint(const Constraint& con);
but I am not sure what this is for.
Hi,
this method is uesd to verify if the generators of the polyhedron *this satisfy the constraint con.
Returns:
- ALL_SATURATE if all generators belong to the hyper-plane defined by con (saturate con),
- ALL_SATISFY if all generators satisfy con but do not belong to the hyper-plane defined by con,
- NONE_SATISFIES if no generators satisfy con,
- SOME_SATISFY if one or more generators do not satisfy con.
Hi,
Which, if any of these flags mean that all points in the polyhedron satisfy the constraint? Also, I want to refer to a specific polyhedron.
ciao, Pat

P M Hill wrote:
Hi,
I wondered if there was a method for testing a given polyhedron to see if it implied that a certain constraint holds. I know I can insert the constraint and then test that the polyhedron is the same as before. That is how I have programmed this. But it seems to me that such a check would be a frequently used task
- but I cannot find such a method.
We are a bit careful at adding new methods not to clutter the library. This is not to say that the method you propose would not be useful However, today you want to check whether a constraint is entailed and tomorrow you want to check whether *two* constraints are entailed. The day after you realize that for termination is enough (besides other conditions) to have one argument whose size is strictly decreasing, so you want to check (among other things) whether
(*) x1 < y1 OR x2 < y2 OR ... OR xn < yn
You will thus negate (*) obtaining n constraints that you will add to a copy of your polyhedron. Then you will want to use Polyhedron::check_empty() to see whether (*) was entailed by the original polyhedron.
Moral: as long as the library allows you to do what you want in a reasonably simple and efficient way, then you should be happy. Any application will develop its own library of functions on top of the PPL: these will be those function that make sense for *that* application. Of course, we still want to add to the library those functions and methods that respond to very general needs. What do others think?
Roberto
participants (4)
-
Elisa Ricci
-
P M Hill
-
Roberto Bagnara
-
Roberto Bagnara