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     #def __del__(self):
  45      #   libisl.isl_ctx_free(self)
  46
  47     def __eq__(self, other):
  48         if not isinstance(other, Context):
  49             return False
  50         return self._ic == other._ic
  51
  52
  53 class Value:
  54
  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)
  60
  61     _RE_NONFINITE = re.compile(
  62             r'^\s*(?P<sign>[-+])?((?P<inf>Inf(inity)?)|(?P<nan>NaN))\s*$',
  63             re.IGNORECASE)
  64
  65     _RE_FRACTION = re.compile(r'^(?P<num>[-+]?\d+)(/(?P<den>\d+))?$')
  66
  67     __slots__ = ('context', '_iv', '_numerator', '_denominator')
  68
  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()
 116             self._iv = libisl.isl_val_read_from_str(context, numerator)
 117         else:
 118             numerator = str(frac.numerator).encode()
 119             numerator = libisl.isl_val_read_from_str(context, numerator)
 120             denominator = str(frac.denominator).encode()
 121             denominator = libisl.isl_val_read_from_str(context, denominator)
 122             self._iv = libisl.isl_val_div(numerator, denominator)
 123         print('in isl')
 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))