346ffff2d0810d1ea87f7d457ef96e37123517e9
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 Polyhedron class allows users to build and inspect polyherons. Polyhedron inherits from Domain.
40 """
41 __slots__ = (
42 '_equalities',
43 '_inequalities',
44 '_constraints',
45 '_symbols',
46 '_dimension',
47 )
49 def __new__(cls, equalities=None, inequalities=None):
50 """
51 Create and return a new Polyhedron from a string or list of equalities and inequalities.
52 """
54 if isinstance(equalities, str):
55 if inequalities is not None:
56 raise TypeError('too many arguments')
57 return cls.fromstring(equalities)
58 elif isinstance(equalities, GeometricObject):
59 if inequalities is not None:
60 raise TypeError('too many arguments')
61 return equalities.aspolyhedron()
62 if equalities is None:
63 equalities = []
64 else:
65 for i, equality in enumerate(equalities):
66 if not isinstance(equality, LinExpr):
67 raise TypeError('equalities must be linear expressions')
68 equalities[i] = equality.scaleint()
69 if inequalities is None:
70 inequalities = []
71 else:
72 for i, inequality in enumerate(inequalities):
73 if not isinstance(inequality, LinExpr):
74 raise TypeError('inequalities must be linear expressions')
75 inequalities[i] = inequality.scaleint()
76 symbols = cls._xsymbols(equalities + inequalities)
77 islbset = cls._toislbasicset(equalities, inequalities, symbols)
78 return cls._fromislbasicset(islbset, symbols)
80 @property
81 def equalities(self):
82 """
83 Return a list of the equalities in a polyhedron.
84 """
85 return self._equalities
87 @property
88 def inequalities(self):
89 """
90 Return a list of the inequalities in a polyhedron.
91 """
92 return self._inequalities
94 @property
95 def constraints(self):
96 """
97 Return the list of the constraints of a polyhedron.
98 """
99 return self._constraints
101 @property
102 def polyhedra(self):
103 return self,
105 def make_disjoint(self):
106 """
107 Return a polyhedron as disjoint.
108 """
109 return self
111 def isuniverse(self):
112 """
113 Return true if a polyhedron is the Universe set.
114 """
115 islbset = self._toislbasicset(self.equalities, self.inequalities,
116 self.symbols)
117 universe = bool(libisl.isl_basic_set_is_universe(islbset))
118 libisl.isl_basic_set_free(islbset)
119 return universe
121 def aspolyhedron(self):
122 """
123 Return the polyhedral hull of a polyhedron.
124 """
125 return self
127 def __contains__(self, point):
128 """
129 Report whether a polyhedron constains an integer point
130 """
131 if not isinstance(point, Point):
132 raise TypeError('point must be a Point instance')
133 if self.symbols != point.symbols:
134 raise ValueError('arguments must belong to the same space')
135 for equality in self.equalities:
136 if equality.subs(point.coordinates()) != 0:
137 return False
138 for inequality in self.inequalities:
139 if inequality.subs(point.coordinates()) < 0:
140 return False
141 return True
143 def subs(self, symbol, expression=None):
144 """
145 Subsitute the given value into an expression and return the resulting
146 expression.
147 """
148 equalities = [equality.subs(symbol, expression)
149 for equality in self.equalities]
150 inequalities = [inequality.subs(symbol, expression)
151 for inequality in self.inequalities]
152 return Polyhedron(equalities, inequalities)
154 def _asinequalities(self):
155 inequalities = list(self.equalities)
156 inequalities.extend([-expression for expression in self.equalities])
157 inequalities.extend(self.inequalities)
158 return inequalities
160 def widen(self, other):
161 if not isinstance(other, Polyhedron):
162 raise ValueError('argument must be a Polyhedron instance')
163 inequalities1 = self._asinequalities()
164 inequalities2 = other._asinequalities()
165 inequalities = []
166 for inequality1 in inequalities1:
167 if other <= Polyhedron(inequalities=[inequality1]):
168 inequalities.append(inequality1)
169 for inequality2 in inequalities2:
170 for i in range(len(inequalities1)):
171 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
172 inequalities3.append(inequality2)
173 polyhedron3 = Polyhedron(inequalities=inequalities3)
174 if self == polyhedron3:
175 inequalities.append(inequality2)
176 break
177 return Polyhedron(inequalities=inequalities)
179 @classmethod
180 def _fromislbasicset(cls, islbset, symbols):
181 islconstraints = islhelper.isl_basic_set_constraints(islbset)
182 equalities = []
183 inequalities = []
184 for islconstraint in islconstraints:
185 constant = libisl.isl_constraint_get_constant_val(islconstraint)
186 constant = islhelper.isl_val_to_int(constant)
187 coefficients = {}
188 for index, symbol in enumerate(symbols):
189 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
190 libisl.isl_dim_set, index)
191 coefficient = islhelper.isl_val_to_int(coefficient)
192 if coefficient != 0:
193 coefficients[symbol] = coefficient
194 expression = LinExpr(coefficients, constant)
195 if libisl.isl_constraint_is_equality(islconstraint):
196 equalities.append(expression)
197 else:
198 inequalities.append(expression)
199 libisl.isl_basic_set_free(islbset)
200 self = object().__new__(Polyhedron)
201 self._equalities = tuple(equalities)
202 self._inequalities = tuple(inequalities)
203 self._constraints = tuple(equalities + inequalities)
204 self._symbols = cls._xsymbols(self._constraints)
205 self._dimension = len(self._symbols)
206 return self
208 @classmethod
209 def _toislbasicset(cls, equalities, inequalities, symbols):
210 dimension = len(symbols)
211 indices = {symbol: index for index, symbol in enumerate(symbols)}
212 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
213 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
214 islls = libisl.isl_local_space_from_space(islsp)
215 for equality in equalities:
216 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
217 for symbol, coefficient in equality.coefficients():
218 islval = str(coefficient).encode()
220 index = indices[symbol]
221 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
222 libisl.isl_dim_set, index, islval)
223 if equality.constant != 0:
224 islval = str(equality.constant).encode()
226 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
228 for inequality in inequalities:
229 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
230 for symbol, coefficient in inequality.coefficients():
231 islval = str(coefficient).encode()
233 index = indices[symbol]
234 islin = libisl.isl_constraint_set_coefficient_val(islin,
235 libisl.isl_dim_set, index, islval)
236 if inequality.constant != 0:
237 islval = str(inequality.constant).encode()
239 islin = libisl.isl_constraint_set_constant_val(islin, islval)
241 return islbset
243 @classmethod
244 def fromstring(cls, string):
245 """
246 Create and return a Polyhedron from a string.
247 """
248 domain = Domain.fromstring(string)
249 if not isinstance(domain, Polyhedron):
250 raise ValueError('non-polyhedral expression: {!r}'.format(string))
251 return domain
253 def __repr__(self):
254 strings = []
255 for equality in self.equalities:
256 strings.append('Eq({}, 0)'.format(equality))
257 for inequality in self.inequalities:
258 strings.append('Ge({}, 0)'.format(inequality))
259 if len(strings) == 1:
260 return strings
261 else:
262 return 'And({})'.format(', '.join(strings))
265 def _repr_latex_(self):
266 strings = []
267 for equality in self.equalities:
268 strings.append('{} = 0'.format(equality._repr_latex_().strip('\$')))
269 for inequality in self.inequalities:
270 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('\$')))
271 return '\$\${}\$\$'.format(' \\wedge '.join(strings))
273 @classmethod
274 def fromsympy(cls, expr):
275 """
276 Convert a sympy object to a polyhedron.
277 """
278 domain = Domain.fromsympy(expr)
279 if not isinstance(domain, Polyhedron):
280 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
281 return domain
283 def tosympy(self):
284 """
285 Return a polyhedron as a sympy object.
286 """
287 import sympy
288 constraints = []
289 for equality in self.equalities:
290 constraints.append(sympy.Eq(equality.tosympy(), 0))
291 for inequality in self.inequalities:
292 constraints.append(sympy.Ge(inequality.tosympy(), 0))
293 return sympy.And(*constraints)
296 class EmptyType(Polyhedron):
298 __slots__ = Polyhedron.__slots__
300 def __new__(cls):
301 self = object().__new__(cls)
302 self._equalities = (Rational(1),)
303 self._inequalities = ()
304 self._constraints = self._equalities
305 self._symbols = ()
306 self._dimension = 0
307 return self
309 def widen(self, other):
310 if not isinstance(other, Polyhedron):
311 raise ValueError('argument must be a Polyhedron instance')
312 return other
314 def __repr__(self):
315 return 'Empty'
317 def _repr_latex_(self):
318 return '\$\$\\emptyset\$\$'
320 Empty = EmptyType()
323 class UniverseType(Polyhedron):
325 __slots__ = Polyhedron.__slots__
327 def __new__(cls):
328 self = object().__new__(cls)
329 self._equalities = ()
330 self._inequalities = ()
331 self._constraints = ()
332 self._symbols = ()
333 self._dimension = ()
334 return self
336 def __repr__(self):
337 return 'Universe'
339 def _repr_latex_(self):
340 return '\$\$\\Omega\$\$'
342 Universe = UniverseType()
345 def _polymorphic(func):
346 @functools.wraps(func)
347 def wrapper(left, right):
348 if not isinstance(left, LinExpr):
349 if isinstance(left, numbers.Rational):
350 left = Rational(left)
351 else:
352 raise TypeError('left must be a a rational number '
353 'or a linear expression')
354 if not isinstance(right, LinExpr):
355 if isinstance(right, numbers.Rational):
356 right = Rational(right)
357 else:
358 raise TypeError('right must be a a rational number '
359 'or a linear expression')
360 return func(left, right)
361 return wrapper
363 @_polymorphic
364 def Lt(left, right):
365 """
366 Returns a Polyhedron instance with a single constraint as left less than right.
367 """
368 return Polyhedron([], [right - left - 1])
370 @_polymorphic
371 def Le(left, right):
372 """
373 Returns a Polyhedron instance with a single constraint as left less than or equal to right.
374 """
375 return Polyhedron([], [right - left])
377 @_polymorphic
378 def Eq(left, right):
379 """
380 Returns a Polyhedron instance with a single constraint as left equal to right.
381 """
382 return Polyhedron([left - right], [])
384 @_polymorphic
385 def Ne(left, right):
386 """
387 Returns a Polyhedron instance with a single constraint as left not equal to right.
388 """
389 return ~Eq(left, right)
391 @_polymorphic
392 def Gt(left, right):
393 """
394 Returns a Polyhedron instance with a single constraint as left greater than right.
395 """
396 return Polyhedron([], [left - right - 1])
398 @_polymorphic
399 def Ge(left, right):
400 """
401 Returns a Polyhedron instance with a single constraint as left greater than or equal to right.
402 """
403 return Polyhedron([], [left - right])