1 # Copyright 2014 MINES ParisTech
2 #
3 # This file is part of LinPy.
4 #
5 # LinPy is free software: you can redistribute it and/or modify
7 # the Free Software Foundation, either version 3 of the License, or
8 # (at your option) any later version.
9 #
10 # LinPy is distributed in the hope that it will be useful,
11 # but WITHOUT ANY WARRANTY; without even the implied warranty of
12 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 # GNU General Public License for more details.
14 #
15 # You should have received a copy of the GNU General Public License
16 # along with LinPy. If not, see <http://www.gnu.org/licenses/>.
18 import functools
19 import math
20 import numbers
22 from . import islhelper
24 from .islhelper import mainctx, libisl
25 from .geometry import GeometricObject, Point
26 from .linexprs import LinExpr, Rational
27 from .domains import Domain
30 __all__ = [
31 'Polyhedron',
32 'Lt', 'Le', 'Eq', 'Ne', 'Ge', 'Gt',
33 'Empty', 'Universe',
34 ]
37 class Polyhedron(Domain):
38 """
39 A convex polyhedron (or simply "polyhedron") is the space defined by a
40 system of linear equalities and inequalities. This space can be unbounded. A
41 Z-polyhedron (simply called "polyhedron" in LinPy) is the set of integer
42 points in a convex polyhedron.
43 """
45 __slots__ = (
46 '_equalities',
47 '_inequalities',
48 '_symbols',
49 '_dimension',
50 )
52 def __new__(cls, equalities=None, inequalities=None):
53 """
54 Return a polyhedron from two sequences of linear expressions: equalities
55 is a list of expressions equal to 0, and inequalities is a list of
56 expressions greater or equal to 0. For example, the polyhedron
57 0 <= x <= 2, 0 <= y <= 2 can be constructed with:
59 >>> x, y = symbols('x y')
60 >>> square1 = Polyhedron([], [x, 2 - x, y, 2 - y])
61 >>> square1
62 And(0 <= x, x <= 2, 0 <= y, y <= 2)
64 It may be easier to use comparison operators LinExpr.__lt__(),
65 LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
66 Le(), Eq(), Ge() and Gt(), using one of the following instructions:
68 >>> x, y = symbols('x y')
69 >>> square1 = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
70 >>> square1 = Le(0, x, 2) & Le(0, y, 2)
72 It is also possible to build a polyhedron from a string.
74 >>> square1 = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
76 Finally, a polyhedron can be constructed from a GeometricObject
77 instance, calling the GeometricObject.aspolyedron() method. This way, it
78 is possible to compute the polyhedral hull of a Domain instance, i.e.,
79 the convex hull of two polyhedra:
81 >>> square1 = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
82 >>> square2 = Polyhedron('1 <= x <= 3, 1 <= y <= 3')
83 >>> Polyhedron(square1 | square2)
84 And(0 <= x, 0 <= y, x <= y + 2, y <= x + 2, x <= 3, y <= 3)
85 """
86 if isinstance(equalities, str):
87 if inequalities is not None:
88 raise TypeError('too many arguments')
89 return cls.fromstring(equalities)
90 elif isinstance(equalities, GeometricObject):
91 if inequalities is not None:
92 raise TypeError('too many arguments')
93 return equalities.aspolyhedron()
94 sc_equalities = []
95 if equalities is not None:
96 for equality in equalities:
97 if not isinstance(equality, LinExpr):
98 raise TypeError('equalities must be linear expressions')
99 sc_equalities.append(equality.scaleint())
100 sc_inequalities = []
101 if inequalities is not None:
102 for inequality in inequalities:
103 if not isinstance(inequality, LinExpr):
104 raise TypeError('inequalities must be linear expressions')
105 sc_inequalities.append(inequality.scaleint())
106 symbols = cls._xsymbols(sc_equalities + sc_inequalities)
107 islbset = cls._toislbasicset(sc_equalities, sc_inequalities, symbols)
108 return cls._fromislbasicset(islbset, symbols)
110 @property
111 def equalities(self):
112 """
113 The tuple of equalities. This is a list of LinExpr instances that are
114 equal to 0 in the polyhedron.
115 """
116 return self._equalities
118 @property
119 def inequalities(self):
120 """
121 The tuple of inequalities. This is a list of LinExpr instances that are
122 greater or equal to 0 in the polyhedron.
123 """
124 return self._inequalities
126 @property
127 def constraints(self):
128 """
129 The tuple of constraints, i.e., equalities and inequalities. This is
130 semantically equivalent to: equalities + inequalities.
131 """
132 return self._equalities + self._inequalities
134 @property
135 def polyhedra(self):
136 return self,
138 def make_disjoint(self):
139 return self
141 def isuniverse(self):
142 islbset = self._toislbasicset(self.equalities, self.inequalities,
143 self.symbols)
144 universe = bool(libisl.isl_basic_set_is_universe(islbset))
145 libisl.isl_basic_set_free(islbset)
146 return universe
148 def aspolyhedron(self):
149 return self
151 def convex_union(self, *others):
152 """
153 Return the convex union of two or more polyhedra.
154 """
155 for other in others:
156 if not isinstance(other, Polyhedron):
157 raise TypeError('arguments must be Polyhedron instances')
158 return Polyhedron(self.union(*others))
160 def __contains__(self, point):
161 if not isinstance(point, Point):
162 raise TypeError('point must be a Point instance')
163 if self.symbols != point.symbols:
164 raise ValueError('arguments must belong to the same space')
165 for equality in self.equalities:
166 if equality.subs(point.coordinates()) != 0:
167 return False
168 for inequality in self.inequalities:
169 if inequality.subs(point.coordinates()) < 0:
170 return False
171 return True
173 def subs(self, symbol, expression=None):
174 equalities = [equality.subs(symbol, expression)
175 for equality in self.equalities]
176 inequalities = [inequality.subs(symbol, expression)
177 for inequality in self.inequalities]
178 return Polyhedron(equalities, inequalities)
180 def asinequalities(self):
181 """
182 Express the polyhedron using inequalities, given as a list of
183 expressions greater or equal to 0.
184 """
185 inequalities = list(self.equalities)
186 inequalities.extend([-expression for expression in self.equalities])
187 inequalities.extend(self.inequalities)
188 return inequalities
190 def widen(self, other):
191 """
192 Compute the standard widening of two polyhedra, à la Halbwachs.
194 In its current implementation, this method is slow and should not be
195 used on large polyhedra.
196 """
197 if not isinstance(other, Polyhedron):
198 raise TypeError('argument must be a Polyhedron instance')
199 inequalities1 = self.asinequalities()
200 inequalities2 = other.asinequalities()
201 inequalities = []
202 for inequality1 in inequalities1:
203 if other <= Polyhedron(inequalities=[inequality1]):
204 inequalities.append(inequality1)
205 for inequality2 in inequalities2:
206 for i in range(len(inequalities1)):
207 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
208 inequalities3.append(inequality2)
209 polyhedron3 = Polyhedron(inequalities=inequalities3)
210 if self == polyhedron3:
211 inequalities.append(inequality2)
212 break
213 return Polyhedron(inequalities=inequalities)
215 @classmethod
216 def _fromislbasicset(cls, islbset, symbols):
217 islconstraints = islhelper.isl_basic_set_constraints(islbset)
218 equalities = []
219 inequalities = []
220 for islconstraint in islconstraints:
221 constant = libisl.isl_constraint_get_constant_val(islconstraint)
222 constant = islhelper.isl_val_to_int(constant)
223 coefficients = {}
224 for index, symbol in enumerate(symbols):
225 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
226 libisl.isl_dim_set, index)
227 coefficient = islhelper.isl_val_to_int(coefficient)
228 if coefficient != 0:
229 coefficients[symbol] = coefficient
230 expression = LinExpr(coefficients, constant)
231 if libisl.isl_constraint_is_equality(islconstraint):
232 equalities.append(expression)
233 else:
234 inequalities.append(expression)
235 libisl.isl_basic_set_free(islbset)
236 self = object().__new__(Polyhedron)
237 self._equalities = tuple(equalities)
238 self._inequalities = tuple(inequalities)
239 self._symbols = cls._xsymbols(self.constraints)
240 self._dimension = len(self._symbols)
241 return self
243 @classmethod
244 def _toislbasicset(cls, equalities, inequalities, symbols):
245 dimension = len(symbols)
246 indices = {symbol: index for index, symbol in enumerate(symbols)}
247 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
248 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
249 islls = libisl.isl_local_space_from_space(islsp)
250 for equality in equalities:
251 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
252 for symbol, coefficient in equality.coefficients():
253 islval = str(coefficient).encode()
255 index = indices[symbol]
256 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
257 libisl.isl_dim_set, index, islval)
258 if equality.constant != 0:
259 islval = str(equality.constant).encode()
261 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
263 for inequality in inequalities:
264 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
265 for symbol, coefficient in inequality.coefficients():
266 islval = str(coefficient).encode()
268 index = indices[symbol]
269 islin = libisl.isl_constraint_set_coefficient_val(islin,
270 libisl.isl_dim_set, index, islval)
271 if inequality.constant != 0:
272 islval = str(inequality.constant).encode()
274 islin = libisl.isl_constraint_set_constant_val(islin, islval)
276 return islbset
278 @classmethod
279 def fromstring(cls, string):
280 domain = Domain.fromstring(string)
281 if not isinstance(domain, Polyhedron):
282 raise ValueError('non-polyhedral expression: {!r}'.format(string))
283 return domain
285 def __repr__(self):
286 strings = []
287 for equality in self.equalities:
288 left, right, swap = 0, 0, False
289 for i, (symbol, coefficient) in enumerate(equality.coefficients()):
290 if coefficient > 0:
291 left += coefficient * symbol
292 else:
293 right -= coefficient * symbol
294 if i == 0:
295 swap = True
296 if equality.constant > 0:
297 left += equality.constant
298 else:
299 right -= equality.constant
300 if swap:
301 left, right = right, left
302 strings.append('{} == {}'.format(left, right))
303 for inequality in self.inequalities:
304 left, right = 0, 0
305 for symbol, coefficient in inequality.coefficients():
306 if coefficient < 0:
307 left -= coefficient * symbol
308 else:
309 right += coefficient * symbol
310 if inequality.constant < 0:
311 left -= inequality.constant
312 else:
313 right += inequality.constant
314 strings.append('{} <= {}'.format(left, right))
315 if len(strings) == 1:
316 return strings
317 else:
318 return 'And({})'.format(', '.join(strings))
320 def _repr_latex_(self):
321 strings = []
322 for equality in self.equalities:
323 strings.append('{} = 0'.format(equality._repr_latex_().strip('\$')))
324 for inequality in self.inequalities:
325 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('\$')))
326 return '\$\${}\$\$'.format(' \\wedge '.join(strings))
328 @classmethod
329 def fromsympy(cls, expr):
330 domain = Domain.fromsympy(expr)
331 if not isinstance(domain, Polyhedron):
332 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
333 return domain
335 def tosympy(self):
336 import sympy
337 constraints = []
338 for equality in self.equalities:
339 constraints.append(sympy.Eq(equality.tosympy(), 0))
340 for inequality in self.inequalities:
341 constraints.append(sympy.Ge(inequality.tosympy(), 0))
342 return sympy.And(*constraints)
345 class EmptyType(Polyhedron):
346 """
347 The empty polyhedron, whose set of constraints is not satisfiable.
348 """
350 def __new__(cls):
351 self = object().__new__(cls)
352 self._equalities = (Rational(1),)
353 self._inequalities = ()
354 self._symbols = ()
355 self._dimension = 0
356 return self
358 def widen(self, other):
359 if not isinstance(other, Polyhedron):
360 raise ValueError('argument must be a Polyhedron instance')
361 return other
363 def __repr__(self):
364 return 'Empty'
366 def _repr_latex_(self):
367 return '\$\$\\emptyset\$\$'
369 Empty = EmptyType()
372 class UniverseType(Polyhedron):
373 """
374 The universe polyhedron, whose set of constraints is always satisfiable,
375 i.e. is empty.
376 """
378 def __new__(cls):
379 self = object().__new__(cls)
380 self._equalities = ()
381 self._inequalities = ()
382 self._symbols = ()
383 self._dimension = ()
384 return self
386 def __repr__(self):
387 return 'Universe'
389 def _repr_latex_(self):
390 return '\$\$\\Omega\$\$'
392 Universe = UniverseType()
395 def _pseudoconstructor(func):
396 @functools.wraps(func)
397 def wrapper(expr1, expr2, *exprs):
398 exprs = (expr1, expr2) + exprs
399 for expr in exprs:
400 if not isinstance(expr, LinExpr):
401 if isinstance(expr, numbers.Rational):
402 expr = Rational(expr)
403 else:
404 raise TypeError('arguments must be rational numbers '
405 'or linear expressions')
406 return func(*exprs)
407 return wrapper
409 @_pseudoconstructor
410 def Lt(*exprs):
411 """
412 Create the polyhedron with constraints expr1 < expr2 < expr3 ...
413 """
414 inequalities = []
415 for left, right in zip(exprs, exprs[1:]):
416 inequalities.append(right - left - 1)
417 return Polyhedron([], inequalities)
419 @_pseudoconstructor
420 def Le(*exprs):
421 """
422 Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
423 """
424 inequalities = []
425 for left, right in zip(exprs, exprs[1:]):
426 inequalities.append(right - left)
427 return Polyhedron([], inequalities)
429 @_pseudoconstructor
430 def Eq(*exprs):
431 """
432 Create the polyhedron with constraints expr1 == expr2 == expr3 ...
433 """
434 equalities = []
435 for left, right in zip(exprs, exprs[1:]):
436 equalities.append(left - right)
437 return Polyhedron(equalities, [])
439 @_pseudoconstructor
440 def Ne(*exprs):
441 """
442 Create the domain such that expr1 != expr2 != expr3 ... The result is a
443 Domain object, not a Polyhedron.
444 """
445 domain = Universe
446 for left, right in zip(exprs, exprs[1:]):
447 domain &= ~Eq(left, right)
448 return domain
450 @_pseudoconstructor
451 def Ge(*exprs):
452 """
453 Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
454 """
455 inequalities = []
456 for left, right in zip(exprs, exprs[1:]):
457 inequalities.append(left - right)
458 return Polyhedron([], inequalities)
460 @_pseudoconstructor
461 def Gt(*exprs):
462 """
463 Create the polyhedron with constraints expr1 > expr2 > expr3 ...
464 """
465 inequalities = []
466 for left, right in zip(exprs, exprs[1:]):
467 inequalities.append(left - right - 1)
468 return Polyhedron([], inequalities)