-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',
- 'eq', 'le', 'lt', 'ge', 'gt',
- 'Polyhedron',
- '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)
- if isinstance(coefficients, dict):
- coefficients = coefficients.items()
- 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 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):
- return self._symbols
-
- @property
- def dimension(self):
- return self._dimension
-
- def coefficient(self, symbol):
- if isinstance(symbol, Symbol):
- symbol = str(symbol)
- elif not isinstance(symbol, str):
- raise TypeError('symbol must be a string or a Symbol instance')
- try:
- return self._coefficients[symbol]
- except KeyError:
- return 0
-
- __getitem__ = coefficient
-
- def coefficients(self):
- for symbol in self.symbols:
- yield symbol, self.coefficient(symbol)
-
- @property
- def constant(self):
- return self._constant
-
- def isconstant(self):
- return False
-
- def values(self):
- for symbol in self.symbols:
- yield self.coefficient(symbol)
- yield self.constant
-
- def issymbol(self):
- return False
-
- def __bool__(self):
- return True
-
- def __pos__(self):
- return self
-
- def __neg__(self):
- return self * -1
-
- @_polymorphic_method
- def __add__(self, other):
- coefficients = dict(self.coefficients())
- for symbol, coefficient in other.coefficients():
- if symbol in coefficients:
- coefficients[symbol] += coefficient
- else:
- coefficients[symbol] = coefficient
- constant = self.constant + other.constant
- return Expression(coefficients, constant)
-
- __radd__ = __add__
-
- @_polymorphic_method
- def __sub__(self, other):
- coefficients = dict(self.coefficients())
- for symbol, coefficient in other.coefficients():
- if symbol in coefficients:
- coefficients[symbol] -= coefficient
- else:
- coefficients[symbol] = -coefficient
- constant = self.constant - other.constant
- return Expression(coefficients, constant)
-
- def __rsub__(self, other):
- return -(self - other)
-
- @_polymorphic_method
- def __mul__(self, other):
- if other.isconstant():
- coefficients = dict(self.coefficients())
- for symbol in coefficients:
- coefficients[symbol] *= other.constant
- constant = self.constant * other.constant
- return Expression(coefficients, constant)
- if isinstance(other, Expression) and not self.isconstant():
- raise ValueError('non-linear expression: '
- '{} * {}'.format(self._parenstr(), other._parenstr()))
- return NotImplemented
-
- __rmul__ = __mul__
-
- @_polymorphic_method
- def __truediv__(self, other):
- if other.isconstant():
- coefficients = dict(self.coefficients())
- for symbol in coefficients:
- coefficients[symbol] = \
- Fraction(coefficients[symbol], other.constant)
- constant = Fraction(self.constant, other.constant)
- return Expression(coefficients, constant)
- if isinstance(other, Expression):
- raise ValueError('non-linear expression: '
- '{} / {}'.format(self._parenstr(), other._parenstr()))
- return NotImplemented
-
- def __rtruediv__(self, other):
- if isinstance(other, self):
- if self.isconstant():
- constant = Fraction(other, self.constant)
- return Expression(constant=constant)
- else:
- raise ValueError('non-linear expression: '
- '{} / {}'.format(other._parenstr(), self._parenstr()))
- return NotImplemented
-
- def __str__(self):
- string = ''
- i = 0
- for symbol in self.symbols:
- coefficient = self.coefficient(symbol)
- if coefficient == 1:
- if i == 0:
- string += symbol
- else:
- string += ' + {}'.format(symbol)
- elif coefficient == -1:
- if i == 0:
- string += '-{}'.format(symbol)
- else:
- string += ' - {}'.format(symbol)
- else:
- if i == 0:
- string += '{}*{}'.format(coefficient, symbol)
- elif coefficient > 0:
- string += ' + {}*{}'.format(coefficient, symbol)
- else:
- assert coefficient < 0
- coefficient *= -1
- string += ' - {}*{}'.format(coefficient, symbol)
- i += 1
- constant = self.constant
- if constant != 0 and i == 0:
- string += '{}'.format(constant)
- elif constant > 0:
- string += ' + {}'.format(constant)
- elif constant < 0:
- constant *= -1
- string += ' - {}'.format(constant)
- if string == '':
- string = '0'
- return string
-
- def _parenstr(self, always=False):
- string = str(self)
- if not always and (self.isconstant() or self.issymbol()):
- return string
- else:
- return '({})'.format(string)
-
- def __repr__(self):
- return '{}({!r})'.format(self.__class__.__name__, str(self))
-
- @_polymorphic_method
- def __eq__(self, other):
- # "normal" equality
- # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs
- return isinstance(other, Expression) and \
- self._coefficients == other._coefficients and \
- self.constant == other.constant
-
- def __hash__(self):
- return hash((tuple(sorted(self._coefficients.items())), self._constant))
-
- 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_method
- def _eq(self, other):
- return Polyhedron(equalities=[(self - other)._toint()])
-
- @_polymorphic_method
- def __le__(self, other):
- return Polyhedron(inequalities=[(other - self)._toint()])
-
- @_polymorphic_method
- def __lt__(self, other):
- return Polyhedron(inequalities=[(other - self)._toint() - 1])
-
- @_polymorphic_method
- def __ge__(self, other):
- return Polyhedron(inequalities=[(self - other)._toint()])
-
- @_polymorphic_method
- def __gt__(self, other):
- 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
-
- @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 symbols(names):
- if isinstance(names, str):
- names = names.replace(',', ' ').split()
- return (Symbol(name) for name in names)
-
-
-@_polymorphic_operator
-def eq(a, b):
- return a.__eq__(b)
-
-@_polymorphic_operator
-def le(a, b):
- return a.__le__(b)
-
-@_polymorphic_operator
-def lt(a, b):
- return a.__lt__(b)
-
-@_polymorphic_operator
-def ge(a, b):
- return a.__ge__(b)
-
-@_polymorphic_operator
-def gt(a, b):
- return a.__gt__(b)
-
-
-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:
- raise TypeError('too many arguments')
- return cls.fromstring(equalities)
- self = super().__new__(cls)
- self._equalities = []
- if equalities is not None:
- for constraint in equalities:
- for value in constraint.values():
- if value.denominator != 1:
- 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:
- for value in constraint.values():
- if value.denominator != 1:
- 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):
- return self._equalities
-
- @property
- def inequalities(self):
- return self._inequalities
-
- @property
- def constraints(self):
- return self._constraints
-
- @property
- def symbols(self):
- return self._symbols
-
- @property
- def dimension(self):
- return len(self.symbols)
-
- def __bool__(self):
- return not self.is_empty()
-
- def __contains__(self, value):
- # is the value in the polyhedron?
- raise NotImplementedError
-
- def __eq__(self, other):
- # 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):
- bset = self._toisl()
- return bool(libisl.isl_basic_set_is_empty(bset))
-
- def isuniverse(self):
- 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
- #symbols = self._symbolunion(other)
- bset = self._toisl()
- other = other._toisl()
- return bool(libisl.isl_set_is_disjoint(bset, other))
-
- def issubset(self, other):
- # 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):
- 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
- raise NotImplementedError
-
- def __ge__(self, other):
- 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):
- # return a new polyhedron with elements from the polyhedron and all
- # others (convex union)
- raise NotImplementedError
-
- def __or__(self, other):
- return self.union(other)
-
- def intersection(self, *others):
- # return a new polyhedron with elements common to the polyhedron and all
- # others
- # a poor man's implementation could be:
- # equalities = list(self.equalities)
- # inequalities = list(self.inequalities)
- # for other in others:
- # equalities.extend(other.equalities)
- # inequalities.extend(other.inequalities)
- # return self.__class__(equalities, inequalities)
- raise NotImplementedError
-
- def __and__(self, other):
- return self.intersection(other)
-
- 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)
-
- def __str__(self):
- constraints = []
- for constraint in self.equalities:
- constraints.append('{} == 0'.format(constraint))
- for constraint in self.inequalities:
- constraints.append('{} >= 0'.format(constraint))
- return '{}'.format(', '.join(constraints))
-
- def __repr__(self):
- if self.isempty():
- return 'Empty'
- elif self.isuniverse():
- return 'Universe'
- else:
- return '{}({!r})'.format(self.__class__.__name__, str(self))
-
- @classmethod
- def _fromsympy(cls, expr):
- import sympy
- equalities = []
- inequalities = []
- if expr.func == sympy.And:
- for arg in expr.args:
- arg_eqs, arg_ins = cls._fromsympy(arg)
- equalities.extend(arg_eqs)
- inequalities.extend(arg_ins)
- elif expr.func == sympy.Eq:
- expr = Expression.fromsympy(expr.args[0] - expr.args[1])
- equalities.append(expr)
- else:
- if expr.func == sympy.Lt:
- expr = Expression.fromsympy(expr.args[1] - expr.args[0] - 1)
- elif expr.func == sympy.Le:
- expr = Expression.fromsympy(expr.args[1] - expr.args[0])
- elif expr.func == sympy.Ge:
- expr = Expression.fromsympy(expr.args[0] - expr.args[1])
- elif expr.func == sympy.Gt:
- expr = Expression.fromsympy(expr.args[0] - expr.args[1] - 1)
- else:
- raise ValueError('non-polyhedral expression: {!r}'.format(expr))
- inequalities.append(expr)
- return equalities, inequalities
-
- @classmethod
- def fromsympy(cls, expr):
- import sympy
- equalities, inequalities = cls._fromsympy(expr)
- return cls(equalities, inequalities)
-
- def tosympy(self):
- import sympy
- constraints = []
- for equality in self.equalities:
- constraints.append(sympy.Eq(equality.tosympy(), 0))
- for inequality in self.inequalities:
- constraints.append(sympy.Ge(inequality.tosympy(), 0))
- return sympy.And(*constraints)
-
- 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 _fromisl(cls, bset, symbols):
- raise NotImplementedError
- 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())
projects / linpy.git / commitdiff