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