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
6 # it under the terms of the GNU General Public License as published by
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
41 unbounded.
42 """
44 __slots__ = (
45 '_equalities',
46 '_inequalities',
47 '_symbols',
48 '_dimension',
49 )
51 def __new__(cls, equalities=None, inequalities=None):
52 """
53 Return a polyhedron from two sequences of linear expressions: equalities
54 is a list of expressions equal to 0, and inequalities is a list of
55 expressions greater or equal to 0. For example, the polyhedron
56 0 <= x <= 2, 0 <= y <= 2 can be constructed with:
58 >>> x, y = symbols('x y')
59 >>> square = Polyhedron([], [x, 2 - x, y, 2 - y])
61 It may be easier to use comparison operators LinExpr.__lt__(),
62 LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
63 Le(), Eq(), Ge() and Gt(), using one of the following instructions:
65 >>> x, y = symbols('x y')
66 >>> square = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
67 >>> square = Le(0, x, 2) & Le(0, y, 2)
69 It is also possible to build a polyhedron from a string.
71 >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
73 Finally, a polyhedron can be constructed from a GeometricObject
74 instance, calling the GeometricObject.aspolyedron() method. This way, it
75 is possible to compute the polyhedral hull of a Domain instance, i.e.,
76 the convex hull of two polyhedra:
78 >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
79 >>> square2 = Polyhedron('2 <= x <= 4, 2 <= y <= 4')
80 >>> Polyhedron(square | square2)
81 """
82 if isinstance(equalities, str):
83 if inequalities is not None:
84 raise TypeError('too many arguments')
85 return cls.fromstring(equalities)
86 elif isinstance(equalities, GeometricObject):
87 if inequalities is not None:
88 raise TypeError('too many arguments')
89 return equalities.aspolyhedron()
90 sc_equalities = []
91 if equalities is not None:
92 for equality in equalities:
93 if not isinstance(equality, LinExpr):
94 raise TypeError('equalities must be linear expressions')
95 sc_equalities.append(equality.scaleint())
96 sc_inequalities = []
97 if inequalities is not None:
98 for inequality in inequalities:
99 if not isinstance(inequality, LinExpr):
100 raise TypeError('inequalities must be linear expressions')
101 sc_inequalities.append(inequality.scaleint())
102 symbols = cls._xsymbols(sc_equalities + sc_inequalities)
103 islbset = cls._toislbasicset(sc_equalities, sc_inequalities, symbols)
104 return cls._fromislbasicset(islbset, symbols)
106 @property
107 def equalities(self):
108 """
109 The tuple of equalities. This is a list of LinExpr instances that are
110 equal to 0 in the polyhedron.
111 """
112 return self._equalities
114 @property
115 def inequalities(self):
116 """
117 The tuple of inequalities. This is a list of LinExpr instances that are
118 greater or equal to 0 in the polyhedron.
119 """
120 return self._inequalities
122 @property
123 def constraints(self):
124 """
125 The tuple of constraints, i.e., equalities and inequalities. This is
126 semantically equivalent to: equalities + inequalities.
127 """
128 return self._equalities + self._inequalities
130 @property
131 def polyhedra(self):
132 return self,
134 def make_disjoint(self):
135 return self
137 def isuniverse(self):
138 islbset = self._toislbasicset(self.equalities, self.inequalities,
139 self.symbols)
140 universe = bool(libisl.isl_basic_set_is_universe(islbset))
141 libisl.isl_basic_set_free(islbset)
142 return universe
144 def aspolyhedron(self):
145 return self
147 def convex_union(self, *others):
148 """
149 Return the convex union of two or more polyhedra.
150 """
151 for other in others:
152 if not isinstance(other, Polyhedron):
153 raise TypeError('arguments must be Polyhedron instances')
154 return Polyhedron(self.union(*others))
156 def __contains__(self, point):
157 if not isinstance(point, Point):
158 raise TypeError('point must be a Point instance')
159 if self.symbols != point.symbols:
160 raise ValueError('arguments must belong to the same space')
161 for equality in self.equalities:
162 if equality.subs(point.coordinates()) != 0:
163 return False
164 for inequality in self.inequalities:
165 if inequality.subs(point.coordinates()) < 0:
166 return False
167 return True
169 def subs(self, symbol, expression=None):
170 equalities = [equality.subs(symbol, expression)
171 for equality in self.equalities]
172 inequalities = [inequality.subs(symbol, expression)
173 for inequality in self.inequalities]
174 return Polyhedron(equalities, inequalities)
176 def asinequalities(self):
177 """
178 Express the polyhedron using inequalities, given as a list of
179 expressions greater or equal to 0.
180 """
181 inequalities = list(self.equalities)
182 inequalities.extend([-expression for expression in self.equalities])
183 inequalities.extend(self.inequalities)
184 return inequalities
186 def widen(self, other):
187 """
188 Compute the standard widening of two polyhedra, à la Halbwachs.
190 In its current implementation, this method is slow and should not be
191 used on large polyhedra.
192 """
193 if not isinstance(other, Polyhedron):
194 raise TypeError('argument must be a Polyhedron instance')
195 inequalities1 = self.asinequalities()
196 inequalities2 = other.asinequalities()
197 inequalities = []
198 for inequality1 in inequalities1:
199 if other <= Polyhedron(inequalities=[inequality1]):
200 inequalities.append(inequality1)
201 for inequality2 in inequalities2:
202 for i in range(len(inequalities1)):
203 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
204 inequalities3.append(inequality2)
205 polyhedron3 = Polyhedron(inequalities=inequalities3)
206 if self == polyhedron3:
207 inequalities.append(inequality2)
208 break
209 return Polyhedron(inequalities=inequalities)
211 @classmethod
212 def _fromislbasicset(cls, islbset, symbols):
213 islconstraints = islhelper.isl_basic_set_constraints(islbset)
214 equalities = []
215 inequalities = []
216 for islconstraint in islconstraints:
217 constant = libisl.isl_constraint_get_constant_val(islconstraint)
218 constant = islhelper.isl_val_to_int(constant)
219 coefficients = {}
220 for index, symbol in enumerate(symbols):
221 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
222 libisl.isl_dim_set, index)
223 coefficient = islhelper.isl_val_to_int(coefficient)
224 if coefficient != 0:
225 coefficients[symbol] = coefficient
226 expression = LinExpr(coefficients, constant)
227 if libisl.isl_constraint_is_equality(islconstraint):
228 equalities.append(expression)
229 else:
230 inequalities.append(expression)
231 libisl.isl_basic_set_free(islbset)
232 self = object().__new__(Polyhedron)
233 self._equalities = tuple(equalities)
234 self._inequalities = tuple(inequalities)
235 self._symbols = cls._xsymbols(self.constraints)
236 self._dimension = len(self._symbols)
237 return self
239 @classmethod
240 def _toislbasicset(cls, equalities, inequalities, symbols):
241 dimension = len(symbols)
242 indices = {symbol: index for index, symbol in enumerate(symbols)}
243 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
244 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
245 islls = libisl.isl_local_space_from_space(islsp)
246 for equality in equalities:
247 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
248 for symbol, coefficient in equality.coefficients():
249 islval = str(coefficient).encode()
250 islval = libisl.isl_val_read_from_str(mainctx, islval)
251 index = indices[symbol]
252 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
253 libisl.isl_dim_set, index, islval)
254 if equality.constant != 0:
255 islval = str(equality.constant).encode()
256 islval = libisl.isl_val_read_from_str(mainctx, islval)
257 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
258 islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
259 for inequality in inequalities:
260 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
261 for symbol, coefficient in inequality.coefficients():
262 islval = str(coefficient).encode()
263 islval = libisl.isl_val_read_from_str(mainctx, islval)
264 index = indices[symbol]
265 islin = libisl.isl_constraint_set_coefficient_val(islin,
266 libisl.isl_dim_set, index, islval)
267 if inequality.constant != 0:
268 islval = str(inequality.constant).encode()
269 islval = libisl.isl_val_read_from_str(mainctx, islval)
270 islin = libisl.isl_constraint_set_constant_val(islin, islval)
271 islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
272 return islbset
274 @classmethod
275 def fromstring(cls, string):
276 domain = Domain.fromstring(string)
277 if not isinstance(domain, Polyhedron):
278 raise ValueError('non-polyhedral expression: {!r}'.format(string))
279 return domain
281 def __repr__(self):
282 strings = []
283 for equality in self.equalities:
284 left, right, swap = 0, 0, False
285 for i, (symbol, coefficient) in enumerate(equality.coefficients()):
286 if coefficient > 0:
287 left += coefficient * symbol
288 else:
289 right -= coefficient * symbol
290 if i == 0:
291 swap = True
292 if equality.constant > 0:
293 left += equality.constant
294 else:
295 right -= equality.constant
296 if swap:
297 left, right = right, left
298 strings.append('{} == {}'.format(left, right))
299 for inequality in self.inequalities:
300 left, right = 0, 0
301 for symbol, coefficient in inequality.coefficients():
302 if coefficient < 0:
303 left -= coefficient * symbol
304 else:
305 right += coefficient * symbol
306 if inequality.constant < 0:
307 left -= inequality.constant
308 else:
309 right += inequality.constant
310 strings.append('{} <= {}'.format(left, right))
311 if len(strings) == 1:
312 return strings
313 else:
314 return 'And({})'.format(', '.join(strings))
316 def _repr_latex_(self):
317 strings = []
318 for equality in self.equalities:
319 strings.append('{} = 0'.format(equality._repr_latex_().strip('\$')))
320 for inequality in self.inequalities:
321 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('\$')))
322 return '\$\${}\$\$'.format(' \\wedge '.join(strings))
324 @classmethod
325 def fromsympy(cls, expr):
326 domain = Domain.fromsympy(expr)
327 if not isinstance(domain, Polyhedron):
328 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
329 return domain
331 def tosympy(self):
332 import sympy
333 constraints = []
334 for equality in self.equalities:
335 constraints.append(sympy.Eq(equality.tosympy(), 0))
336 for inequality in self.inequalities:
337 constraints.append(sympy.Ge(inequality.tosympy(), 0))
338 return sympy.And(*constraints)
341 class EmptyType(Polyhedron):
342 """
343 The empty polyhedron, whose set of constraints is not satisfiable.
344 """
346 def __new__(cls):
347 self = object().__new__(cls)
348 self._equalities = (Rational(1),)
349 self._inequalities = ()
350 self._symbols = ()
351 self._dimension = 0
352 return self
354 def widen(self, other):
355 if not isinstance(other, Polyhedron):
356 raise ValueError('argument must be a Polyhedron instance')
357 return other
359 def __repr__(self):
360 return 'Empty'
362 def _repr_latex_(self):
363 return '\$\$\\emptyset\$\$'
365 Empty = EmptyType()
368 class UniverseType(Polyhedron):
369 """
370 The universe polyhedron, whose set of constraints is always satisfiable,
371 i.e. is empty.
372 """
374 def __new__(cls):
375 self = object().__new__(cls)
376 self._equalities = ()
377 self._inequalities = ()
378 self._symbols = ()
379 self._dimension = ()
380 return self
382 def __repr__(self):
383 return 'Universe'
385 def _repr_latex_(self):
386 return '\$\$\\Omega\$\$'
388 Universe = UniverseType()
391 def _pseudoconstructor(func):
392 @functools.wraps(func)
393 def wrapper(expr1, expr2, *exprs):
394 exprs = (expr1, expr2) + exprs
395 for expr in exprs:
396 if not isinstance(expr, LinExpr):
397 if isinstance(expr, numbers.Rational):
398 expr = Rational(expr)
399 else:
400 raise TypeError('arguments must be rational numbers '
401 'or linear expressions')
402 return func(*exprs)
403 return wrapper
405 @_pseudoconstructor
406 def Lt(*exprs):
407 """
408 Create the polyhedron with constraints expr1 < expr2 < expr3 ...
409 """
410 inequalities = []
411 for left, right in zip(exprs, exprs[1:]):
412 inequalities.append(right - left - 1)
413 return Polyhedron([], inequalities)
415 @_pseudoconstructor
416 def Le(*exprs):
417 """
418 Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
419 """
420 inequalities = []
421 for left, right in zip(exprs, exprs[1:]):
422 inequalities.append(right - left)
423 return Polyhedron([], inequalities)
425 @_pseudoconstructor
426 def Eq(*exprs):
427 """
428 Create the polyhedron with constraints expr1 == expr2 == expr3 ...
429 """
430 equalities = []
431 for left, right in zip(exprs, exprs[1:]):
432 equalities.append(left - right)
433 return Polyhedron(equalities, [])
435 @_pseudoconstructor
436 def Ne(*exprs):
437 """
438 Create the domain such that expr1 != expr2 != expr3 ... The result is a
439 Domain object, not a Polyhedron.
440 """
441 domain = Universe
442 for left, right in zip(exprs, exprs[1:]):
443 domain &= ~Eq(left, right)
444 return domain
446 @_pseudoconstructor
447 def Ge(*exprs):
448 """
449 Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
450 """
451 inequalities = []
452 for left, right in zip(exprs, exprs[1:]):
453 inequalities.append(left - right)
454 return Polyhedron([], inequalities)
456 @_pseudoconstructor
457 def Gt(*exprs):
458 """
459 Create the polyhedron with constraints expr1 > expr2 > expr3 ...
460 """
461 inequalities = []
462 for left, right in zip(exprs, exprs[1:]):
463 inequalities.append(left - right - 1)
464 return Polyhedron([], inequalities)