New example from French Baccalauréat 2014 (courtesy of Pierre Guillou)
[linpy.git] / pypol / domains.py
1 import functools
2
3 from . import islhelper
4
5 from .islhelper import mainctx, libisl, isl_set_basic_sets
6
7
8 __all__ = [
9 'Domain',
10 'And', 'Or', 'Not',
11 ]
12
13
14 @functools.total_ordering
15 class Domain:
16
17 __slots__ = (
18 '_polyhedra',
19 '_symbols',
20 '_dimension',
21 )
22
23 def __new__(cls, *polyhedra):
24 from .polyhedra import Polyhedron
25 if len(polyhedra) == 1:
26 polyhedron = polyhedra[0]
27 if isinstance(polyhedron, str):
28 return cls.fromstring(polyhedron)
29 elif isinstance(polyhedron, Polyhedron):
30 return polyhedron
31 else:
32 raise TypeError('argument must be a string '
33 'or a Polyhedron instance')
34 else:
35 for polyhedron in polyhedra:
36 if not isinstance(polyhedron, Polyhedron):
37 raise TypeError('arguments must be Polyhedron instances')
38 symbols = cls._xsymbols(polyhedra)
39 islset = cls._toislset(polyhedra, symbols)
40 return cls._fromislset(islset, symbols)
41
42 @classmethod
43 def _xsymbols(cls, iterator):
44 """
45 Return the ordered tuple of symbols present in iterator.
46 """
47 symbols = set()
48 for item in iterator:
49 symbols.update(item.symbols)
50 return tuple(sorted(symbols))
51
52 @property
53 def polyhedra(self):
54 return self._polyhedra
55
56 @property
57 def symbols(self):
58 return self._symbols
59
60 @property
61 def dimension(self):
62 return self._dimension
63
64 def disjoint(self):
65 islset = self._toislset(self.polyhedra, self.symbols)
66 islset = libisl.isl_set_make_disjoint(mainctx, islset)
67 return self._fromislset(islset, self.symbols)
68
69 def isempty(self):
70 islset = self._toislset(self.polyhedra, self.symbols)
71 empty = bool(libisl.isl_set_is_empty(islset))
72 libisl.isl_set_free(islset)
73 return empty
74
75 def __bool__(self):
76 return not self.isempty()
77
78 def isuniverse(self):
79 islset = self._toislset(self.polyhedra, self.symbols)
80 universe = bool(libisl.isl_set_plain_is_universe(islset))
81 libisl.isl_set_free(islset)
82 return universe
83
84 def __eq__(self, other):
85 symbols = self._xsymbols([self, other])
86 islset1 = self._toislset(self.polyhedra, symbols)
87 islset2 = other._toislset(other.polyhedra, symbols)
88 equal = bool(libisl.isl_set_is_equal(islset1, islset2))
89 libisl.isl_set_free(islset1)
90 libisl.isl_set_free(islset2)
91 return equal
92
93 def isdisjoint(self, other):
94 symbols = self._xsymbols([self, other])
95 islset1 = self._toislset(self.polyhedra, symbols)
96 islset2 = self._toislset(other.polyhedra, symbols)
97 equal = bool(libisl.isl_set_is_disjoint(islset1, islset2))
98 libisl.isl_set_free(islset1)
99 libisl.isl_set_free(islset2)
100 return equal
101
102 def issubset(self, other):
103 symbols = self._xsymbols([self, other])
104 islset1 = self._toislset(self.polyhedra, symbols)
105 islset2 = self._toislset(other.polyhedra, symbols)
106 equal = bool(libisl.isl_set_is_subset(islset1, islset2))
107 libisl.isl_set_free(islset1)
108 libisl.isl_set_free(islset2)
109 return equal
110
111 def __le__(self, other):
112 return self.issubset(other)
113
114 def __lt__(self, other):
115 symbols = self._xsymbols([self, other])
116 islset1 = self._toislset(self.polyhedra, symbols)
117 islset2 = self._toislset(other.polyhedra, symbols)
118 equal = bool(libisl.isl_set_is_strict_subset(islset1, islset2))
119 libisl.isl_set_free(islset1)
120 libisl.isl_set_free(islset2)
121 return equal
122
123 def complement(self):
124 islset = self._toislset(self.polyhedra, self.symbols)
125 islset = libisl.isl_set_complement(islset)
126 return self._fromislset(islset, self.symbols)
127
128 def __invert__(self):
129 return self.complement()
130
131 def simplify(self):
132 # see isl_set_coalesce, isl_set_detect_equalities,
133 # isl_set_remove_redundancies
134 # which ones? in which order?
135 raise NotImplementedError
136
137 def polyhedral_hull(self):
138 # several types of hull are available
139 # polyhedral seems to be the more appropriate, to be checked
140 from .polyhedra import Polyhedron
141 islset = self._toislset(self.polyhedra, self.symbols)
142 islbset = libisl.isl_set_polyhedral_hull(islset)
143 return Polyhedron._fromislbasicset(islbset, self.symbols)
144
145 def project(self, symbols):
146 # not sure what isl_set_project_out actually does…
147 # use isl_set_drop_constraints_involving_dims instead?
148 raise NotImplementedError
149
150 def sample(self):
151 from .polyhedra import Polyhedron
152 islset = self._toislset(self.polyhedra, self.symbols)
153 islbset = libisl.isl_set_sample(islset)
154 return Polyhedron._fromislbasicset(islbset, self.symbols)
155
156 def intersection(self, *others):
157 if len(others) == 0:
158 return self
159 symbols = self._xsymbols((self,) + others)
160 islset1 = self._toislset(self.polyhedra, symbols)
161 for other in others:
162 islset2 = other._toislset(other.polyhedra, symbols)
163 islset1 = libisl.isl_set_intersect(islset1, islset2)
164 return self._fromislset(islset1, symbols)
165
166 def __and__(self, other):
167 return self.intersection(other)
168
169 def union(self, *others):
170 if len(others) == 0:
171 return self
172 symbols = self._xsymbols((self,) + others)
173 islset1 = self._toislset(self.polyhedra, symbols)
174 for other in others:
175 islset2 = other._toislset(other.polyhedra, symbols)
176 islset1 = libisl.isl_set_union(islset1, islset2)
177 return self._fromislset(islset1, symbols)
178
179 def __or__(self, other):
180 return self.union(other)
181
182 def __add__(self, other):
183 return self.union(other)
184
185 def difference(self, other):
186 symbols = self._xsymbols([self, other])
187 islset1 = self._toislset(self.polyhedra, symbols)
188 islset2 = other._toislset(other.polyhedra, symbols)
189 islset = libisl.isl_set_subtract(islset1, islset2)
190 return self._fromislset(islset, symbols)
191
192 def __sub__(self, other):
193 return self.difference(other)
194
195 def lexmin(self):
196 islset = self._toislset(self.polyhedra, self.symbols)
197 islset = libisl.isl_set_lexmin(islset)
198 return self._fromislset(islset, self.symbols)
199
200 def lexmax(self):
201 islset = self._toislset(self.polyhedra, self.symbols)
202 islset = libisl.isl_set_lexmax(islset)
203 return self._fromislset(islset, self.symbols)
204
205 @classmethod
206 def _fromislset(cls, islset, symbols):
207 from .polyhedra import Polyhedron
208 islset = libisl.isl_set_remove_divs(islset)
209 islbsets = isl_set_basic_sets(islset)
210 libisl.isl_set_free(islset)
211 polyhedra = []
212 for islbset in islbsets:
213 polyhedron = Polyhedron._fromislbasicset(islbset, symbols)
214 polyhedra.append(polyhedron)
215 if len(polyhedra) == 0:
216 from .polyhedra import Empty
217 return Empty
218 elif len(polyhedra) == 1:
219 return polyhedra[0]
220 else:
221 self = object().__new__(Domain)
222 self._polyhedra = tuple(polyhedra)
223 self._symbols = cls._xsymbols(polyhedra)
224 self._dimension = len(self._symbols)
225 return self
226
227 def _toislset(cls, polyhedra, symbols):
228 polyhedron = polyhedra[0]
229 islbset = polyhedron._toislbasicset(polyhedron.equalities,
230 polyhedron.inequalities, symbols)
231 islset1 = libisl.isl_set_from_basic_set(islbset)
232 for polyhedron in polyhedra[1:]:
233 islbset = polyhedron._toislbasicset(polyhedron.equalities,
234 polyhedron.inequalities, symbols)
235 islset2 = libisl.isl_set_from_basic_set(islbset)
236 islset1 = libisl.isl_set_union(islset1, islset2)
237 return islset1
238
239 @classmethod
240 def fromstring(cls, string):
241 raise NotImplementedError
242
243 def __repr__(self):
244 assert len(self.polyhedra) >= 2
245 strings = [repr(polyhedron) for polyhedron in self.polyhedra]
246 return 'Or({})'.format(', '.join(strings))
247
248 @classmethod
249 def fromsympy(cls, expr):
250 raise NotImplementedError
251
252 def tosympy(self):
253 raise NotImplementedError
254
255
256 def And(*domains):
257 if len(domains) == 0:
258 from .polyhedra import Universe
259 return Universe
260 else:
261 return domains[0].intersection(*domains[1:])
262
263 def Or(*domains):
264 if len(domains) == 0:
265 from .polyhedra import Empty
266 return Empty
267 else:
268 return domains[0].union(*domains[1:])
269
270 def Not(domain):
271 return ~domain