Add support for computing the symbolic integer lexmin of a polyhedron.
This finds, for every assignment to the symbols, the lexicographically
minimum value attained by the dimensions. For example, the symbolic lexmin
of the set
(x, y)[a, b, c] : (a <= x, b <= x, x <= c)
can be written as
x = a if b <= a, a <= c x = b if a < b, b <= c
This also finds the set of assignments to the symbols that make the lexmin unbounded.
I would prefer not treating the relation as a set while producing this lexmin. Can we instead also treat the domain variables as parameters and have something like:
I think this is a more general case of what the current implementation produces.