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 '_constraints',
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 >>> square = Polyhedron([], [x, 2 - x, y, 2 - y])
62 It may be easier to use comparison operators LinExpr.__lt__(),
63 LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
64 Le(), Eq(), Ge() and Gt(), using one of the following instructions:
66 >>> x, y = symbols('x y')
67 >>> square = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
68 >>> square = Le(0, x, 2) & Le(0, y, 2)
70 It is also possible to build a polyhedron from a string.
72 >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
74 Finally, a polyhedron can be constructed from a GeometricObject
75 instance, calling the GeometricObject.aspolyedron() method. This way, it
76 is possible to compute the polyhedral hull of a Domain instance, i.e.,
77 the convex hull of two polyhedra:
79 >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
80 >>> square2 = Polyhedron('2 <= x <= 4, 2 <= y <= 4')
81 >>> Polyhedron(square | square2)
82 """
83 if isinstance(equalities, str):
84 if inequalities is not None:
85 raise TypeError('too many arguments')
86 return cls.fromstring(equalities)
87 elif isinstance(equalities, GeometricObject):
88 if inequalities is not None:
89 raise TypeError('too many arguments')
90 return equalities.aspolyhedron()
91 if equalities is None:
92 equalities = []
93 else:
94 for i, equality in enumerate(equalities):
95 if not isinstance(equality, LinExpr):
96 raise TypeError('equalities must be linear expressions')
97 equalities[i] = equality.scaleint()
98 if inequalities is None:
99 inequalities = []
100 else:
101 for i, inequality in enumerate(inequalities):
102 if not isinstance(inequality, LinExpr):
103 raise TypeError('inequalities must be linear expressions')
104 inequalities[i] = inequality.scaleint()
105 symbols = cls._xsymbols(equalities + inequalities)
106 islbset = cls._toislbasicset(equalities, 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._constraints
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 __contains__(self, point):
151 if not isinstance(point, Point):
152 raise TypeError('point must be a Point instance')
153 if self.symbols != point.symbols:
154 raise ValueError('arguments must belong to the same space')
155 for equality in self.equalities:
156 if equality.subs(point.coordinates()) != 0:
157 return False
158 for inequality in self.inequalities:
159 if inequality.subs(point.coordinates()) < 0:
160 return False
161 return True
163 def subs(self, symbol, expression=None):
164 equalities = [equality.subs(symbol, expression)
165 for equality in self.equalities]
166 inequalities = [inequality.subs(symbol, expression)
167 for inequality in self.inequalities]
168 return Polyhedron(equalities, inequalities)
170 def _asinequalities(self):
171 inequalities = list(self.equalities)
172 inequalities.extend([-expression for expression in self.equalities])
173 inequalities.extend(self.inequalities)
174 return inequalities
176 def widen(self, other):
177 """
178 Compute the standard widening of two polyhedra, à la Halbwachs.
179 """
180 if not isinstance(other, Polyhedron):
181 raise ValueError('argument must be a Polyhedron instance')
182 inequalities1 = self._asinequalities()
183 inequalities2 = other._asinequalities()
184 inequalities = []
185 for inequality1 in inequalities1:
186 if other <= Polyhedron(inequalities=[inequality1]):
187 inequalities.append(inequality1)
188 for inequality2 in inequalities2:
189 for i in range(len(inequalities1)):
190 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
191 inequalities3.append(inequality2)
192 polyhedron3 = Polyhedron(inequalities=inequalities3)
193 if self == polyhedron3:
194 inequalities.append(inequality2)
195 break
196 return Polyhedron(inequalities=inequalities)
198 @classmethod
199 def _fromislbasicset(cls, islbset, symbols):
200 islconstraints = islhelper.isl_basic_set_constraints(islbset)
201 equalities = []
202 inequalities = []
203 for islconstraint in islconstraints:
204 constant = libisl.isl_constraint_get_constant_val(islconstraint)
205 constant = islhelper.isl_val_to_int(constant)
206 coefficients = {}
207 for index, symbol in enumerate(symbols):
208 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
209 libisl.isl_dim_set, index)
210 coefficient = islhelper.isl_val_to_int(coefficient)
211 if coefficient != 0:
212 coefficients[symbol] = coefficient
213 expression = LinExpr(coefficients, constant)
214 if libisl.isl_constraint_is_equality(islconstraint):
215 equalities.append(expression)
216 else:
217 inequalities.append(expression)
218 libisl.isl_basic_set_free(islbset)
219 self = object().__new__(Polyhedron)
220 self._equalities = tuple(equalities)
221 self._inequalities = tuple(inequalities)
222 self._constraints = tuple(equalities + inequalities)
223 self._symbols = cls._xsymbols(self._constraints)
224 self._dimension = len(self._symbols)
225 return self
227 @classmethod
228 def _toislbasicset(cls, equalities, inequalities, symbols):
229 dimension = len(symbols)
230 indices = {symbol: index for index, symbol in enumerate(symbols)}
231 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
232 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
233 islls = libisl.isl_local_space_from_space(islsp)
234 for equality in equalities:
235 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
236 for symbol, coefficient in equality.coefficients():
237 islval = str(coefficient).encode()
239 index = indices[symbol]
240 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
241 libisl.isl_dim_set, index, islval)
242 if equality.constant != 0:
243 islval = str(equality.constant).encode()
245 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
247 for inequality in inequalities:
248 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
249 for symbol, coefficient in inequality.coefficients():
250 islval = str(coefficient).encode()
252 index = indices[symbol]
253 islin = libisl.isl_constraint_set_coefficient_val(islin,
254 libisl.isl_dim_set, index, islval)
255 if inequality.constant != 0:
256 islval = str(inequality.constant).encode()
258 islin = libisl.isl_constraint_set_constant_val(islin, islval)
260 return islbset
262 @classmethod
263 def fromstring(cls, string):
264 domain = Domain.fromstring(string)
265 if not isinstance(domain, Polyhedron):
266 raise ValueError('non-polyhedral expression: {!r}'.format(string))
267 return domain
269 def __repr__(self):
270 strings = []
271 for equality in self.equalities:
272 strings.append('Eq({}, 0)'.format(equality))
273 for inequality in self.inequalities:
274 strings.append('Ge({}, 0)'.format(inequality))
275 if len(strings) == 1:
276 return strings
277 else:
278 return 'And({})'.format(', '.join(strings))
280 def _repr_latex_(self):
281 strings = []
282 for equality in self.equalities:
283 strings.append('{} = 0'.format(equality._repr_latex_().strip('\$')))
284 for inequality in self.inequalities:
285 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('\$')))
286 return '\$\${}\$\$'.format(' \\wedge '.join(strings))
288 @classmethod
289 def fromsympy(cls, expr):
290 domain = Domain.fromsympy(expr)
291 if not isinstance(domain, Polyhedron):
292 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
293 return domain
295 def tosympy(self):
296 import sympy
297 constraints = []
298 for equality in self.equalities:
299 constraints.append(sympy.Eq(equality.tosympy(), 0))
300 for inequality in self.inequalities:
301 constraints.append(sympy.Ge(inequality.tosympy(), 0))
302 return sympy.And(*constraints)
305 class EmptyType(Polyhedron):
306 """
307 The empty polyhedron, whose set of constraints is not satisfiable.
308 """
310 __slots__ = Polyhedron.__slots__
312 def __new__(cls):
313 self = object().__new__(cls)
314 self._equalities = (Rational(1),)
315 self._inequalities = ()
316 self._constraints = self._equalities
317 self._symbols = ()
318 self._dimension = 0
319 return self
321 def widen(self, other):
322 if not isinstance(other, Polyhedron):
323 raise ValueError('argument must be a Polyhedron instance')
324 return other
326 def __repr__(self):
327 return 'Empty'
329 def _repr_latex_(self):
330 return '\$\$\\emptyset\$\$'
332 Empty = EmptyType()
335 class UniverseType(Polyhedron):
336 """
337 The universe polyhedron, whose set of constraints is always satisfiable,
338 i.e. is empty.
339 """
341 __slots__ = Polyhedron.__slots__
343 def __new__(cls):
344 self = object().__new__(cls)
345 self._equalities = ()
346 self._inequalities = ()
347 self._constraints = ()
348 self._symbols = ()
349 self._dimension = ()
350 return self
352 def __repr__(self):
353 return 'Universe'
355 def _repr_latex_(self):
356 return '\$\$\\Omega\$\$'
358 Universe = UniverseType()
361 def _polymorphic(func):
362 @functools.wraps(func)
363 def wrapper(left, right):
364 if not isinstance(left, LinExpr):
365 if isinstance(left, numbers.Rational):
366 left = Rational(left)
367 else:
368 raise TypeError('left must be a a rational number '
369 'or a linear expression')
370 if not isinstance(right, LinExpr):
371 if isinstance(right, numbers.Rational):
372 right = Rational(right)
373 else:
374 raise TypeError('right must be a a rational number '
375 'or a linear expression')
376 return func(left, right)
377 return wrapper
379 @_polymorphic
380 def Lt(left, right):
381 """
382 Create the polyhedron with constraints expr1 < expr2 < expr3 ...
383 """
384 return Polyhedron([], [right - left - 1])
386 @_polymorphic
387 def Le(left, right):
388 """
389 Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
390 """
391 return Polyhedron([], [right - left])
393 @_polymorphic
394 def Eq(left, right):
395 """
396 Create the polyhedron with constraints expr1 == expr2 == expr3 ...
397 """
398 return Polyhedron([left - right], [])
400 @_polymorphic
401 def Ne(left, right):
402 """
403 Create the domain such that expr1 != expr2 != expr3 ... The result is a
404 Domain, not a Polyhedron.
405 """
406 return ~Eq(left, right)
408 @_polymorphic
409 def Gt(left, right):
410 """
411 Create the polyhedron with constraints expr1 > expr2 > expr3 ...
412 """
413 return Polyhedron([], [left - right - 1])
415 @_polymorphic
416 def Ge(left, right):
417 """
418 Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
419 """
420 return Polyhedron([], [left - right])