Enea Zaffanella wrote:
At this point we have that:
a) both the con_sys and the gen_sys do represent the same NNC-polyhedron b) the gen_sys is NNC-minimized c) the con_sys is minimized, but it might be NNC-redundant d) gen_sys and con_sys might represent DIFFERENT (n+1-space-dim) closed polyhedra.
Note in particular points a) and d). This situation could be exploited positively: we could add further status flags to the polyhedron, to remember that the con_sys is both up-to-date and minimized, but it is not NNC-minimized, while the gen_sys is NNC-minimized (which implies the other two).
This is why we have a Status class in the first place: to make it simple to add new introspective capabilities to the polyhedra classes. The idea of distinguishing between minimization and NNC-minimization looks promising (even though the name "NNC-minimization" is horrible ;-)
Clearly, we have to be careful with this "partial" misalignment of con_sys and gen_sys ... they are NOT the dual of each other! In particular, in such a situation the saturation matrices will NOT be up-to-date (as far as I can see).
So, a first question for Elisa: as things are now, do we ever "assume" that whenever both con_sys and gen_sys are minimized, then the saturation matrices are up-to-date ?
We never assume that consciously (i.e., if the actual code happens to rely on that assumptiom, then it is a bug).
Roberto