41716c146b754eb13e8ba663a01d04d94ab546e6
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 """
6 import ctypes, ctypes.util
7 import math
8 import numbers
9 import operator
10 import re
11 import functools
14 from decimal import Decimal
15 from fractions import Fraction
16 from functools import wraps
18 libisl = ctypes.CDLL(ctypes.util.find_library('isl'))
20 libisl.isl_printer_get_str.restype = ctypes.c_char_p
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
33 class Context:
35 __slots__ = ('_ic')
37 def __init__(self):
38 self._ic = libisl.isl_ctx_alloc()
40 @property
41 def _as_parameter_(self):
42 return self._ic
44 #def __del__(self):
45 # libisl.isl_ctx_free(self)
47 def __eq__(self, other):
48 if not isinstance(other, Context):
49 return False
50 return self._ic == other._ic
53 class Value:
55 class _ptr(int):
56 def __new__(cls, iv):
57 return super().__new__(cls, iv)
58 def __repr__(self):
59 return '{}({})'.format(self.__class__.__name__, self)
61 _RE_NONFINITE = re.compile(
62 r'^\s*(?P<sign>[-+])?((?P<inf>Inf(inity)?)|(?P<nan>NaN))\s*\$',
63 re.IGNORECASE)
65 _RE_FRACTION = re.compile(r'^(?P<num>[-+]?\d+)(/(?P<den>\d+))?\$')
67 __slots__ = ('context', '_iv', '_numerator', '_denominator')
69 def __new__(cls, context, numerator=0, denominator=None):
70 self = super().__new__(cls)
71 if not isinstance(context, Context):
72 raise TypeError('first argument should be a context')
73 self.context = context
74 if isinstance(numerator, cls._ptr):
75 assert denominator is None
76 self._iv = numerator
77 if libisl.isl_val_is_rat(self):
78 # retrieve numerator and denominator as strings to avoid integer
79 # overflows
80 ip = libisl.isl_printer_to_str(self.context)
81 ip = libisl.isl_printer_print_val(ip, self)
82 string = libisl.isl_printer_get_str(ip).decode()
83 libisl.isl_printer_free(ip)
84 m = self._RE_FRACTION.match(string)
85 assert m is not None
86 self._numerator = int(m.group('num'))
87 self._denominator = int(m.group('den')) if m.group('den') else 1
88 else:
89 self._numerator = None
90 self._denominator = None
91 return self
92 if isinstance(numerator, str) and denominator is None:
93 m = self._RE_NONFINITE.match(numerator)
94 if m is not None:
95 self._numerator = None
96 self._denominator = None
97 if m.group('inf'):
98 if m.group('sign') == '-':
99 self._iv = libisl.isl_val_neginfty(context)
100 else:
101 self._iv = libisl.isl_val_infty(context)
102 else:
103 assert m.group('nan')
104 self._iv = libisl.isl_val_nan(context)
105 return self
106 try:
107 frac = Fraction(numerator, denominator)
108 except ValueError:
109 raise ValueError('invalid literal for {}: {!r}'.format(
110 cls.__name__, numerator))
111 self._numerator = frac.numerator
112 self._denominator = frac.denominator
113 # values passed as strings to avoid integer overflows
114 if frac.denominator == 1:
115 numerator = str(frac.numerator).encode()
117 else:
118 numerator = str(frac.numerator).encode()
120 denominator = str(frac.denominator).encode()
122 self._iv = libisl.isl_val_div(numerator, denominator)
123 print('in isl')
124 return self
127 @property
128 def _as_parameter_(self):
129 return self._iv
131 def symbols(self):
132 s = set()
133 for constraint in self.constraints():
134 s.update(constraint.symbols)
135 yield from sorted(s)
137 def __del__(self):
138 libisl.isl_val_free(self)
139 self.context # prevents context from being GC'ed before the value
141 @property
142 def numerator(self):
143 if self._numerator is None:
144 raise ValueError('not a rational number')
145 return self._numerator
147 @property
148 def denominator(self):
149 if self._denominator is None:
150 raise ValueError('not a rational number')
151 return self._denominator
153 def __bool__(self):
154 return not bool(libisl.isl_val_is_zero(self))
156 @_polymorphic_method
157 def __lt__(self, other):
158 return bool(libisl.isl_val_lt(self, other))
160 @_polymorphic_method
161 def __le__(self, other):
162 return bool(libisl.isl_val_le(self, other))
164 @_polymorphic_method
165 def __gt__(self, other):
166 return bool(libisl.isl_val_gt(self, other))
168 @_polymorphic_method
169 def __ge__(self, other):
170 return bool(libisl.isl_val_ge(self, other))
172 @_polymorphic_method
173 def __eq__(self, other):
174 return bool(libisl.isl_val_eq(self, other))
176 # __ne__ is not implemented, ISL semantics does not match Python's on
177 # nan != nan
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))
184 def __pos__(self):
185 return self
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))
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))
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))
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))
207 @_polymorphic_method
209 val1 = libisl.isl_val_copy(self)
210 val2 = libisl.isl_val_copy(other)
212 return self.__class__(self.context, self._ptr(val))
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))
223 __rsub__ = __sub__
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))
232 __rmul__ = __mul__
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))
241 __rtruediv__ = __truediv__
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')
254 def is_finite(self):
255 return bool(libisl.isl_val_is_rat(self))
257 def is_infinite(self):
258 return bool(libisl.isl_val_is_infty(self) or
259 libisl.isl_val_is_neginfty(self))
261 def is_nan(self):
262 return bool(libisl.isl_val_is_nan(self))
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'
278 def __repr__(self):
279 return '{}({!r})'.format(self.__class__.__name__, str(self))