X-Git-Url: https://svn.cri.ensmp.fr/git/linpy.git/blobdiff_plain/844f76f670a227d335e9bc539e1a61be7161452a..5a4b72c59f689a3eb67303c60a5d76a99d4b097c:/pypol/linear.py diff --git a/pypol/linear.py b/pypol/linear.py index 6550e92..b69836d 100644 --- a/pypol/linear.py +++ b/pypol/linear.py @@ -1,60 +1,144 @@ - +import ast import functools import numbers +import re from fractions import Fraction, gcd +from . import isl +from .isl import libisl + __all__ = [ - 'Expression', - 'constant', 'symbol', 'symbols', + 'Expression', 'Constant', 'Symbol', 'symbols', 'eq', 'le', 'lt', 'ge', 'gt', 'Polyhedron', - 'empty', 'universe' + 'Empty', 'Universe' ] +def _polymorphic_method(func): + @functools.wraps(func) + def wrapper(a, b): + if isinstance(b, Expression): + return func(a, b) + if isinstance(b, numbers.Rational): + b = Constant(b) + return func(a, b) + return NotImplemented + return wrapper + +def _polymorphic_operator(func): + # A polymorphic operator should call a polymorphic method, hence we just + # have to test the left operand. + @functools.wraps(func) + def wrapper(a, b): + if isinstance(a, numbers.Rational): + a = Constant(a) + return func(a, b) + elif isinstance(a, Expression): + return func(a, b) + raise TypeError('arguments must be linear expressions') + return wrapper + + +_main_ctx = isl.Context() + + class Expression: """ This class implements linear expressions. """ + __slots__ = ( + '_coefficients', + '_constant', + '_symbols', + '_dimension', + ) + def __new__(cls, coefficients=None, constant=0): if isinstance(coefficients, str): if constant: raise TypeError('too many arguments') return cls.fromstring(coefficients) - self = super().__new__(cls) - self._coefficients = {} if isinstance(coefficients, dict): coefficients = coefficients.items() - if coefficients is not None: - for symbol, coefficient in coefficients: - if isinstance(symbol, Expression) and symbol.issymbol(): - symbol = str(symbol) - elif not isinstance(symbol, str): - raise TypeError('symbols must be strings') - if not isinstance(coefficient, numbers.Rational): - raise TypeError('coefficients must be rational numbers') - if coefficient != 0: - self._coefficients[symbol] = coefficient + if coefficients is None: + return Constant(constant) + coefficients = [(symbol, coefficient) + for symbol, coefficient in coefficients if coefficient != 0] + if len(coefficients) == 0: + return Constant(constant) + elif len(coefficients) == 1 and constant == 0: + symbol, coefficient = coefficients[0] + if coefficient == 1: + return Symbol(symbol) + self = object().__new__(cls) + self._coefficients = {} + for symbol, coefficient in coefficients: + if isinstance(symbol, Symbol): + symbol = symbol.name + elif not isinstance(symbol, str): + raise TypeError('symbols must be strings or Symbol instances') + if isinstance(coefficient, Constant): + coefficient = coefficient.constant + if not isinstance(coefficient, numbers.Rational): + raise TypeError('coefficients must be rational numbers or Constant instances') + self._coefficients[symbol] = coefficient + if isinstance(constant, Constant): + constant = constant.constant if not isinstance(constant, numbers.Rational): - raise TypeError('constant must be a rational number') + raise TypeError('constant must be a rational number or a Constant instance') self._constant = constant + self._symbols = tuple(sorted(self._coefficients)) + self._dimension = len(self._symbols) return self + @classmethod + def _fromast(cls, node): + if isinstance(node, ast.Module) and len(node.body) == 1: + return cls._fromast(node.body[0]) + elif isinstance(node, ast.Expr): + return cls._fromast(node.value) + elif isinstance(node, ast.Name): + return Symbol(node.id) + elif isinstance(node, ast.Num): + return Constant(node.n) + elif isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub): + return -cls._fromast(node.operand) + elif isinstance(node, ast.BinOp): + left = cls._fromast(node.left) + right = cls._fromast(node.right) + if isinstance(node.op, ast.Add): + return left + right + elif isinstance(node.op, ast.Sub): + return left - right + elif isinstance(node.op, ast.Mult): + return left * right + elif isinstance(node.op, ast.Div): + return left / right + raise SyntaxError('invalid syntax') + + @classmethod + def fromstring(cls, string): + string = re.sub(r'(\d+|\))\s*([^\W\d_]\w*|\()', r'\1*\2', string) + tree = ast.parse(string, 'eval') + return cls._fromast(tree) + + @property def symbols(self): - yield from sorted(self._coefficients) + return self._symbols @property def dimension(self): - return len(list(self.symbols())) + return self._dimension def coefficient(self, symbol): - if isinstance(symbol, Expression) and symbol.issymbol(): + if isinstance(symbol, Symbol): symbol = str(symbol) elif not isinstance(symbol, str): - raise TypeError('symbol must be a string') + raise TypeError('symbol must be a string or a Symbol instance') try: return self._coefficients[symbol] except KeyError: @@ -63,7 +147,7 @@ class Expression: __getitem__ = coefficient def coefficients(self): - for symbol in self.symbols(): + for symbol in self.symbols: yield symbol, self.coefficient(symbol) @property @@ -71,24 +155,18 @@ class Expression: return self._constant def isconstant(self): - return len(self._coefficients) == 0 + return False def values(self): - for symbol in self.symbols(): + for symbol in self.symbols: yield self.coefficient(symbol) yield self.constant - def symbol(self): - if not self.issymbol(): - raise ValueError('not a symbol: {}'.format(self)) - for symbol in self.symbols(): - return symbol - def issymbol(self): - return len(self._coefficients) == 1 and self._constant == 0 + return False def __bool__(self): - return (not self.isconstant()) or bool(self.constant) + return True def __pos__(self): return self @@ -96,18 +174,7 @@ class Expression: def __neg__(self): return self * -1 - def _polymorphic(func): - @functools.wraps(func) - def wrapper(self, other): - if isinstance(other, Expression): - return func(self, other) - if isinstance(other, numbers.Rational): - other = Expression(constant=other) - return func(self, other) - return NotImplemented - return wrapper - - @_polymorphic + @_polymorphic_method def __add__(self, other): coefficients = dict(self.coefficients()) for symbol, coefficient in other.coefficients(): @@ -120,7 +187,7 @@ class Expression: __radd__ = __add__ - @_polymorphic + @_polymorphic_method def __sub__(self, other): coefficients = dict(self.coefficients()) for symbol, coefficient in other.coefficients(): @@ -131,9 +198,10 @@ class Expression: constant = self.constant - other.constant return Expression(coefficients, constant) - __rsub__ = __sub__ + def __rsub__(self, other): + return -(self - other) - @_polymorphic + @_polymorphic_method def __mul__(self, other): if other.isconstant(): coefficients = dict(self.coefficients()) @@ -148,7 +216,7 @@ class Expression: __rmul__ = __mul__ - @_polymorphic + @_polymorphic_method def __truediv__(self, other): if other.isconstant(): coefficients = dict(self.coefficients()) @@ -163,7 +231,7 @@ class Expression: return NotImplemented def __rtruediv__(self, other): - if isinstance(other, Rational): + if isinstance(other, self): if self.isconstant(): constant = Fraction(other, self.constant) return Expression(constant=constant) @@ -174,10 +242,9 @@ class Expression: def __str__(self): string = '' - symbols = sorted(self.symbols()) i = 0 - for symbol in symbols: - coefficient = self[symbol] + for symbol in self.symbols: + coefficient = self.coefficient(symbol) if coefficient == 1: if i == 0: string += symbol @@ -226,11 +293,7 @@ class Expression: string += '}}, {!r})'.format(self.constant) return string - @classmethod - def fromstring(cls, string): - raise NotImplementedError - - @_polymorphic + @_polymorphic_method def __eq__(self, other): # "normal" equality # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs @@ -239,79 +302,164 @@ class Expression: self.constant == other.constant def __hash__(self): - return hash((self._coefficients, self._constant)) + return hash((tuple(sorted(self._coefficients.items())), self._constant)) - def _canonify(self): + def _toint(self): lcm = functools.reduce(lambda a, b: a*b // gcd(a, b), [value.denominator for value in self.values()]) return self * lcm - @_polymorphic + @_polymorphic_method def _eq(self, other): - return Polyhedron(equalities=[(self - other)._canonify()]) + return Polyhedron(equalities=[(self - other)._toint()]) - @_polymorphic + @_polymorphic_method def __le__(self, other): - return Polyhedron(inequalities=[(self - other)._canonify()]) + return Polyhedron(inequalities=[(other - self)._toint()]) - @_polymorphic + @_polymorphic_method def __lt__(self, other): - return Polyhedron(inequalities=[(self - other)._canonify() + 1]) + return Polyhedron(inequalities=[(other - self)._toint() - 1]) - @_polymorphic + @_polymorphic_method def __ge__(self, other): - return Polyhedron(inequalities=[(other - self)._canonify()]) + return Polyhedron(inequalities=[(self - other)._toint()]) - @_polymorphic + @_polymorphic_method def __gt__(self, other): - return Polyhedron(inequalities=[(other - self)._canonify() + 1]) + return Polyhedron(inequalities=[(self - other)._toint() - 1]) + + @classmethod + def fromsympy(cls, expr): + import sympy + coefficients = {} + constant = 0 + for symbol, coefficient in expr.as_coefficients_dict().items(): + coefficient = Fraction(coefficient.p, coefficient.q) + if symbol == sympy.S.One: + constant = coefficient + elif isinstance(symbol, sympy.Symbol): + symbol = symbol.name + coefficients[symbol] = coefficient + else: + raise ValueError('non-linear expression: {!r}'.format(expr)) + return cls(coefficients, constant) + + def tosympy(self): + import sympy + expr = 0 + for symbol, coefficient in self.coefficients(): + term = coefficient * sympy.Symbol(symbol) + expr += term + expr += self.constant + return expr + + +class Constant(Expression): + + def __new__(cls, numerator=0, denominator=None): + self = object().__new__(cls) + if denominator is None: + if isinstance(numerator, numbers.Rational): + self._constant = numerator + elif isinstance(numerator, Constant): + self._constant = numerator.constant + else: + raise TypeError('constant must be a rational number or a Constant instance') + else: + self._constant = Fraction(numerator, denominator) + self._coefficients = {} + self._symbols = () + self._dimension = 0 + return self + + def isconstant(self): + return True + + def __bool__(self): + return bool(self.constant) + + def __repr__(self): + if self.constant.denominator == 1: + return '{}({!r})'.format(self.__class__.__name__, self.constant) + else: + return '{}({!r}, {!r})'.format(self.__class__.__name__, + self.constant.numerator, self.constant.denominator) + @classmethod + def fromsympy(cls, expr): + import sympy + if isinstance(expr, sympy.Rational): + return cls(expr.p, expr.q) + elif isinstance(expr, numbers.Rational): + return cls(expr) + else: + raise TypeError('expr must be a sympy.Rational instance') + + +class Symbol(Expression): + + __slots__ = Expression.__slots__ + ( + '_name', + ) + + def __new__(cls, name): + if isinstance(name, Symbol): + name = name.name + elif not isinstance(name, str): + raise TypeError('name must be a string or a Symbol instance') + self = object().__new__(cls) + self._coefficients = {name: 1} + self._constant = 0 + self._symbols = tuple(name) + self._name = name + self._dimension = 1 + return self -def constant(numerator=0, denominator=None): - return Expression(constant=Fraction(numerator, denominator)) + @property + def name(self): + return self._name + + def issymbol(self): + return True + + def __repr__(self): + return '{}({!r})'.format(self.__class__.__name__, self._name) + + @classmethod + def fromsympy(cls, expr): + import sympy + if isinstance(expr, sympy.Symbol): + return cls(expr.name) + else: + raise TypeError('expr must be a sympy.Symbol instance') -def symbol(name): - if not isinstance(name, str): - raise TypeError('name must be a string') - return Expression(coefficients={name: 1}) def symbols(names): if isinstance(names, str): names = names.replace(',', ' ').split() - return (symbol(name) for name in names) - + return (Symbol(name) for name in names) -def _operator(func): - @functools.wraps(func) - def wrapper(a, b): - if isinstance(a, numbers.Rational): - a = constant(a) - if isinstance(b, numbers.Rational): - b = constant(b) - if isinstance(a, Expression) and isinstance(b, Expression): - return func(a, b) - raise TypeError('arguments must be linear expressions') - return wrapper -@_operator +@_polymorphic_operator def eq(a, b): - return a._eq(b) + return a.__eq__(b) -@_operator +@_polymorphic_operator def le(a, b): - return a <= b + return a.__le__(b) -@_operator +@_polymorphic_operator def lt(a, b): - return a < b + return a.__lt__(b) -@_operator +@_polymorphic_operator def ge(a, b): - return a >= b + return a.__ge__(b) -@_operator +@_polymorphic_operator def gt(a, b): - return a > b + return a.__gt__(b) class Polyhedron: @@ -319,6 +467,13 @@ class Polyhedron: This class implements polyhedrons. """ + __slots__ = ( + '_equalities', + '_inequalities', + '_constraints', + '_symbols', + ) + def __new__(cls, equalities=None, inequalities=None): if isinstance(equalities, str): if inequalities is not None: @@ -333,6 +488,7 @@ class Polyhedron: raise TypeError('non-integer constraint: ' '{} == 0'.format(constraint)) self._equalities.append(constraint) + self._equalities = tuple(self._equalities) self._inequalities = [] if inequalities is not None: for constraint in inequalities: @@ -341,59 +497,127 @@ class Polyhedron: raise TypeError('non-integer constraint: ' '{} <= 0'.format(constraint)) self._inequalities.append(constraint) + self._inequalities = tuple(self._inequalities) + self._constraints = self._equalities + self._inequalities + self._symbols = set() + for constraint in self._constraints: + self.symbols.update(constraint.symbols) + self._symbols = tuple(sorted(self._symbols)) return self + @classmethod + def _fromast(cls, node): + if isinstance(node, ast.Module) and len(node.body) == 1: + return cls._fromast(node.body[0]) + elif isinstance(node, ast.Expr): + return cls._fromast(node.value) + elif isinstance(node, ast.BinOp) and isinstance(node.op, ast.BitAnd): + equalities1, inequalities1 = cls._fromast(node.left) + equalities2, inequalities2 = cls._fromast(node.right) + equalities = equalities1 + equalities2 + inequalities = inequalities1 + inequalities2 + return equalities, inequalities + elif isinstance(node, ast.Compare): + equalities = [] + inequalities = [] + left = Expression._fromast(node.left) + for i in range(len(node.ops)): + op = node.ops[i] + right = Expression._fromast(node.comparators[i]) + if isinstance(op, ast.Lt): + inequalities.append(right - left - 1) + elif isinstance(op, ast.LtE): + inequalities.append(right - left) + elif isinstance(op, ast.Eq): + equalities.append(left - right) + elif isinstance(op, ast.GtE): + inequalities.append(left - right) + elif isinstance(op, ast.Gt): + inequalities.append(left - right - 1) + else: + break + left = right + else: + return equalities, inequalities + raise SyntaxError('invalid syntax') + + @classmethod + def fromstring(cls, string): + string = string.strip() + string = re.sub(r'^\{\s*|\s*\}$', '', string) + string = re.sub(r'([^<=>])=([^<=>])', r'\1==\2', string) + string = re.sub(r'(\d+|\))\s*([^\W\d_]\w*|\()', r'\1*\2', string) + tokens = re.split(r',|;|and|&&|/\\|∧', string, flags=re.I) + tokens = ['({})'.format(token) for token in tokens] + string = ' & '.join(tokens) + tree = ast.parse(string, 'eval') + equalities, inequalities = cls._fromast(tree) + return cls(equalities, inequalities) + @property def equalities(self): - yield from self._equalities + return self._equalities @property def inequalities(self): - yield from self._inequalities + return self._inequalities + @property def constraints(self): - yield from self.equalities - yield from self.inequalities + return self._constraints + @property def symbols(self): - s = set() - for constraint in self.constraints(): - s.update(constraint.symbols) - yield from sorted(s) + return self._symbols @property def dimension(self): - return len(self.symbols()) + return len(self.symbols) def __bool__(self): - # return false if the polyhedron is empty, true otherwise - raise NotImplementedError + return not self.is_empty() def __contains__(self, value): # is the value in the polyhedron? raise NotImplementedError def __eq__(self, other): - raise NotImplementedError + # works correctly when symbols is not passed + # should be equal if values are the same even if symbols are different + bset = self._toisl() + other = other._toisl() + return bool(libisl.isl_basic_set_plain_is_equal(bset, other)) def isempty(self): - return self == empty + bset = self._toisl() + return bool(libisl.isl_basic_set_is_empty(bset)) def isuniverse(self): - return self == universe + bset = self._toisl() + return bool(libisl.isl_basic_set_is_universe(bset)) def isdisjoint(self, other): # return true if the polyhedron has no elements in common with other - raise NotImplementedError + #symbols = self._symbolunion(other) + bset = self._toisl() + other = other._toisl() + return bool(libisl.isl_set_is_disjoint(bset, other)) def issubset(self, other): - raise NotImplementedError + # check if self(bset) is a subset of other + symbols = self._symbolunion(other) + bset = self._toisl(symbols) + other = other._toisl(symbols) + return bool(libisl.isl_set_is_strict_subset(other, bset)) def __le__(self, other): return self.issubset(other) def __lt__(self, other): - raise NotImplementedError + symbols = self._symbolunion(other) + bset = self._toisl(symbols) + other = other._toisl(symbols) + return bool(libisl.isl_set_is_strict_subset(other, bset)) def issuperset(self, other): # test whether every element in other is in the polyhedron @@ -403,6 +627,10 @@ class Polyhedron: return self.issuperset(other) def __gt__(self, other): + symbols = self._symbolunion(other) + bset = self._toisl(symbols) + other = other._toisl(symbols) + bool(libisl.isl_set_is_strict_subset(other, bset)) raise NotImplementedError def union(self, *others): @@ -428,10 +656,13 @@ class Polyhedron: def __and__(self, other): return self.intersection(other) - def difference(self, *others): - # return a new polyhedron with elements in the polyhedron that are not - # in the others - raise NotImplementedError + def difference(self, other): + # return a new polyhedron with elements in the polyhedron that are not in the other + symbols = self._symbolunion(other) + bset = self._toisl(symbols) + other = other._toisl(symbols) + difference = libisl.isl_set_subtract(bset, other) + return difference def __sub__(self, other): return self.difference(other) @@ -441,20 +672,80 @@ class Polyhedron: for constraint in self.equalities: constraints.append('{} == 0'.format(constraint)) for constraint in self.inequalities: - constraints.append('{} <= 0'.format(constraint)) + constraints.append('{} >= 0'.format(constraint)) return '{{{}}}'.format(', '.join(constraints)) def __repr__(self): - equalities = list(self.equalities) - inequalities = list(self.inequalities) - return '{}(equalities={!r}, inequalities={!r})' \ - ''.format(self.__class__.__name__, equalities, inequalities) + if self.isempty(): + return 'Empty' + elif self.isuniverse(): + return 'Universe' + else: + equalities = list(self.equalities) + inequalities = list(self.inequalities) + return '{}(equalities={!r}, inequalities={!r})' \ + ''.format(self.__class__.__name__, equalities, inequalities) + + def _symbolunion(self, *others): + symbols = set(self.symbols) + for other in others: + symbols.update(other.symbols) + return sorted(symbols) + + def _toisl(self, symbols=None): + if symbols is None: + symbols = self.symbols + dimension = len(symbols) + space = libisl.isl_space_set_alloc(_main_ctx, 0, dimension) + bset = libisl.isl_basic_set_universe(libisl.isl_space_copy(space)) + ls = libisl.isl_local_space_from_space(space) + for equality in self.equalities: + ceq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(ls)) + for symbol, coefficient in equality.coefficients(): + val = str(coefficient).encode() + val = libisl.isl_val_read_from_str(_main_ctx, val) + dim = symbols.index(symbol) + ceq = libisl.isl_constraint_set_coefficient_val(ceq, libisl.isl_dim_set, dim, val) + if equality.constant != 0: + val = str(equality.constant).encode() + val = libisl.isl_val_read_from_str(_main_ctx, val) + ceq = libisl.isl_constraint_set_constant_val(ceq, val) + bset = libisl.isl_basic_set_add_constraint(bset, ceq) + for inequality in self.inequalities: + cin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(ls)) + for symbol, coefficient in inequality.coefficients(): + val = str(coefficient).encode() + val = libisl.isl_val_read_from_str(_main_ctx, val) + dim = symbols.index(symbol) + cin = libisl.isl_constraint_set_coefficient_val(cin, libisl.isl_dim_set, dim, val) + if inequality.constant != 0: + val = str(inequality.constant).encode() + val = libisl.isl_val_read_from_str(_main_ctx, val) + cin = libisl.isl_constraint_set_constant_val(cin, val) + bset = libisl.isl_basic_set_add_constraint(bset, cin) + bset = isl.BasicSet(bset) + return bset @classmethod - def fromstring(cls, string): + def _fromisl(cls, bset, symbols): raise NotImplementedError - - -empty = le(1, 0) - -universe = Polyhedron() + equalities = ... + inequalities = ... + return cls(equalities, inequalities) + '''takes basic set in isl form and puts back into python version of polyhedron + isl example code gives isl form as: + "{[i] : exists (a : i = 2a and i >= 10 and i <= 42)}") + our printer is giving form as: + { [i0, i1] : 2i1 >= -2 - i0 } ''' + +Empty = eq(0,1) + +Universe = Polyhedron() + + +if __name__ == '__main__': + #p = Polyhedron('2a + 2b + 1 == 0') # empty + p = Polyhedron('3x + 2y + 3 == 0, y == 0') # not empty + ip = p._toisl() + print(ip) + print(ip.constraints())