pypol/linear.py

   1 import functools
   2 import numbers
   3 import ctypes, ctypes.util
   4 from pypol import isl
   5
   6 from fractions import Fraction, gcd
   7
   8 libisl = ctypes.CDLL(ctypes.util.find_library('isl'))
   9
  10 libisl.isl_printer_get_str.restype = ctypes.c_char_p
  11
  12 __all__ = [
  13     'Expression',
  14     'constant', 'symbol', 'symbols',
  15     'eq', 'le', 'lt', 'ge', 'gt',
  16     'Polyhedron',
  17     'empty', 'universe'
  18 ]
  19
  20
  21 _CONTEXT = isl.Context()
  22
  23 def _polymorphic_method(func):
  24     @functools.wraps(func)
  25     def wrapper(a, b):
  26         if isinstance(b, Expression):
  27             return func(a, b)
  28         if isinstance(b, numbers.Rational):
  29             b = constant(b)
  30             return func(a, b)
  31         return NotImplemented
  32     return wrapper
  33
  34 def _polymorphic_operator(func):
  35     # A polymorphic operator should call a polymorphic method, hence we just
  36     # have to test the left operand.
  37     @functools.wraps(func)
  38     def wrapper(a, b):
  39         if isinstance(a, numbers.Rational):
  40             a = constant(a)
  41             return func(a, b)
  42         elif isinstance(a, Expression):
  43             return func(a, b)
  44         raise TypeError('arguments must be linear expressions')
  45     return wrapper
  46
  47
  48 class Expression:
  49     """
  50     This class implements linear expressions.
  51     """
  52
  53     def __new__(cls, coefficients=None, constant=0):
  54         if isinstance(coefficients, str):
  55             if constant:
  56                 raise TypeError('too many arguments')
  57             return cls.fromstring(coefficients)
  58         self = super().__new__(cls)
  59         self._coefficients = {}
  60         if isinstance(coefficients, dict):
  61             coefficients = coefficients.items()
  62         if coefficients is not None:
  63             for symbol, coefficient in coefficients:
  64                 if isinstance(symbol, Expression) and symbol.issymbol():
  65                     symbol = str(symbol)
  66                 elif not isinstance(symbol, str):
  67                     raise TypeError('symbols must be strings')
  68                 if not isinstance(coefficient, numbers.Rational):
  69                     raise TypeError('coefficients must be rational numbers')
  70                 if coefficient != 0:
  71                     self._coefficients[symbol] = coefficient
  72         if not isinstance(constant, numbers.Rational):
  73             raise TypeError('constant must be a rational number')
  74         self._constant = constant
  75         return self
  76
  77
  78     def symbols(self):
  79         yield from sorted(self._coefficients)
  80
  81     @property
  82     def dimension(self):
  83         return len(list(self.symbols()))
  84
  85     def coefficient(self, symbol):
  86         if isinstance(symbol, Expression) and symbol.issymbol():
  87             symbol = str(symbol)
  88         elif not isinstance(symbol, str):
  89             raise TypeError('symbol must be a string')
  90         try:
  91             return self._coefficients[symbol]
  92         except KeyError:
  93             return 0
  94
  95     __getitem__ = coefficient
  96
  97     def coefficients(self):
  98         for symbol in self.symbols():
  99             yield symbol, self.coefficient(symbol)
 100
 101     @property
 102     def constant(self):
 103         return self._constant
 104
 105     def isconstant(self):
 106         return len(self._coefficients) == 0
 107
 108     def values(self):
 109         for symbol in self.symbols():
 110             yield self.coefficient(symbol)
 111         yield self.constant
 112
 113     def values_int(self):
 114         for symbol in self.symbols():
 115             return self.coefficient(symbol)
 116         return int(self.constant)
 117
 118
 119     def symbol(self):
 120         if not self.issymbol():
 121             raise ValueError('not a symbol: {}'.format(self))
 122         for symbol in self.symbols():
 123             return symbol
 124
 125     def issymbol(self):
 126         return len(self._coefficients) == 1 and self._constant == 0
 127
 128     def __bool__(self):
 129         return (not self.isconstant()) or bool(self.constant)
 130
 131     def __pos__(self):
 132         return self
 133
 134     def __neg__(self):
 135         return self * -1
 136
 137     @_polymorphic_method
 138     def __add__(self, other):
 139         coefficients = dict(self.coefficients())
 140         for symbol, coefficient in other.coefficients():
 141             if symbol in coefficients:
 142                 coefficients[symbol] += coefficient
 143             else:
 144                 coefficients[symbol] = coefficient
 145         constant = self.constant + other.constant
 146         return Expression(coefficients, constant)
 147
 148     __radd__ = __add__
 149
 150     @_polymorphic_method
 151     def __sub__(self, other):
 152         coefficients = dict(self.coefficients())
 153         for symbol, coefficient in other.coefficients():
 154             if symbol in coefficients:
 155                 coefficients[symbol] -= coefficient
 156             else:
 157                 coefficients[symbol] = -coefficient
 158         constant = self.constant - other.constant
 159         return Expression(coefficients, constant)
 160
 161     __rsub__ = __sub__
 162
 163     @_polymorphic_method
 164     def __mul__(self, other):
 165         if other.isconstant():
 166             coefficients = dict(self.coefficients())
 167             for symbol in coefficients:
 168                 coefficients[symbol] *= other.constant
 169             constant = self.constant * other.constant
 170             return Expression(coefficients, constant)
 171         if isinstance(other, Expression) and not self.isconstant():
 172             raise ValueError('non-linear expression: '
 173                     '{} * {}'.format(self._parenstr(), other._parenstr()))
 174         return NotImplemented
 175
 176     __rmul__ = __mul__
 177
 178     @_polymorphic_method
 179     def __truediv__(self, other):
 180         if other.isconstant():
 181             coefficients = dict(self.coefficients())
 182             for symbol in coefficients:
 183                 coefficients[symbol] = \
 184                         Fraction(coefficients[symbol], other.constant)
 185             constant = Fraction(self.constant, other.constant)
 186             return Expression(coefficients, constant)
 187         if isinstance(other, Expression):
 188             raise ValueError('non-linear expression: '
 189                 '{} / {}'.format(self._parenstr(), other._parenstr()))
 190         return NotImplemented
 191
 192     def __rtruediv__(self, other):
 193         if isinstance(other, self):
 194             if self.isconstant():
 195                 constant = Fraction(other, self.constant)
 196                 return Expression(constant=constant)
 197             else:
 198                 raise ValueError('non-linear expression: '
 199                         '{} / {}'.format(other._parenstr(), self._parenstr()))
 200         return NotImplemented
 201
 202     def __str__(self):
 203         string = ''
 204         symbols = sorted(self.symbols())
 205         i = 0
 206         for symbol in symbols:
 207             coefficient = self[symbol]
 208             if coefficient == 1:
 209                 if i == 0:
 210                     string += symbol
 211                 else:
 212                     string += ' + {}'.format(symbol)
 213             elif coefficient == -1:
 214                 if i == 0:
 215                     string += '-{}'.format(symbol)
 216                 else:
 217                     string += ' - {}'.format(symbol)
 218             else:
 219                 if i == 0:
 220                     string += '{}*{}'.format(coefficient, symbol)
 221                 elif coefficient > 0:
 222                     string += ' + {}*{}'.format(coefficient, symbol)
 223                 else:
 224                     assert coefficient < 0
 225                     coefficient *= -1
 226                     string += ' - {}*{}'.format(coefficient, symbol)
 227             i += 1
 228         constant = self.constant
 229         if constant != 0 and i == 0:
 230             string += '{}'.format(constant)
 231         elif constant > 0:
 232             string += ' + {}'.format(constant)
 233         elif constant < 0:
 234             constant *= -1
 235             string += ' - {}'.format(constant)
 236         if string == '':
 237             string = '0'
 238         return string
 239
 240     def _parenstr(self, always=False):
 241         string = str(self)
 242         if not always and (self.isconstant() or self.issymbol()):
 243             return string
 244         else:
 245             return '({})'.format(string)
 246
 247     def __repr__(self):
 248         string = '{}({{'.format(self.__class__.__name__)
 249         for i, (symbol, coefficient) in enumerate(self.coefficients()):
 250             if i != 0:
 251                 string += ', '
 252             string += '{!r}: {!r}'.format(symbol, coefficient)
 253         string += '}}, {!r})'.format(self.constant)
 254         return string
 255
 256     @classmethod
 257     def fromstring(cls, string):
 258         raise NotImplementedError
 259
 260     @_polymorphic_method
 261     def __eq__(self, other):
 262         # "normal" equality
 263         # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs
 264         return isinstance(other, Expression) and \
 265                 self._coefficients == other._coefficients and \
 266                 self.constant == other.constant
 267
 268     def __hash__(self):
 269         return hash((self._coefficients, self._constant))
 270
 271     def _canonify(self):
 272         lcm = functools.reduce(lambda a, b: a*b // gcd(a, b),
 273                 [value.denominator for value in self.values()])
 274         return self * lcm
 275
 276     @_polymorphic_method
 277     def _eq(self, other):
 278         return Polyhedron(equalities=[(self - other)._canonify()])
 279
 280     @_polymorphic_method
 281     def __le__(self, other):
 282         return Polyhedron(inequalities=[(self - other)._canonify()])
 283
 284     @_polymorphic_method
 285     def __lt__(self, other):
 286         return Polyhedron(inequalities=[(self - other)._canonify() + 1])
 287
 288     @_polymorphic_method
 289     def __ge__(self, other):
 290         return Polyhedron(inequalities=[(other - self)._canonify()])
 291
 292     @_polymorphic_method
 293     def __gt__(self, other):
 294         return Polyhedron(inequalities=[(other - self)._canonify() + 1])
 295
 296
 297 def constant(numerator=0, denominator=None):
 298     if denominator is None and isinstance(numerator, numbers.Rational):
 299         return Expression(constant=numerator)
 300     else:
 301         return Expression(constant=Fraction(numerator, denominator))
 302
 303 def symbol(name):
 304     if not isinstance(name, str):
 305         raise TypeError('name must be a string')
 306     return Expression(coefficients={name: 1})
 307
 308 def symbols(names):
 309     if isinstance(names, str):
 310         names = names.replace(',', ' ').split()
 311     return (symbol(name) for name in names)
 312
 313
 314 @_polymorphic_operator
 315 def eq(a, b):
 316     return a._eq(b)
 317
 318 @_polymorphic_operator
 319 def le(a, b):
 320     return a <= b
 321
 322 @_polymorphic_operator
 323 def lt(a, b):
 324     return a < b
 325
 326 @_polymorphic_operator
 327 def ge(a, b):
 328     return a >= b
 329
 330 @_polymorphic_operator
 331 def gt(a, b):
 332     return a > b
 333
 334
 335 class Polyhedron:
 336     """
 337     This class implements polyhedrons.
 338     """
 339
 340     def __new__(cls, equalities=None, inequalities=None):
 341         if isinstance(equalities, str):
 342             if inequalities is not None:
 343                 raise TypeError('too many arguments')
 344             return cls.fromstring(equalities)
 345         self = super().__new__(cls)
 346         self._equalities = []
 347         if equalities is not None:
 348             for constraint in equalities:
 349                 for value in constraint.values():
 350                     if value.denominator != 1:
 351                         raise TypeError('non-integer constraint: '
 352                                 '{} == 0'.format(constraint))
 353                 self._equalities.append(constraint)
 354         self._inequalities = []
 355         if inequalities is not None:
 356             for constraint in inequalities:
 357                 for value in constraint.values():
 358                     if value.denominator != 1:
 359                         raise TypeError('non-integer constraint: '
 360                                 '{} <= 0'.format(constraint))
 361                 self._inequalities.append(constraint)
 362         print('in polyhedron')
 363         #print(self.constraints())
 364         self._bset = self.to_isl()
 365         #print(self._bset)
 366         return self
 367
 368
 369     @property
 370     def equalities(self):
 371         yield from self._equalities
 372
 373     @property
 374     def inequalities(self):
 375         yield from self._inequalities
 376
 377     @property
 378     def constant(self):
 379         return self._constant
 380
 381     def isconstant(self):
 382         return len(self._coefficients) == 0
 383
 384
 385     def isempty(self):
 386         return bool(libisl.isl_basic_set_is_empty(self._bset))
 387
 388     def constraints(self):
 389         yield from self.equalities
 390         yield from self.inequalities
 391
 392
 393     def symbols(self):
 394         s = set()
 395         for constraint in self.constraints():
 396             s.update(constraint.symbols)
 397             yield from sorted(s)
 398
 399     def symbol_count(self):
 400         s = []
 401         for constraint in self.constraints():
 402             s.append(constraint.symbols)
 403         print(s)
 404         return s
 405
 406     @property
 407     def dimension(self):
 408         return len(self.symbols())
 409
 410     def __bool__(self):
 411         # return false if the polyhedron is empty, true otherwise
 412         if self._equalities or self._inequalities:
 413             return False
 414         else:
 415             return True
 416
 417
 418     def __contains__(self, value):
 419         # is the value in the polyhedron?
 420         raise NotImplementedError
 421
 422     def __eq__(self, other):
 423         raise NotImplementedError
 424
 425     def is_empty(self):
 426         return
 427
 428     def isuniverse(self):
 429         return self == universe
 430
 431     def isdisjoint(self, other):
 432         # return true if the polyhedron has no elements in common with other
 433         raise NotImplementedError
 434
 435     def issubset(self, other):
 436         raise NotImplementedError
 437
 438     def __le__(self, other):
 439         return self.issubset(other)
 440
 441     def __lt__(self, other):
 442         raise NotImplementedError
 443
 444     def issuperset(self, other):
 445         # test whether every element in other is in the polyhedron
 446         for value in other:
 447             if value == self.constraints():
 448                 return True
 449             else:
 450                 return False
 451         raise NotImplementedError
 452
 453     def __ge__(self, other):
 454         return self.issuperset(other)
 455
 456     def __gt__(self, other):
 457         raise NotImplementedError
 458
 459     def union(self, *others):
 460         # return a new polyhedron with elements from the polyhedron and all
 461         # others (convex union)
 462         raise NotImplementedError
 463
 464     def __or__(self, other):
 465         return self.union(other)
 466
 467     def intersection(self, *others):
 468         # return a new polyhedron with elements common to the polyhedron and all
 469         # others
 470         # a poor man's implementation could be:
 471         # equalities = list(self.equalities)
 472         # inequalities = list(self.inequalities)
 473         # for other in others:
 474         #     equalities.extend(other.equalities)
 475         #     inequalities.extend(other.inequalities)
 476         # return self.__class__(equalities, inequalities)
 477         raise NotImplementedError
 478
 479     def __and__(self, other):
 480         return self.intersection(other)
 481
 482     def difference(self, *others):
 483         # return a new polyhedron with elements in the polyhedron that are not
 484         # in the others
 485         raise NotImplementedError
 486
 487     def __sub__(self, other):
 488         return self.difference(other)
 489
 490     def __str__(self):
 491         constraints = []
 492         for constraint in self.equalities:
 493             constraints.append('{} == 0'.format(constraint))
 494         for constraint in self.inequalities:
 495             constraints.append('{} <= 0'.format(constraint))
 496         return '{{{}}}'.format(', '.join(constraints))
 497
 498     def __repr__(self):
 499         equalities = list(self.equalities)
 500         inequalities = list(self.inequalities)
 501         return '{}(equalities={!r}, inequalities={!r})' \
 502                 ''.format(self.__class__.__name__, equalities, inequalities)
 503
 504     @classmethod
 505     def fromstring(cls, string):
 506         raise NotImplementedError
 507
 508     def printer(self):
 509
 510         ip = libisl.isl_printer_to_str(_CONTEXT)
 511         ip = libisl.isl_printer_print_val(ip, self)
 512         string = libisl.isl_printer_get_str(ip).decode()
 513         print(string)
 514         return string
 515
 516
 517     def to_isl(self):
 518         space = libisl.isl_space_set_alloc(_CONTEXT, 0, len(self.symbol_count()))
 519         bset = libisl.isl_basic_set_empty(libisl.isl_space_copy(space))
 520         ls = libisl.isl_local_space_from_space(libisl.isl_space_copy(space))
 521         ceq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(ls))
 522         cin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(ls))
 523         dict_ex = Expression().__dict__
 524         '''
 525         if there are equalities/inequalities, take each constant and coefficient and add as a constraint to the basic set
 526         need to change the symbols method to a lookup table for the integer value for each letter that could be a symbol
 527         '''
 528         if self.equalities:
 529             for _constant in dict_ex:
 530                 value = dict_ex.get('_constant')
 531                 ceq = libisl.isl_constraint_set_constant_val(ceq, value)
 532             for _coefficients in dict_ex:
 533                 value_co = dict_ex.get('_coefficients')
 534                 if value_co:
 535                     ceq = libisl.isl_constraint_set_coefficient_si(ceq, libisl.isl_set_dim, self.symbols(), value_co)
 536             bset = libisl.isl_set_add_constraint(bset, ceq)
 537
 538         elif self.inequalities:
 539             for _constant in dict_ex:
 540                 value = dict_ex.get('_constant')
 541                 cin = libisl.isl_constraint_set_constant_val(cin, value)
 542             for _coefficients in dict_ex:
 543                 value_co = dict_ex.get('_coefficients')
 544                 if value_co:
 545                     cin = libisl.isl_constraint_set_coefficient_si(cin, libisl.isl_set_dim, self.symbols(), value_co)
 546             bset = libisl.isl_set_add_contraint(bset, cin)
 547         string = self.printer()
 548         #string = libisl.isl_printer_print_basic_set(bset)
 549         print('here')
 550         print(string)
 551         print(self)
 552         return string
 553
 554 empty = eq(1, 1)
 555
 556
 557 universe = Polyhedron()