Remove Arch Linux installation of isl in the doc
[linpy.git] / linpy / polyhedra.py
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/>.
17
18 import functools
19 import math
20 import numbers
21
22 from . import islhelper
23
24 from .islhelper import mainctx, libisl
25 from .geometry import GeometricObject, Point
26 from .linexprs import LinExpr, Rational
27 from .domains import Domain
28
29
30 __all__ = [
31 'Polyhedron',
32 'Lt', 'Le', 'Eq', 'Ne', 'Ge', 'Gt',
33 'Empty', 'Universe',
34 ]
35
36
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 """
44
45 __slots__ = (
46 '_equalities',
47 '_inequalities',
48 '_symbols',
49 '_dimension',
50 )
51
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:
58
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)
63
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:
67
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)
71
72 It is also possible to build a polyhedron from a string.
73
74 >>> square1 = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
75
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:
80
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 isinstance(equality, LinExpr):
98 sc_equalities.append(equality.scaleint())
99 elif isinstance(equality, numbers.Rational):
100 sc_equalities.append(Rational(equality).scaleint())
101 else:
102 raise TypeError('equalities must be linear expressions '
103 'or rational numbers')
104 sc_inequalities = []
105 if inequalities is not None:
106 for inequality in inequalities:
107 if isinstance(inequality, LinExpr):
108 sc_inequalities.append(inequality.scaleint())
109 elif isinstance(inequality, numbers.Rational):
110 sc_inequalities.append(Rational(inequality).scaleint())
111 else:
112 raise TypeError('inequalities must be linear expressions '
113 'or rational numbers')
114 symbols = cls._xsymbols(sc_equalities + sc_inequalities)
115 islbset = cls._toislbasicset(sc_equalities, sc_inequalities, symbols)
116 return cls._fromislbasicset(islbset, symbols)
117
118 @property
119 def equalities(self):
120 """
121 The tuple of equalities. This is a list of LinExpr instances that are
122 equal to 0 in the polyhedron.
123 """
124 return self._equalities
125
126 @property
127 def inequalities(self):
128 """
129 The tuple of inequalities. This is a list of LinExpr instances that are
130 greater or equal to 0 in the polyhedron.
131 """
132 return self._inequalities
133
134 @property
135 def constraints(self):
136 """
137 The tuple of constraints, i.e., equalities and inequalities. This is
138 semantically equivalent to: equalities + inequalities.
139 """
140 return self._equalities + self._inequalities
141
142 @property
143 def polyhedra(self):
144 return self,
145
146 def make_disjoint(self):
147 return self
148
149 def isuniverse(self):
150 islbset = self._toislbasicset(self.equalities, self.inequalities,
151 self.symbols)
152 universe = bool(libisl.isl_basic_set_is_universe(islbset))
153 libisl.isl_basic_set_free(islbset)
154 return universe
155
156 def aspolyhedron(self):
157 return self
158
159 def convex_union(self, *others):
160 """
161 Return the convex union of two or more polyhedra.
162 """
163 for other in others:
164 if not isinstance(other, Polyhedron):
165 raise TypeError('arguments must be Polyhedron instances')
166 return Polyhedron(self.union(*others))
167
168 def __contains__(self, point):
169 if not isinstance(point, Point):
170 raise TypeError('point must be a Point instance')
171 if self.symbols != point.symbols:
172 raise ValueError('arguments must belong to the same space')
173 for equality in self.equalities:
174 if equality.subs(point.coordinates()) != 0:
175 return False
176 for inequality in self.inequalities:
177 if inequality.subs(point.coordinates()) < 0:
178 return False
179 return True
180
181 def subs(self, symbol, expression=None):
182 equalities = [equality.subs(symbol, expression)
183 for equality in self.equalities]
184 inequalities = [inequality.subs(symbol, expression)
185 for inequality in self.inequalities]
186 return Polyhedron(equalities, inequalities)
187
188 def asinequalities(self):
189 """
190 Express the polyhedron using inequalities, given as a list of
191 expressions greater or equal to 0.
192 """
193 inequalities = list(self.equalities)
194 inequalities.extend([-expression for expression in self.equalities])
195 inequalities.extend(self.inequalities)
196 return inequalities
197
198 def widen(self, other):
199 """
200 Compute the standard widening of two polyhedra, à la Halbwachs.
201
202 In its current implementation, this method is slow and should not be
203 used on large polyhedra.
204 """
205 if not isinstance(other, Polyhedron):
206 raise TypeError('argument must be a Polyhedron instance')
207 inequalities1 = self.asinequalities()
208 inequalities2 = other.asinequalities()
209 inequalities = []
210 for inequality1 in inequalities1:
211 if other <= Polyhedron(inequalities=[inequality1]):
212 inequalities.append(inequality1)
213 for inequality2 in inequalities2:
214 for i in range(len(inequalities1)):
215 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
216 inequalities3.append(inequality2)
217 polyhedron3 = Polyhedron(inequalities=inequalities3)
218 if self == polyhedron3:
219 inequalities.append(inequality2)
220 break
221 return Polyhedron(inequalities=inequalities)
222
223 @classmethod
224 def _fromislbasicset(cls, islbset, symbols):
225 if bool(libisl.isl_basic_set_is_empty(islbset)):
226 return Empty
227 if bool(libisl.isl_basic_set_is_universe(islbset)):
228 return Universe
229 islconstraints = islhelper.isl_basic_set_constraints(islbset)
230 equalities = []
231 inequalities = []
232 for islconstraint in islconstraints:
233 constant = libisl.isl_constraint_get_constant_val(islconstraint)
234 constant = islhelper.isl_val_to_int(constant)
235 coefficients = {}
236 for index, symbol in enumerate(symbols):
237 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
238 libisl.isl_dim_set, index)
239 coefficient = islhelper.isl_val_to_int(coefficient)
240 if coefficient != 0:
241 coefficients[symbol] = coefficient
242 expression = LinExpr(coefficients, constant)
243 if libisl.isl_constraint_is_equality(islconstraint):
244 equalities.append(expression)
245 else:
246 inequalities.append(expression)
247 libisl.isl_basic_set_free(islbset)
248 self = object().__new__(Polyhedron)
249 self._equalities = tuple(equalities)
250 self._inequalities = tuple(inequalities)
251 self._symbols = cls._xsymbols(self.constraints)
252 self._dimension = len(self._symbols)
253 return self
254
255 @classmethod
256 def _toislbasicset(cls, equalities, inequalities, symbols):
257 dimension = len(symbols)
258 indices = {symbol: index for index, symbol in enumerate(symbols)}
259 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
260 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
261 islls = libisl.isl_local_space_from_space(islsp)
262 for equality in equalities:
263 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
264 for symbol, coefficient in equality.coefficients():
265 islval = str(coefficient).encode()
266 islval = libisl.isl_val_read_from_str(mainctx, islval)
267 index = indices[symbol]
268 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
269 libisl.isl_dim_set, index, islval)
270 if equality.constant != 0:
271 islval = str(equality.constant).encode()
272 islval = libisl.isl_val_read_from_str(mainctx, islval)
273 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
274 islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
275 for inequality in inequalities:
276 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
277 for symbol, coefficient in inequality.coefficients():
278 islval = str(coefficient).encode()
279 islval = libisl.isl_val_read_from_str(mainctx, islval)
280 index = indices[symbol]
281 islin = libisl.isl_constraint_set_coefficient_val(islin,
282 libisl.isl_dim_set, index, islval)
283 if inequality.constant != 0:
284 islval = str(inequality.constant).encode()
285 islval = libisl.isl_val_read_from_str(mainctx, islval)
286 islin = libisl.isl_constraint_set_constant_val(islin, islval)
287 islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
288 return islbset
289
290 @classmethod
291 def fromstring(cls, string):
292 domain = Domain.fromstring(string)
293 if not isinstance(domain, Polyhedron):
294 raise ValueError('non-polyhedral expression: {!r}'.format(string))
295 return domain
296
297 def __repr__(self):
298 strings = []
299 for equality in self.equalities:
300 left, right, swap = 0, 0, False
301 for i, (symbol, coefficient) in enumerate(equality.coefficients()):
302 if coefficient > 0:
303 left += coefficient * symbol
304 else:
305 right -= coefficient * symbol
306 if i == 0:
307 swap = True
308 if equality.constant > 0:
309 left += equality.constant
310 else:
311 right -= equality.constant
312 if swap:
313 left, right = right, left
314 strings.append('{} == {}'.format(left, right))
315 for inequality in self.inequalities:
316 left, right = 0, 0
317 for symbol, coefficient in inequality.coefficients():
318 if coefficient < 0:
319 left -= coefficient * symbol
320 else:
321 right += coefficient * symbol
322 if inequality.constant < 0:
323 left -= inequality.constant
324 else:
325 right += inequality.constant
326 strings.append('{} <= {}'.format(left, right))
327 if len(strings) == 1:
328 return strings[0]
329 else:
330 return 'And({})'.format(', '.join(strings))
331
332 @classmethod
333 def fromsympy(cls, expression):
334 domain = Domain.fromsympy(expression)
335 if not isinstance(domain, Polyhedron):
336 raise ValueError('non-polyhedral expression: {!r}'.format(expression))
337 return domain
338
339 def tosympy(self):
340 import sympy
341 constraints = []
342 for equality in self.equalities:
343 constraints.append(sympy.Eq(equality.tosympy(), 0))
344 for inequality in self.inequalities:
345 constraints.append(sympy.Ge(inequality.tosympy(), 0))
346 return sympy.And(*constraints)
347
348
349 class EmptyType(Polyhedron):
350 """
351 The empty polyhedron, whose set of constraints is not satisfiable.
352 """
353
354 def __new__(cls):
355 self = object().__new__(cls)
356 self._equalities = (Rational(1),)
357 self._inequalities = ()
358 self._symbols = ()
359 self._dimension = 0
360 return self
361
362 def widen(self, other):
363 if not isinstance(other, Polyhedron):
364 raise ValueError('argument must be a Polyhedron instance')
365 return other
366
367 def __repr__(self):
368 return 'Empty'
369
370 Empty = EmptyType()
371
372
373 class UniverseType(Polyhedron):
374 """
375 The universe polyhedron, whose set of constraints is always satisfiable,
376 i.e. is empty.
377 """
378
379 def __new__(cls):
380 self = object().__new__(cls)
381 self._equalities = ()
382 self._inequalities = ()
383 self._symbols = ()
384 self._dimension = ()
385 return self
386
387 def __repr__(self):
388 return 'Universe'
389
390 Universe = UniverseType()
391
392
393 def _pseudoconstructor(func):
394 @functools.wraps(func)
395 def wrapper(expression1, expression2, *expressions):
396 expressions = (expression1, expression2) + expressions
397 for expression in expressions:
398 if not isinstance(expression, LinExpr):
399 if isinstance(expression, numbers.Rational):
400 expression = Rational(expression)
401 else:
402 raise TypeError('arguments must be rational numbers '
403 'or linear expressions')
404 return func(*expressions)
405 return wrapper
406
407 @_pseudoconstructor
408 def Lt(*expressions):
409 """
410 Create the polyhedron with constraints expr1 < expr2 < expr3 ...
411 """
412 inequalities = []
413 for left, right in zip(expressions, expressions[1:]):
414 inequalities.append(right - left - 1)
415 return Polyhedron([], inequalities)
416
417 @_pseudoconstructor
418 def Le(*expressions):
419 """
420 Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
421 """
422 inequalities = []
423 for left, right in zip(expressions, expressions[1:]):
424 inequalities.append(right - left)
425 return Polyhedron([], inequalities)
426
427 @_pseudoconstructor
428 def Eq(*expressions):
429 """
430 Create the polyhedron with constraints expr1 == expr2 == expr3 ...
431 """
432 equalities = []
433 for left, right in zip(expressions, expressions[1:]):
434 equalities.append(left - right)
435 return Polyhedron(equalities, [])
436
437 @_pseudoconstructor
438 def Ne(*expressions):
439 """
440 Create the domain such that expr1 != expr2 != expr3 ... The result is a
441 Domain object, not a Polyhedron.
442 """
443 domain = Universe
444 for left, right in zip(expressions, expressions[1:]):
445 domain &= ~Eq(left, right)
446 return domain
447
448 @_pseudoconstructor
449 def Ge(*expressions):
450 """
451 Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
452 """
453 inequalities = []
454 for left, right in zip(expressions, expressions[1:]):
455 inequalities.append(left - right)
456 return Polyhedron([], inequalities)
457
458 @_pseudoconstructor
459 def Gt(*expressions):
460 """
461 Create the polyhedron with constraints expr1 > expr2 > expr3 ...
462 """
463 inequalities = []
464 for left, right in zip(expressions, expressions[1:]):
465 inequalities.append(left - right - 1)
466 return Polyhedron([], inequalities)