[PPL-devel] PPL functions and methods [Was: test if polyhedron satisfies a constraint]

[Roberto Bagnara]

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

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