[PPL-devel] test if polyhedron satisfies a constraint

[P M Hill]

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.