pypol/linear.py

   1 import ast
   2 import functools
   3 import numbers
   4 import re
   5
   6 from fractions import Fraction, gcd
   7
   8 from . import isl
   9 from .isl import libisl
  10
  11
  12 __all__ = [
  13     'Expression', 'Constant', 'Symbol', 'symbols',
  14     'eq', 'le', 'lt', 'ge', 'gt',
  15     'Polyhedron',
  16     'Empty', 'Universe'
  17 ]
  18
  19
  20 def _polymorphic_method(func):
  21     @functools.wraps(func)
  22     def wrapper(a, b):
  23         if isinstance(b, Expression):
  24             return func(a, b)
  25         if isinstance(b, numbers.Rational):
  26             b = Constant(b)
  27             return func(a, b)
  28         return NotImplemented
  29     return wrapper
  30
  31 def _polymorphic_operator(func):
  32     # A polymorphic operator should call a polymorphic method, hence we just
  33     # have to test the left operand.
  34     @functools.wraps(func)
  35     def wrapper(a, b):
  36         if isinstance(a, numbers.Rational):
  37             a = Constant(a)
  38             return func(a, b)
  39         elif isinstance(a, Expression):
  40             return func(a, b)
  41         raise TypeError('arguments must be linear expressions')
  42     return wrapper
  43
  44
  45 _main_ctx = isl.Context()
  46
  47
  48 class Expression:
  49     """
  50     This class implements linear expressions.
  51     """
  52
  53     __slots__ = (
  54         '_coefficients',
  55         '_constant',
  56         '_symbols',
  57         '_dimension',
  58     )
  59
  60     def __new__(cls, coefficients=None, constant=0):
  61         if isinstance(coefficients, str):
  62             if constant:
  63                 raise TypeError('too many arguments')
  64             return cls.fromstring(coefficients)
  65         if isinstance(coefficients, dict):
  66             coefficients = coefficients.items()
  67         if coefficients is None:
  68             return Constant(constant)
  69         coefficients = [(symbol, coefficient)
  70                 for symbol, coefficient in coefficients if coefficient != 0]
  71         if len(coefficients) == 0:
  72             return Constant(constant)
  73         elif len(coefficients) == 1 and constant == 0:
  74             symbol, coefficient = coefficients[0]
  75             if coefficient == 1:
  76                 return Symbol(symbol)
  77         self = object().__new__(cls)
  78         self._coefficients = {}
  79         for symbol, coefficient in coefficients:
  80             if isinstance(symbol, Symbol):
  81                 symbol = symbol.name
  82             elif not isinstance(symbol, str):
  83                 raise TypeError('symbols must be strings or Symbol instances')
  84             if isinstance(coefficient, Constant):
  85                 coefficient = coefficient.constant
  86             if not isinstance(coefficient, numbers.Rational):
  87                 raise TypeError('coefficients must be rational numbers or Constant instances')
  88             self._coefficients[symbol] = coefficient
  89         if isinstance(constant, Constant):
  90             constant = constant.constant
  91         if not isinstance(constant, numbers.Rational):
  92             raise TypeError('constant must be a rational number or a Constant instance')
  93         self._constant = constant
  94         self._symbols = tuple(sorted(self._coefficients))
  95         self._dimension = len(self._symbols)
  96         return self
  97
  98     @classmethod
  99     def _fromast(cls, node):
 100         if isinstance(node, ast.Module) and len(node.body) == 1:
 101             return cls._fromast(node.body[0])
 102         elif isinstance(node, ast.Expr):
 103             return cls._fromast(node.value)
 104         elif isinstance(node, ast.Name):
 105             return Symbol(node.id)
 106         elif isinstance(node, ast.Num):
 107             return Constant(node.n)
 108         elif isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub):
 109             return -cls._fromast(node.operand)
 110         elif isinstance(node, ast.BinOp):
 111             left = cls._fromast(node.left)
 112             right = cls._fromast(node.right)
 113             if isinstance(node.op, ast.Add):
 114                 return left + right
 115             elif isinstance(node.op, ast.Sub):
 116                 return left - right
 117             elif isinstance(node.op, ast.Mult):
 118                 return left * right
 119             elif isinstance(node.op, ast.Div):
 120                 return left / right
 121         raise SyntaxError('invalid syntax')
 122
 123     @classmethod
 124     def fromstring(cls, string):
 125         string = re.sub(r'(\d+|\))\s*([^\W\d_]\w*|\()', r'\1*\2', string)
 126         tree = ast.parse(string, 'eval')
 127         return cls._fromast(tree)
 128
 129     @property
 130     def symbols(self):
 131         return self._symbols
 132
 133     @property
 134     def dimension(self):
 135         return self._dimension
 136
 137     def coefficient(self, symbol):
 138         if isinstance(symbol, Symbol):
 139             symbol = str(symbol)
 140         elif not isinstance(symbol, str):
 141             raise TypeError('symbol must be a string or a Symbol instance')
 142         try:
 143             return self._coefficients[symbol]
 144         except KeyError:
 145             return 0
 146
 147     __getitem__ = coefficient
 148
 149     def coefficients(self):
 150         for symbol in self.symbols:
 151             yield symbol, self.coefficient(symbol)
 152
 153     @property
 154     def constant(self):
 155         return self._constant
 156
 157     def isconstant(self):
 158         return False
 159
 160     def values(self):
 161         for symbol in self.symbols:
 162             yield self.coefficient(symbol)
 163         yield self.constant
 164
 165     def issymbol(self):
 166         return False
 167
 168     def __bool__(self):
 169         return True
 170
 171     def __pos__(self):
 172         return self
 173
 174     def __neg__(self):
 175         return self * -1
 176
 177     @_polymorphic_method
 178     def __add__(self, other):
 179         coefficients = dict(self.coefficients())
 180         for symbol, coefficient in other.coefficients():
 181             if symbol in coefficients:
 182                 coefficients[symbol] += coefficient
 183             else:
 184                 coefficients[symbol] = coefficient
 185         constant = self.constant + other.constant
 186         return Expression(coefficients, constant)
 187
 188     __radd__ = __add__
 189
 190     @_polymorphic_method
 191     def __sub__(self, other):
 192         coefficients = dict(self.coefficients())
 193         for symbol, coefficient in other.coefficients():
 194             if symbol in coefficients:
 195                 coefficients[symbol] -= coefficient
 196             else:
 197                 coefficients[symbol] = -coefficient
 198         constant = self.constant - other.constant
 199         return Expression(coefficients, constant)
 200
 201     def __rsub__(self, other):
 202         return -(self - other)
 203
 204     @_polymorphic_method
 205     def __mul__(self, other):
 206         if other.isconstant():
 207             coefficients = dict(self.coefficients())
 208             for symbol in coefficients:
 209                 coefficients[symbol] *= other.constant
 210             constant = self.constant * other.constant
 211             return Expression(coefficients, constant)
 212         if isinstance(other, Expression) and not self.isconstant():
 213             raise ValueError('non-linear expression: '
 214                     '{} * {}'.format(self._parenstr(), other._parenstr()))
 215         return NotImplemented
 216
 217     __rmul__ = __mul__
 218
 219     @_polymorphic_method
 220     def __truediv__(self, other):
 221         if other.isconstant():
 222             coefficients = dict(self.coefficients())
 223             for symbol in coefficients:
 224                 coefficients[symbol] = \
 225                         Fraction(coefficients[symbol], other.constant)
 226             constant = Fraction(self.constant, other.constant)
 227             return Expression(coefficients, constant)
 228         if isinstance(other, Expression):
 229             raise ValueError('non-linear expression: '
 230                 '{} / {}'.format(self._parenstr(), other._parenstr()))
 231         return NotImplemented
 232
 233     def __rtruediv__(self, other):
 234         if isinstance(other, self):
 235             if self.isconstant():
 236                 constant = Fraction(other, self.constant)
 237                 return Expression(constant=constant)
 238             else:
 239                 raise ValueError('non-linear expression: '
 240                         '{} / {}'.format(other._parenstr(), self._parenstr()))
 241         return NotImplemented
 242
 243     def __str__(self):
 244         string = ''
 245         i = 0
 246         for symbol in self.symbols:
 247             coefficient = self.coefficient(symbol)
 248             if coefficient == 1:
 249                 if i == 0:
 250                     string += symbol
 251                 else:
 252                     string += ' + {}'.format(symbol)
 253             elif coefficient == -1:
 254                 if i == 0:
 255                     string += '-{}'.format(symbol)
 256                 else:
 257                     string += ' - {}'.format(symbol)
 258             else:
 259                 if i == 0:
 260                     string += '{}*{}'.format(coefficient, symbol)
 261                 elif coefficient > 0:
 262                     string += ' + {}*{}'.format(coefficient, symbol)
 263                 else:
 264                     assert coefficient < 0
 265                     coefficient *= -1
 266                     string += ' - {}*{}'.format(coefficient, symbol)
 267             i += 1
 268         constant = self.constant
 269         if constant != 0 and i == 0:
 270             string += '{}'.format(constant)
 271         elif constant > 0:
 272             string += ' + {}'.format(constant)
 273         elif constant < 0:
 274             constant *= -1
 275             string += ' - {}'.format(constant)
 276         if string == '':
 277             string = '0'
 278         return string
 279
 280     def _parenstr(self, always=False):
 281         string = str(self)
 282         if not always and (self.isconstant() or self.issymbol()):
 283             return string
 284         else:
 285             return '({})'.format(string)
 286
 287     def __repr__(self):
 288         return '{}({!r})'.format(self.__class__.__name__, str(self))
 289
 290     @_polymorphic_method
 291     def __eq__(self, other):
 292         # "normal" equality
 293         # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs
 294         return isinstance(other, Expression) and \
 295                 self._coefficients == other._coefficients and \
 296                 self.constant == other.constant
 297
 298     def __hash__(self):
 299         return hash((tuple(sorted(self._coefficients.items())), self._constant))
 300
 301     def _toint(self):
 302         lcm = functools.reduce(lambda a, b: a*b // gcd(a, b),
 303                 [value.denominator for value in self.values()])
 304         return self * lcm
 305
 306     @_polymorphic_method
 307     def _eq(self, other):
 308         return Polyhedron(equalities=[(self - other)._toint()])
 309
 310     @_polymorphic_method
 311     def __le__(self, other):
 312         return Polyhedron(inequalities=[(other - self)._toint()])
 313
 314     @_polymorphic_method
 315     def __lt__(self, other):
 316         return Polyhedron(inequalities=[(other - self)._toint() - 1])
 317
 318     @_polymorphic_method
 319     def __ge__(self, other):
 320         return Polyhedron(inequalities=[(self - other)._toint()])
 321
 322     @_polymorphic_method
 323     def __gt__(self, other):
 324         return Polyhedron(inequalities=[(self - other)._toint() - 1])
 325
 326     @classmethod
 327     def fromsympy(cls, expr):
 328         import sympy
 329         coefficients = {}
 330         constant = 0
 331         for symbol, coefficient in expr.as_coefficients_dict().items():
 332             coefficient = Fraction(coefficient.p, coefficient.q)
 333             if symbol == sympy.S.One:
 334                 constant = coefficient
 335             elif isinstance(symbol, sympy.Symbol):
 336                 symbol = symbol.name
 337                 coefficients[symbol] = coefficient
 338             else:
 339                 raise ValueError('non-linear expression: {!r}'.format(expr))
 340         return cls(coefficients, constant)
 341
 342     def tosympy(self):
 343         import sympy
 344         expr = 0
 345         for symbol, coefficient in self.coefficients():
 346             term = coefficient * sympy.Symbol(symbol)
 347             expr += term
 348         expr += self.constant
 349         return expr
 350
 351
 352 class Constant(Expression):
 353
 354     def __new__(cls, numerator=0, denominator=None):
 355         self = object().__new__(cls)
 356         if denominator is None:
 357             if isinstance(numerator, numbers.Rational):
 358                 self._constant = numerator
 359             elif isinstance(numerator, Constant):
 360                 self._constant = numerator.constant
 361             else:
 362                 raise TypeError('constant must be a rational number or a Constant instance')
 363         else:
 364             self._constant = Fraction(numerator, denominator)
 365         self._coefficients = {}
 366         self._symbols = ()
 367         self._dimension = 0
 368         return self
 369
 370     def isconstant(self):
 371         return True
 372
 373     def __bool__(self):
 374         return bool(self.constant)
 375
 376     def __repr__(self):
 377         if self.constant.denominator == 1:
 378             return '{}({!r})'.format(self.__class__.__name__, self.constant)
 379         else:
 380             return '{}({!r}, {!r})'.format(self.__class__.__name__,
 381                 self.constant.numerator, self.constant.denominator)
 382
 383     @classmethod
 384     def fromsympy(cls, expr):
 385         import sympy
 386         if isinstance(expr, sympy.Rational):
 387             return cls(expr.p, expr.q)
 388         elif isinstance(expr, numbers.Rational):
 389             return cls(expr)
 390         else:
 391             raise TypeError('expr must be a sympy.Rational instance')
 392
 393
 394 class Symbol(Expression):
 395
 396     __slots__ = Expression.__slots__ + (
 397         '_name',
 398     )
 399
 400     def __new__(cls, name):
 401         if isinstance(name, Symbol):
 402             name = name.name
 403         elif not isinstance(name, str):
 404             raise TypeError('name must be a string or a Symbol instance')
 405         self = object().__new__(cls)
 406         self._coefficients = {name: 1}
 407         self._constant = 0
 408         self._symbols = tuple(name)
 409         self._name = name
 410         self._dimension = 1
 411         return self
 412
 413     @property
 414     def name(self):
 415         return self._name
 416
 417     def issymbol(self):
 418         return True
 419
 420     def __repr__(self):
 421         return '{}({!r})'.format(self.__class__.__name__, self._name)
 422
 423     @classmethod
 424     def fromsympy(cls, expr):
 425         import sympy
 426         if isinstance(expr, sympy.Symbol):
 427             return cls(expr.name)
 428         else:
 429             raise TypeError('expr must be a sympy.Symbol instance')
 430
 431
 432 def symbols(names):
 433     if isinstance(names, str):
 434         names = names.replace(',', ' ').split()
 435     return (Symbol(name) for name in names)
 436
 437
 438 @_polymorphic_operator
 439 def eq(a, b):
 440     return a.__eq__(b)
 441
 442 @_polymorphic_operator
 443 def le(a, b):
 444     return a.__le__(b)
 445
 446 @_polymorphic_operator
 447 def lt(a, b):
 448     return a.__lt__(b)
 449
 450 @_polymorphic_operator
 451 def ge(a, b):
 452     return a.__ge__(b)
 453
 454 @_polymorphic_operator
 455 def gt(a, b):
 456     return a.__gt__(b)
 457
 458
 459 class Polyhedron:
 460     """
 461     This class implements polyhedrons.
 462     """
 463
 464     __slots__ = (
 465         '_equalities',
 466         '_inequalities',
 467         '_constraints',
 468         '_symbols',
 469     )
 470
 471     def __new__(cls, equalities=None, inequalities=None):
 472         if isinstance(equalities, str):
 473             if inequalities is not None:
 474                 raise TypeError('too many arguments')
 475             return cls.fromstring(equalities)
 476         self = super().__new__(cls)
 477         self._equalities = []
 478         if equalities is not None:
 479             for constraint in equalities:
 480                 for value in constraint.values():
 481                     if value.denominator != 1:
 482                         raise TypeError('non-integer constraint: '
 483                                 '{} == 0'.format(constraint))
 484                 self._equalities.append(constraint)
 485         self._equalities = tuple(self._equalities)
 486         self._inequalities = []
 487         if inequalities is not None:
 488             for constraint in inequalities:
 489                 for value in constraint.values():
 490                     if value.denominator != 1:
 491                         raise TypeError('non-integer constraint: '
 492                                 '{} <= 0'.format(constraint))
 493                 self._inequalities.append(constraint)
 494         self._inequalities = tuple(self._inequalities)
 495         self._constraints = self._equalities + self._inequalities
 496         self._symbols = set()
 497         for constraint in self._constraints:
 498             self.symbols.update(constraint.symbols)
 499         self._symbols = tuple(sorted(self._symbols))
 500         return self
 501
 502     @classmethod
 503     def _fromast(cls, node):
 504         if isinstance(node, ast.Module) and len(node.body) == 1:
 505             return cls._fromast(node.body[0])
 506         elif isinstance(node, ast.Expr):
 507             return cls._fromast(node.value)
 508         elif isinstance(node, ast.BinOp) and isinstance(node.op, ast.BitAnd):
 509             equalities1, inequalities1 = cls._fromast(node.left)
 510             equalities2, inequalities2 = cls._fromast(node.right)
 511             equalities = equalities1 + equalities2
 512             inequalities = inequalities1 + inequalities2
 513             return equalities, inequalities
 514         elif isinstance(node, ast.Compare):
 515             equalities = []
 516             inequalities = []
 517             left = Expression._fromast(node.left)
 518             for i in range(len(node.ops)):
 519                 op = node.ops[i]
 520                 right = Expression._fromast(node.comparators[i])
 521                 if isinstance(op, ast.Lt):
 522                     inequalities.append(right - left - 1)
 523                 elif isinstance(op, ast.LtE):
 524                     inequalities.append(right - left)
 525                 elif isinstance(op, ast.Eq):
 526                     equalities.append(left - right)
 527                 elif isinstance(op, ast.GtE):
 528                     inequalities.append(left - right)
 529                 elif isinstance(op, ast.Gt):
 530                     inequalities.append(left - right - 1)
 531                 else:
 532                     break
 533                 left = right
 534             else:
 535                 return equalities, inequalities
 536         raise SyntaxError('invalid syntax')
 537
 538     @classmethod
 539     def fromstring(cls, string):
 540         string = string.strip()
 541         string = re.sub(r'^\{\s*|\s*\}$', '', string)
 542         string = re.sub(r'([^<=>])=([^<=>])', r'\1==\2', string)
 543         string = re.sub(r'(\d+|\))\s*([^\W\d_]\w*|\()', r'\1*\2', string)
 544         tokens = re.split(r',|;|and|&&|/\\|∧', string, flags=re.I)
 545         tokens = ['({})'.format(token) for token in tokens]
 546         string = ' & '.join(tokens)
 547         tree = ast.parse(string, 'eval')
 548         equalities, inequalities = cls._fromast(tree)
 549         return cls(equalities, inequalities)
 550
 551     @property
 552     def equalities(self):
 553         return self._equalities
 554
 555     @property
 556     def inequalities(self):
 557         return self._inequalities
 558
 559     @property
 560     def constraints(self):
 561         return self._constraints
 562
 563     @property
 564     def symbols(self):
 565         return self._symbols
 566
 567     @property
 568     def dimension(self):
 569         return len(self.symbols)
 570
 571     def __bool__(self):
 572         return not self.is_empty()
 573
 574     def __contains__(self, value):
 575         # is the value in the polyhedron?
 576         raise NotImplementedError
 577
 578     def __eq__(self, other):
 579         # works correctly when symbols is not passed
 580         # should be equal if values are the same even if symbols are different
 581         bset = self._toisl()
 582         other = other._toisl()
 583         return bool(libisl.isl_basic_set_plain_is_equal(bset, other))
 584
 585     def isempty(self):
 586         bset = self._toisl()
 587         return bool(libisl.isl_basic_set_is_empty(bset))
 588
 589     def isuniverse(self):
 590         bset = self._toisl()
 591         return bool(libisl.isl_basic_set_is_universe(bset))
 592
 593     def isdisjoint(self, other):
 594         # return true if the polyhedron has no elements in common with other
 595         #symbols = self._symbolunion(other)
 596         bset = self._toisl()
 597         other = other._toisl()
 598         return bool(libisl.isl_set_is_disjoint(bset, other))
 599
 600     def issubset(self, other):
 601         # check if self(bset) is a subset of other
 602         symbols = self._symbolunion(other)
 603         bset = self._toisl(symbols)
 604         other = other._toisl(symbols)
 605         return bool(libisl.isl_set_is_strict_subset(other, bset))
 606
 607     def __le__(self, other):
 608         return self.issubset(other)
 609
 610     def __lt__(self, other):
 611         symbols = self._symbolunion(other)
 612         bset = self._toisl(symbols)
 613         other = other._toisl(symbols)
 614         return bool(libisl.isl_set_is_strict_subset(other, bset))
 615
 616     def issuperset(self, other):
 617         # test whether every element in other is in the polyhedron
 618         raise NotImplementedError
 619
 620     def __ge__(self, other):
 621         return self.issuperset(other)
 622
 623     def __gt__(self, other):
 624         symbols = self._symbolunion(other)
 625         bset = self._toisl(symbols)
 626         other = other._toisl(symbols)
 627         bool(libisl.isl_set_is_strict_subset(other, bset))
 628         raise NotImplementedError
 629
 630     def union(self, *others):
 631         # return a new polyhedron with elements from the polyhedron and all
 632         # others (convex union)
 633         raise NotImplementedError
 634
 635     def __or__(self, other):
 636         return self.union(other)
 637
 638     def intersection(self, *others):
 639         # return a new polyhedron with elements common to the polyhedron and all
 640         # others
 641         # a poor man's implementation could be:
 642         # equalities = list(self.equalities)
 643         # inequalities = list(self.inequalities)
 644         # for other in others:
 645         #     equalities.extend(other.equalities)
 646         #     inequalities.extend(other.inequalities)
 647         # return self.__class__(equalities, inequalities)
 648         raise NotImplementedError
 649
 650     def __and__(self, other):
 651         return self.intersection(other)
 652
 653     def difference(self, other):
 654         # return a new polyhedron with elements in the polyhedron that are not in the other
 655         symbols = self._symbolunion(other)
 656         bset = self._toisl(symbols)
 657         other = other._toisl(symbols)
 658         difference = libisl.isl_set_subtract(bset, other)
 659         return difference
 660
 661     def __sub__(self, other):
 662         return self.difference(other)
 663
 664     def __str__(self):
 665         constraints = []
 666         for constraint in self.equalities:
 667             constraints.append('{} == 0'.format(constraint))
 668         for constraint in self.inequalities:
 669             constraints.append('{} >= 0'.format(constraint))
 670         return '{}'.format(', '.join(constraints))
 671
 672     def __repr__(self):
 673         if self.isempty():
 674             return 'Empty'
 675         elif self.isuniverse():
 676             return 'Universe'
 677         else:
 678             return '{}({!r})'.format(self.__class__.__name__, str(self))
 679
 680     @classmethod
 681     def _fromsympy(cls, expr):
 682         import sympy
 683         equalities = []
 684         inequalities = []
 685         if expr.func == sympy.And:
 686             for arg in expr.args:
 687                 arg_eqs, arg_ins = cls._fromsympy(arg)
 688                 equalities.extend(arg_eqs)
 689                 inequalities.extend(arg_ins)
 690         elif expr.func == sympy.Eq:
 691             expr = Expression.fromsympy(expr.args[0] - expr.args[1])
 692             equalities.append(expr)
 693         else:
 694             if expr.func == sympy.Lt:
 695                 expr = Expression.fromsympy(expr.args[1] - expr.args[0] - 1)
 696             elif expr.func == sympy.Le:
 697                 expr = Expression.fromsympy(expr.args[1] - expr.args[0])
 698             elif expr.func == sympy.Ge:
 699                 expr = Expression.fromsympy(expr.args[0] - expr.args[1])
 700             elif expr.func == sympy.Gt:
 701                 expr = Expression.fromsympy(expr.args[0] - expr.args[1] - 1)
 702             else:
 703                 raise ValueError('non-polyhedral expression: {!r}'.format(expr))
 704             inequalities.append(expr)
 705         return equalities, inequalities
 706
 707     @classmethod
 708     def fromsympy(cls, expr):
 709         import sympy
 710         equalities, inequalities = cls._fromsympy(expr)
 711         return cls(equalities, inequalities)
 712
 713     def tosympy(self):
 714         import sympy
 715         constraints = []
 716         for equality in self.equalities:
 717             constraints.append(sympy.Eq(equality.tosympy(), 0))
 718         for inequality in self.inequalities:
 719             constraints.append(sympy.Ge(inequality.tosympy(), 0))
 720         return sympy.And(*constraints)
 721
 722     def _symbolunion(self, *others):
 723         symbols = set(self.symbols)
 724         for other in others:
 725             symbols.update(other.symbols)
 726         return sorted(symbols)
 727
 728     def _toisl(self, symbols=None):
 729         if symbols is None:
 730             symbols = self.symbols
 731         dimension = len(symbols)
 732         space = libisl.isl_space_set_alloc(_main_ctx, 0, dimension)
 733         bset = libisl.isl_basic_set_universe(libisl.isl_space_copy(space))
 734         ls = libisl.isl_local_space_from_space(space)
 735         for equality in self.equalities:
 736             ceq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(ls))
 737             for symbol, coefficient in equality.coefficients():
 738                 val = str(coefficient).encode()
 739                 val = libisl.isl_val_read_from_str(_main_ctx, val)
 740                 dim = symbols.index(symbol)
 741                 ceq = libisl.isl_constraint_set_coefficient_val(ceq, libisl.isl_dim_set, dim, val)
 742             if equality.constant != 0:
 743                 val = str(equality.constant).encode()
 744                 val = libisl.isl_val_read_from_str(_main_ctx, val)
 745                 ceq = libisl.isl_constraint_set_constant_val(ceq, val)
 746             bset = libisl.isl_basic_set_add_constraint(bset, ceq)
 747         for inequality in self.inequalities:
 748             cin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(ls))
 749             for symbol, coefficient in inequality.coefficients():
 750                 val = str(coefficient).encode()
 751                 val = libisl.isl_val_read_from_str(_main_ctx, val)
 752                 dim = symbols.index(symbol)
 753                 cin = libisl.isl_constraint_set_coefficient_val(cin, libisl.isl_dim_set, dim, val)
 754             if inequality.constant != 0:
 755                 val = str(inequality.constant).encode()
 756                 val = libisl.isl_val_read_from_str(_main_ctx, val)
 757                 cin = libisl.isl_constraint_set_constant_val(cin, val)
 758             bset = libisl.isl_basic_set_add_constraint(bset, cin)
 759         bset = isl.BasicSet(bset)
 760         return bset
 761
 762     @classmethod
 763     def _fromisl(cls, bset, symbols):
 764         raise NotImplementedError
 765         equalities = ...
 766         inequalities = ...
 767         return cls(equalities, inequalities)
 768         '''takes basic set  in isl form and puts back into python version of polyhedron
 769         isl example code gives isl form as:
 770             "{[i] : exists (a : i = 2a and i >= 10 and i <= 42)}")
 771             our printer is giving form as:
 772             { [i0, i1] : 2i1 >= -2 - i0 } '''
 773
 774 Empty = eq(0,1)
 775
 776 Universe = Polyhedron()
 777
 778
 779 if __name__ == '__main__':
 780     #p = Polyhedron('2a + 2b + 1 == 0') # empty
 781     p = Polyhedron('3x + 2y + 3 == 0, y == 0') # not empty
 782     ip = p._toisl()
 783     print(ip)
 784     print(ip.constraints())