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))