printing out isl form but test gives incorrect values
[linpy.git] / pypol / isl.py
1 """
2 note: for islpy
3 isl format: basic set: ("{[x, y] : x >= 0 and x < 5 and y >= 0 and y < x+4 }")
4 """
5
6 import ctypes, ctypes.util
7 import math
8 import numbers
9 import operator
10 import re
11 import functools
12
13
14 from decimal import Decimal
15 from fractions import Fraction
16 from functools import wraps
17
18 libisl = ctypes.CDLL(ctypes.util.find_library('isl'))
19
20 libisl.isl_printer_get_str.restype = ctypes.c_char_p
21
22 def _polymorphic_method(func):
23 @functools.wraps(func)
24 def wrapper(self, other):
25 if isinstance(other, Value):
26 return func(self, other)
27 if isinstance(other, numbers.Rational):
28 other = Value(self.context, other)
29 return func(self, other)
30 raise TypeError('operand should be a Value or a Rational')
31 return wrapper
32
33 class Context:
34
35 __slots__ = ('_ic')
36
37 def __init__(self):
38 self._ic = libisl.isl_ctx_alloc()
39
40 @property
41 def _as_parameter_(self):
42 return self._ic
43
44 #comment out so does not delete itself after being created
45 #def __del__(self):
46 # libisl.isl_ctx_free(self)
47
48 def __eq__(self, other):
49 if not isinstance(other, Context):
50 return False
51 return self._ic == other._ic
52
53
54 class Value:
55
56 class _ptr(int):
57 def __new__(cls, iv):
58 return super().__new__(cls, iv)
59 def __repr__(self):
60 return '{}({})'.format(self.__class__.__name__, self)
61
62 _RE_NONFINITE = re.compile(
63 r'^\s*(?P<sign>[-+])?((?P<inf>Inf(inity)?)|(?P<nan>NaN))\s*$',
64 re.IGNORECASE)
65
66 _RE_FRACTION = re.compile(r'^(?P<num>[-+]?\d+)(/(?P<den>\d+))?$')
67
68 __slots__ = ('context', '_iv', '_numerator', '_denominator')
69
70 def __new__(cls, context, numerator=0, denominator=None):
71 self = super().__new__(cls)
72 if not isinstance(context, Context):
73 raise TypeError('first argument should be a context')
74 self.context = context
75 if isinstance(numerator, cls._ptr):
76 assert denominator is None
77 self._iv = numerator
78 if libisl.isl_val_is_rat(self):
79 # retrieve numerator and denominator as strings to avoid integer
80 # overflows
81 ip = libisl.isl_printer_to_str(self.context)
82 ip = libisl.isl_printer_print_val(ip, self)
83 string = libisl.isl_printer_get_str(ip).decode()
84 libisl.isl_printer_free(ip)
85 m = self._RE_FRACTION.match(string)
86 assert m is not None
87 self._numerator = int(m.group('num'))
88 self._denominator = int(m.group('den')) if m.group('den') else 1
89 else:
90 self._numerator = None
91 self._denominator = None
92 return self
93 if isinstance(numerator, str) and denominator is None:
94 m = self._RE_NONFINITE.match(numerator)
95 if m is not None:
96 self._numerator = None
97 self._denominator = None
98 if m.group('inf'):
99 if m.group('sign') == '-':
100 self._iv = libisl.isl_val_neginfty(context)
101 else:
102 self._iv = libisl.isl_val_infty(context)
103 else:
104 assert m.group('nan')
105 self._iv = libisl.isl_val_nan(context)
106 return self
107 try:
108 frac = Fraction(numerator, denominator)
109 except ValueError:
110 raise ValueError('invalid literal for {}: {!r}'.format(
111 cls.__name__, numerator))
112 self._numerator = frac.numerator
113 self._denominator = frac.denominator
114 # values passed as strings to avoid integer overflows
115 if frac.denominator == 1:
116 numerator = str(frac.numerator).encode()
117 self._iv = libisl.isl_val_read_from_str(context, numerator)
118 else:
119 numerator = str(frac.numerator).encode()
120 numerator = libisl.isl_val_read_from_str(context, numerator)
121 denominator = str(frac.denominator).encode()
122 denominator = libisl.isl_val_read_from_str(context, denominator)
123 self._iv = libisl.isl_val_div(numerator, denominator)
124 return self
125
126
127 @property
128 def _as_parameter_(self):
129 return self._iv
130
131 def symbols(self):
132 s = set()
133 for constraint in self.constraints():
134 s.update(constraint.symbols)
135 yield from sorted(s)
136
137 def __del__(self):
138 libisl.isl_val_free(self)
139 self.context # prevents context from being GC'ed before the value
140
141 @property
142 def numerator(self):
143 if self._numerator is None:
144 raise ValueError('not a rational number')
145 return self._numerator
146
147 @property
148 def denominator(self):
149 if self._denominator is None:
150 raise ValueError('not a rational number')
151 return self._denominator
152
153 def __bool__(self):
154 return not bool(libisl.isl_val_is_zero(self))
155
156 @_polymorphic_method
157 def __lt__(self, other):
158 return bool(libisl.isl_val_lt(self, other))
159
160 @_polymorphic_method
161 def __le__(self, other):
162 return bool(libisl.isl_val_le(self, other))
163
164 @_polymorphic_method
165 def __gt__(self, other):
166 return bool(libisl.isl_val_gt(self, other))
167
168 @_polymorphic_method
169 def __ge__(self, other):
170 return bool(libisl.isl_val_ge(self, other))
171
172 @_polymorphic_method
173 def __eq__(self, other):
174 return bool(libisl.isl_val_eq(self, other))
175
176 # __ne__ is not implemented, ISL semantics does not match Python's on
177 # nan != nan
178
179 def __abs__(self):
180 val = libisl.isl_val_copy(self)
181 val = libisl.isl_val_abs(val)
182 return self.__class__(self.context, self._ptr(val))
183
184 def __pos__(self):
185 return self
186
187 def __neg__(self):
188 val = libisl.isl_val_copy(self)
189 val = libisl.isl_val_neg(val)
190 return self.__class__(self.context, self._ptr(val))
191
192 def __floor__(self):
193 val = libisl.isl_val_copy(self)
194 val = libisl.isl_val_floor(val)
195 return self.__class__(self.context, self._ptr(val))
196
197 def __ceil__(self):
198 val = libisl.isl_val_copy(self)
199 val = libisl.isl_val_ceil(val)
200 return self.__class__(self.context, self._ptr(val))
201
202 def __trunc__(self):
203 val = libisl.isl_val_copy(self)
204 val = libisl.isl_val_trunc(val)
205 return self.__class__(self.context, self._ptr(val))
206
207 @_polymorphic_method
208 def __add__(self, other):
209 val1 = libisl.isl_val_copy(self)
210 val2 = libisl.isl_val_copy(other)
211 val = libisl.isl_val_add(val1, val2)
212 return self.__class__(self.context, self._ptr(val))
213
214 __radd__ = __add__
215
216 @_polymorphic_method
217 def __sub__(self, other):
218 val1 = libisl.isl_val_copy(self)
219 val2 = libisl.isl_val_copy(other)
220 val = libisl.isl_val_sub(val1, val2)
221 return self.__class__(self.context, self._ptr(val))
222
223 __rsub__ = __sub__
224
225 @_polymorphic_method
226 def __mul__(self, other):
227 val1 = libisl.isl_val_copy(self)
228 val2 = libisl.isl_val_copy(other)
229 val = libisl.isl_val_mul(val1, val2)
230 return self.__class__(self.context, self._ptr(val))
231
232 __rmul__ = __mul__
233
234 @_polymorphic_method
235 def __truediv__(self, other):
236 val1 = libisl.isl_val_copy(self)
237 val2 = libisl.isl_val_copy(other)
238 val = libisl.isl_val_div(val1, val2)
239 return self.__class__(self.context, self._ptr(val))
240
241 __rtruediv__ = __truediv__
242
243 def __float__(self):
244 if libisl.isl_val_is_rat(self):
245 return self.numerator / self.denominator
246 elif libisl.isl_val_is_infty(self):
247 return float('inf')
248 elif libisl.isl_val_is_neginfty(self):
249 return float('-inf')
250 else:
251 assert libisl.isl_val_is_nan(self)
252 return float('nan')
253
254 def is_finite(self):
255 return bool(libisl.isl_val_is_rat(self))
256
257 def is_infinite(self):
258 return bool(libisl.isl_val_is_infty(self) or
259 libisl.isl_val_is_neginfty(self))
260
261 def is_nan(self):
262 return bool(libisl.isl_val_is_nan(self))
263
264 def __str__(self):
265 if libisl.isl_val_is_rat(self):
266 if self.denominator == 1:
267 return '{}'.format(self.numerator)
268 else:
269 return '{}/{}'.format(self.numerator, self.denominator)
270 elif libisl.isl_val_is_infty(self):
271 return 'Infinity'
272 elif libisl.isl_val_is_neginfty(self):
273 return '-Infinity'
274 else:
275 assert libisl.isl_val_is_nan(self)
276 return 'NaN'
277
278 def __repr__(self):
279 return '{}({!r})'.format(self.__class__.__name__, str(self))