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.