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