Add EmptyType and UniverseType
[linpy.git] / pypol / polyhedra.py
1 import functools
2 import math
3 import numbers
4
5 from . import islhelper
6
7 from .islhelper import mainctx, libisl
8 from .geometry import GeometricObject, Point
9 from .linexprs import Expression, Rational
10 from .domains import Domain
11
12
13 __all__ = [
14 'Polyhedron',
15 'Lt', 'Le', 'Eq', 'Ne', 'Ge', 'Gt',
16 'Empty', 'Universe',
17 ]
18
19
20 class Polyhedron(Domain):
21
22 __slots__ = (
23 '_equalities',
24 '_inequalities',
25 '_constraints',
26 '_symbols',
27 '_dimension',
28 )
29
30 def __new__(cls, equalities=None, inequalities=None):
31 if isinstance(equalities, str):
32 if inequalities is not None:
33 raise TypeError('too many arguments')
34 return cls.fromstring(equalities)
35 elif isinstance(equalities, GeometricObject):
36 if inequalities is not None:
37 raise TypeError('too many arguments')
38 return equalities.aspolyhedron()
39 if equalities is None:
40 equalities = []
41 else:
42 for i, equality in enumerate(equalities):
43 if not isinstance(equality, Expression):
44 raise TypeError('equalities must be linear expressions')
45 equalities[i] = equality.scaleint()
46 if inequalities is None:
47 inequalities = []
48 else:
49 for i, inequality in enumerate(inequalities):
50 if not isinstance(inequality, Expression):
51 raise TypeError('inequalities must be linear expressions')
52 inequalities[i] = inequality.scaleint()
53 symbols = cls._xsymbols(equalities + inequalities)
54 islbset = cls._toislbasicset(equalities, inequalities, symbols)
55 return cls._fromislbasicset(islbset, symbols)
56
57 @property
58 def equalities(self):
59 return self._equalities
60
61 @property
62 def inequalities(self):
63 return self._inequalities
64
65 @property
66 def constraints(self):
67 return self._constraints
68
69 @property
70 def polyhedra(self):
71 return self,
72
73 def disjoint(self):
74 """
75 Return this set as disjoint.
76 """
77 return self
78
79 def isuniverse(self):
80 """
81 Return true if this set is the Universe set.
82 """
83 islbset = self._toislbasicset(self.equalities, self.inequalities,
84 self.symbols)
85 universe = bool(libisl.isl_basic_set_is_universe(islbset))
86 libisl.isl_basic_set_free(islbset)
87 return universe
88
89 def aspolyhedron(self):
90 """
91 Return polyhedral hull of this set.
92 """
93 return self
94
95 def __contains__(self, point):
96 if not isinstance(point, Point):
97 raise TypeError('point must be a Point instance')
98 if self.symbols != point.symbols:
99 raise ValueError('arguments must belong to the same space')
100 for equality in self.equalities:
101 if equality.subs(point.coordinates()) != 0:
102 return False
103 for inequality in self.inequalities:
104 if inequality.subs(point.coordinates()) < 0:
105 return False
106 return True
107
108 def subs(self, symbol, expression=None):
109 equalities = [equality.subs(symbol, expression)
110 for equality in self.equalities]
111 inequalities = [inequality.subs(symbol, expression)
112 for inequality in self.inequalities]
113 return Polyhedron(equalities, inequalities)
114
115 @classmethod
116 def _fromislbasicset(cls, islbset, symbols):
117 if libisl.isl_basic_set_is_empty(islbset):
118 return Empty
119 if libisl.isl_basic_set_is_universe(islbset):
120 return Universe
121 islconstraints = islhelper.isl_basic_set_constraints(islbset)
122 equalities = []
123 inequalities = []
124 for islconstraint in islconstraints:
125 constant = libisl.isl_constraint_get_constant_val(islconstraint)
126 constant = islhelper.isl_val_to_int(constant)
127 coefficients = {}
128 for index, symbol in enumerate(symbols):
129 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
130 libisl.isl_dim_set, index)
131 coefficient = islhelper.isl_val_to_int(coefficient)
132 if coefficient != 0:
133 coefficients[symbol] = coefficient
134 expression = Expression(coefficients, constant)
135 if libisl.isl_constraint_is_equality(islconstraint):
136 equalities.append(expression)
137 else:
138 inequalities.append(expression)
139 libisl.isl_basic_set_free(islbset)
140 self = object().__new__(Polyhedron)
141 self._equalities = tuple(equalities)
142 self._inequalities = tuple(inequalities)
143 self._constraints = tuple(equalities + inequalities)
144 self._symbols = cls._xsymbols(self._constraints)
145 self._dimension = len(self._symbols)
146 return self
147
148 @classmethod
149 def _toislbasicset(cls, equalities, inequalities, symbols):
150 dimension = len(symbols)
151 indices = {symbol: index for index, symbol in enumerate(symbols)}
152 islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
153 islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
154 islls = libisl.isl_local_space_from_space(islsp)
155 for equality in equalities:
156 isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
157 for symbol, coefficient in equality.coefficients():
158 islval = str(coefficient).encode()
159 islval = libisl.isl_val_read_from_str(mainctx, islval)
160 index = indices[symbol]
161 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
162 libisl.isl_dim_set, index, islval)
163 if equality.constant != 0:
164 islval = str(equality.constant).encode()
165 islval = libisl.isl_val_read_from_str(mainctx, islval)
166 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
167 islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
168 for inequality in inequalities:
169 islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
170 for symbol, coefficient in inequality.coefficients():
171 islval = str(coefficient).encode()
172 islval = libisl.isl_val_read_from_str(mainctx, islval)
173 index = indices[symbol]
174 islin = libisl.isl_constraint_set_coefficient_val(islin,
175 libisl.isl_dim_set, index, islval)
176 if inequality.constant != 0:
177 islval = str(inequality.constant).encode()
178 islval = libisl.isl_val_read_from_str(mainctx, islval)
179 islin = libisl.isl_constraint_set_constant_val(islin, islval)
180 islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
181 return islbset
182
183 @classmethod
184 def fromstring(cls, string):
185 domain = Domain.fromstring(string)
186 if not isinstance(domain, Polyhedron):
187 raise ValueError('non-polyhedral expression: {!r}'.format(string))
188 return domain
189
190 def __repr__(self):
191 strings = []
192 for equality in self.equalities:
193 strings.append('Eq({}, 0)'.format(equality))
194 for inequality in self.inequalities:
195 strings.append('Ge({}, 0)'.format(inequality))
196 if len(strings) == 1:
197 return strings[0]
198 else:
199 return 'And({})'.format(', '.join(strings))
200
201 def _repr_latex_(self):
202 strings = []
203 for equality in self.equalities:
204 strings.append('{} = 0'.format(equality._repr_latex_().strip('$')))
205 for inequality in self.inequalities:
206 strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('$')))
207 return '$${}$$'.format(' \\wedge '.join(strings))
208
209 @classmethod
210 def fromsympy(cls, expr):
211 domain = Domain.fromsympy(expr)
212 if not isinstance(domain, Polyhedron):
213 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
214 return domain
215
216 def tosympy(self):
217 import sympy
218 constraints = []
219 for equality in self.equalities:
220 constraints.append(sympy.Eq(equality.tosympy(), 0))
221 for inequality in self.inequalities:
222 constraints.append(sympy.Ge(inequality.tosympy(), 0))
223 return sympy.And(*constraints)
224
225
226 class EmptyType(Polyhedron):
227
228 __slots__ = Polyhedron.__slots__
229
230 def __new__(cls):
231 self = object().__new__(cls)
232 self._equalities = (Rational(1),)
233 self._inequalities = ()
234 self._constraints = self._equalities
235 self._symbols = ()
236 self._dimension = 0
237 return self
238
239 def __repr__(self):
240 return 'Empty'
241
242 def _repr_latex_(self):
243 return '$$\\emptyset$$'
244
245 Empty = EmptyType()
246
247
248 class UniverseType(Polyhedron):
249
250 __slots__ = Polyhedron.__slots__
251
252 def __new__(cls):
253 self = object().__new__(cls)
254 self._equalities = ()
255 self._inequalities = ()
256 self._constraints = ()
257 self._symbols = ()
258 self._dimension = ()
259 return self
260
261 def __repr__(self):
262 return 'Universe'
263
264 def _repr_latex_(self):
265 return '$$\\Omega$$'
266
267 Universe = UniverseType()
268
269
270 def _polymorphic(func):
271 @functools.wraps(func)
272 def wrapper(left, right):
273 if not isinstance(left, Expression):
274 if isinstance(left, numbers.Rational):
275 left = Rational(left)
276 else:
277 raise TypeError('left must be a a rational number '
278 'or a linear expression')
279 if not isinstance(right, Expression):
280 if isinstance(right, numbers.Rational):
281 right = Rational(right)
282 else:
283 raise TypeError('right must be a a rational number '
284 'or a linear expression')
285 return func(left, right)
286 return wrapper
287
288 @_polymorphic
289 def Lt(left, right):
290 """
291 Return true if the first set is less than the second.
292 """
293 return Polyhedron([], [right - left - 1])
294
295 @_polymorphic
296 def Le(left, right):
297 """
298 Return true the first set is less than or equal to the second.
299 """
300 return Polyhedron([], [right - left])
301
302 @_polymorphic
303 def Eq(left, right):
304 """
305 Return true if the sets are equal.
306 """
307 return Polyhedron([left - right], [])
308
309 @_polymorphic
310 def Ne(left, right):
311 """
312 Return true if the sets are NOT equal.
313 """
314 return ~Eq(left, right)
315
316 @_polymorphic
317 def Gt(left, right):
318 """
319 Return true if the first set is greater than the second set.
320 """
321 return Polyhedron([], [left - right - 1])
322
323 @_polymorphic
324 def Ge(left, right):
325 """
326 Return true if the first set is greater than or equal the second set.
327 """
328 return Polyhedron([], [left - right])