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 if equalities is None:
91 equalities = []
92 else:
93 for i, equality in enumerate(equalities):
94 if not isinstance(equality, LinExpr):
95 raise TypeError('equalities must be linear expressions')
96 equalities[i] = equality.scaleint()
97 if inequalities is None:
98 inequalities = []
99 else:
100 for i, inequality in enumerate(inequalities):
101 if not isinstance(inequality, LinExpr):
102 raise TypeError('inequalities must be linear expressions')
103 inequalities[i] = inequality.scaleint()
104 symbols = cls._xsymbols(equalities + inequalities)
105 islbset = cls._toislbasicset(equalities, inequalities, symbols)
106 return cls._fromislbasicset(islbset, symbols)
108 @property
109 def equalities(self):
110 """
111 The tuple of equalities. This is a list of LinExpr instances that are
112 equal to 0 in the polyhedron.
113 """
114 return self._equalities
116 @property
117 def inequalities(self):
118 """
119 The tuple of inequalities. This is a list of LinExpr instances that are
120 greater or equal to 0 in the polyhedron.
121 """
122 return self._inequalities
124 @property
125 def constraints(self):
126 """
127 The tuple of constraints, i.e., equalities and inequalities. This is
128 semantically equivalent to: equalities + inequalities.
129 """
130 return self._equalities + self._inequalities
132 @property
133 def polyhedra(self):
134 return self,
136 def make_disjoint(self):
137 return self
139 def isuniverse(self):
140 islbset = self._toislbasicset(self.equalities, self.inequalities,
141 self.symbols)
142 universe = bool(libisl.isl_basic_set_is_universe(islbset))
143 libisl.isl_basic_set_free(islbset)
144 return universe
146 def aspolyhedron(self):
147 return self
149 def __contains__(self, point):
150 if not isinstance(point, Point):
151 raise TypeError('point must be a Point instance')
152 if self.symbols != point.symbols:
153 raise ValueError('arguments must belong to the same space')
154 for equality in self.equalities:
155 if equality.subs(point.coordinates()) != 0:
156 return False
157 for inequality in self.inequalities:
158 if inequality.subs(point.coordinates()) < 0:
159 return False
160 return True
162 def subs(self, symbol, expression=None):
163 equalities = [equality.subs(symbol, expression)
164 for equality in self.equalities]
165 inequalities = [inequality.subs(symbol, expression)
166 for inequality in self.inequalities]
167 return Polyhedron(equalities, inequalities)
169 def _asinequalities(self):
170 inequalities = list(self.equalities)
171 inequalities.extend([-expression for expression in self.equalities])
172 inequalities.extend(self.inequalities)
173 return inequalities
175 def widen(self, other):
176 """
177 Compute the standard widening of two polyhedra, à la Halbwachs.
178 """
179 if not isinstance(other, Polyhedron):
180 raise ValueError('argument must be a Polyhedron instance')
181 inequalities1 = self._asinequalities()
182 inequalities2 = other._asinequalities()
183 inequalities = []
184 for inequality1 in inequalities1:
185 if other <= Polyhedron(inequalities=[inequality1]):
186 inequalities.append(inequality1)
187 for inequality2 in inequalities2:
188 for i in range(len(inequalities1)):
189 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
190 inequalities3.append(inequality2)
191 polyhedron3 = Polyhedron(inequalities=inequalities3)
192 if self == polyhedron3:
193 inequalities.append(inequality2)
194 break
195 return Polyhedron(inequalities=inequalities)
197 @classmethod
198 def _fromislbasicset(cls, islbset, symbols):
199 islconstraints = islhelper.isl_basic_set_constraints(islbset)
200 equalities = []
201 inequalities = []
202 for islconstraint in islconstraints:
203 constant = libisl.isl_constraint_get_constant_val(islconstraint)
204 constant = islhelper.isl_val_to_int(constant)
205 coefficients = {}
206 for index, symbol in enumerate(symbols):
207 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
208 libisl.isl_dim_set, index)
209 coefficient = islhelper.isl_val_to_int(coefficient)
210 if coefficient != 0:
211 coefficients[symbol] = coefficient
212 expression = LinExpr(coefficients, constant)
213 if libisl.isl_constraint_is_equality(islconstraint):
214 equalities.append(expression)
215 else:
216 inequalities.append(expression)
217 libisl.isl_basic_set_free(islbset)
218 self = object().__new__(Polyhedron)
219 self._equalities = tuple(equalities)
220 self._inequalities = tuple(inequalities)
221 self._symbols = cls._xsymbols(self.constraints)
222 self._dimension = len(self._symbols)
223 return self
225 @classmethod
226 def _toislbasicset(cls, equalities, inequalities, symbols):
227 dimension = len(symbols)
228 indices = {symbol: index for index, symbol in enumerate(symbols)}
229 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
230 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
231 islls = libisl.isl_local_space_from_space(islsp)
232 for equality in equalities:
233 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
234 for symbol, coefficient in equality.coefficients():
235 islval = str(coefficient).encode()
236 islval = libisl.isl_val_read_from_str(mainctx, islval)
237 index = indices[symbol]
238 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
239 libisl.isl_dim_set, index, islval)
240 if equality.constant != 0:
241 islval = str(equality.constant).encode()
242 islval = libisl.isl_val_read_from_str(mainctx, islval)
243 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
244 islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
245 for inequality in inequalities:
246 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
247 for symbol, coefficient in inequality.coefficients():
248 islval = str(coefficient).encode()
249 islval = libisl.isl_val_read_from_str(mainctx, islval)
250 index = indices[symbol]
251 islin = libisl.isl_constraint_set_coefficient_val(islin,
252 libisl.isl_dim_set, index, islval)
253 if inequality.constant != 0:
254 islval = str(inequality.constant).encode()
255 islval = libisl.isl_val_read_from_str(mainctx, islval)
256 islin = libisl.isl_constraint_set_constant_val(islin, islval)
257 islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
258 return islbset
260 @classmethod
261 def fromstring(cls, string):
262 domain = Domain.fromstring(string)
263 if not isinstance(domain, Polyhedron):
264 raise ValueError('non-polyhedral expression: {!r}'.format(string))
265 return domain
267 def __repr__(self):
268 strings = []
269 for equality in self.equalities:
270 strings.append('Eq({}, 0)'.format(equality))
271 for inequality in self.inequalities:
272 strings.append('Ge({}, 0)'.format(inequality))
273 if len(strings) == 1:
274 return strings
275 else:
276 return 'And({})'.format(', '.join(strings))
278 def _repr_latex_(self):
279 strings = []
280 for equality in self.equalities:
281 strings.append('{} = 0'.format(equality._repr_latex_().strip('\$')))
282 for inequality in self.inequalities:
283 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('\$')))
284 return '\$\${}\$\$'.format(' \\wedge '.join(strings))
286 @classmethod
287 def fromsympy(cls, expr):
288 domain = Domain.fromsympy(expr)
289 if not isinstance(domain, Polyhedron):
290 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
291 return domain
293 def tosympy(self):
294 import sympy
295 constraints = []
296 for equality in self.equalities:
297 constraints.append(sympy.Eq(equality.tosympy(), 0))
298 for inequality in self.inequalities:
299 constraints.append(sympy.Ge(inequality.tosympy(), 0))
300 return sympy.And(*constraints)
303 class EmptyType(Polyhedron):
304 """
305 The empty polyhedron, whose set of constraints is not satisfiable.
306 """
308 __slots__ = Polyhedron.__slots__
310 def __new__(cls):
311 self = object().__new__(cls)
312 self._equalities = (Rational(1),)
313 self._inequalities = ()
314 self._symbols = ()
315 self._dimension = 0
316 return self
318 def widen(self, other):
319 if not isinstance(other, Polyhedron):
320 raise ValueError('argument must be a Polyhedron instance')
321 return other
323 def __repr__(self):
324 return 'Empty'
326 def _repr_latex_(self):
327 return '\$\$\\emptyset\$\$'
329 Empty = EmptyType()
332 class UniverseType(Polyhedron):
333 """
334 The universe polyhedron, whose set of constraints is always satisfiable,
335 i.e. is empty.
336 """
338 __slots__ = Polyhedron.__slots__
340 def __new__(cls):
341 self = object().__new__(cls)
342 self._equalities = ()
343 self._inequalities = ()
344 self._symbols = ()
345 self._dimension = ()
346 return self
348 def __repr__(self):
349 return 'Universe'
351 def _repr_latex_(self):
352 return '\$\$\\Omega\$\$'
354 Universe = UniverseType()
357 def _polymorphic(func):
358 @functools.wraps(func)
359 def wrapper(left, right):
360 if not isinstance(left, LinExpr):
361 if isinstance(left, numbers.Rational):
362 left = Rational(left)
363 else:
364 raise TypeError('left must be a a rational number '
365 'or a linear expression')
366 if not isinstance(right, LinExpr):
367 if isinstance(right, numbers.Rational):
368 right = Rational(right)
369 else:
370 raise TypeError('right must be a a rational number '
371 'or a linear expression')
372 return func(left, right)
373 return wrapper
375 @_polymorphic
376 def Lt(left, right):
377 """
378 Create the polyhedron with constraints expr1 < expr2 < expr3 ...
379 """
380 return Polyhedron([], [right - left - 1])
382 @_polymorphic
383 def Le(left, right):
384 """
385 Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
386 """
387 return Polyhedron([], [right - left])
389 @_polymorphic
390 def Eq(left, right):
391 """
392 Create the polyhedron with constraints expr1 == expr2 == expr3 ...
393 """
394 return Polyhedron([left - right], [])
396 @_polymorphic
397 def Ne(left, right):
398 """
399 Create the domain such that expr1 != expr2 != expr3 ... The result is a
400 Domain, not a Polyhedron.
401 """
402 return ~Eq(left, right)
404 @_polymorphic
405 def Gt(left, right):
406 """
407 Create the polyhedron with constraints expr1 > expr2 > expr3 ...
408 """
409 return Polyhedron([], [left - right - 1])
411 @_polymorphic
412 def Ge(left, right):
413 """
414 Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
415 """
416 return Polyhedron([], [left - right])