X-Git-Url: https://scm.cri.ensmp.fr/git/linpy.git/blobdiff_plain/1d494bb187b70135df721c13306d7f26fdf33f50..25ce908cffca380f930182a77c1e5a4491042a1c:/pypol/polyhedra.py diff --git a/pypol/polyhedra.py b/pypol/polyhedra.py index 787e965..fe143d4 100644 --- a/pypol/polyhedra.py +++ b/pypol/polyhedra.py @@ -1,12 +1,12 @@ -import ast import functools +import math import numbers -import re from . import islhelper from .islhelper import mainctx, libisl -from .linexprs import Expression, Constant +from .geometry import GeometricObject, Point +from .linexprs import Expression, Rational from .domains import Domain @@ -32,42 +32,47 @@ class Polyhedron(Domain): if inequalities is not None: raise TypeError('too many arguments') return cls.fromstring(equalities) - elif isinstance(equalities, Polyhedron): + elif isinstance(equalities, GeometricObject): if inequalities is not None: raise TypeError('too many arguments') - return equalities - elif isinstance(equalities, Domain): - if inequalities is not None: - raise TypeError('too many arguments') - return equalities.polyhedral_hull() + return equalities.aspolyhedron() if equalities is None: equalities = [] else: for i, equality in enumerate(equalities): if not isinstance(equality, Expression): raise TypeError('equalities must be linear expressions') - equalities[i] = equality._toint() + equalities[i] = equality.scaleint() if inequalities is None: inequalities = [] else: for i, inequality in enumerate(inequalities): if not isinstance(inequality, Expression): raise TypeError('inequalities must be linear expressions') - inequalities[i] = inequality._toint() + inequalities[i] = inequality.scaleint() symbols = cls._xsymbols(equalities + inequalities) islbset = cls._toislbasicset(equalities, inequalities, symbols) return cls._fromislbasicset(islbset, symbols) @property def equalities(self): + """ + Return a list of the equalities in a set. + """ return self._equalities @property def inequalities(self): + """ + Return a list of the inequalities in a set. + """ return self._inequalities @property def constraints(self): + """ + Return ta list of the constraints of a set. + """ return self._constraints @property @@ -75,30 +80,87 @@ class Polyhedron(Domain): return self, def disjoint(self): + """ + Return a set as disjoint. + """ return self def isuniverse(self): + """ + Return true if a set is the Universe set. + """ islbset = self._toislbasicset(self.equalities, self.inequalities, self.symbols) universe = bool(libisl.isl_basic_set_is_universe(islbset)) libisl.isl_basic_set_free(islbset) return universe - def polyhedral_hull(self): + def aspolyhedron(self): + """ + Return polyhedral hull of a set. + """ return self + def __contains__(self, point): + if not isinstance(point, Point): + raise TypeError('point must be a Point instance') + if self.symbols != point.symbols: + raise ValueError('arguments must belong to the same space') + for equality in self.equalities: + if equality.subs(point.coordinates()) != 0: + return False + for inequality in self.inequalities: + if inequality.subs(point.coordinates()) < 0: + return False + return True + + def subs(self, symbol, expression=None): + """ + Subsitute the given value into an expression and return the resulting expression. + """ + equalities = [equality.subs(symbol, expression) + for equality in self.equalities] + inequalities = [inequality.subs(symbol, expression) + for inequality in self.inequalities] + return Polyhedron(equalities, inequalities) + + def _asinequalities(self): + inequalities = list(self.equalities) + inequalities.extend([-expression for expression in self.equalities]) + inequalities.extend(self.inequalities) + return inequalities + + def widen(self, other): + if not isinstance(other, Polyhedron): + raise ValueError('argument must be a Polyhedron instance') + inequalities1 = self._asinequalities() + inequalities2 = other._asinequalities() + inequalities = [] + for inequality1 in inequalities1: + if other <= Polyhedron(inequalities=[inequality1]): + inequalities.append(inequality1) + for inequality2 in inequalities2: + for i in range(len(inequalities1)): + inequalities3 = inequalities1[:i] + inequalities[i + 1:] + inequalities3.append(inequality2) + polyhedron3 = Polyhedron(inequalities=inequalities3) + if self == polyhedron3: + inequalities.append(inequality2) + break + return Polyhedron(inequalities=inequalities) + @classmethod def _fromislbasicset(cls, islbset, symbols): islconstraints = islhelper.isl_basic_set_constraints(islbset) equalities = [] inequalities = [] for islconstraint in islconstraints: - islpr = libisl.isl_printer_to_str(mainctx) constant = libisl.isl_constraint_get_constant_val(islconstraint) constant = islhelper.isl_val_to_int(constant) coefficients = {} - for dim, symbol in enumerate(symbols): - coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint, libisl.isl_dim_set, dim) + for index, symbol in enumerate(symbols): + coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint, + libisl.isl_dim_set, index) coefficient = islhelper.isl_val_to_int(coefficient) if coefficient != 0: coefficients[symbol] = coefficient @@ -119,136 +181,79 @@ class Polyhedron(Domain): @classmethod def _toislbasicset(cls, equalities, inequalities, symbols): dimension = len(symbols) + indices = {symbol: index for index, symbol in enumerate(symbols)} islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension) islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp)) islls = libisl.isl_local_space_from_space(islsp) for equality in equalities: isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls)) for symbol, coefficient in equality.coefficients(): - val = str(coefficient).encode() - val = libisl.isl_val_read_from_str(mainctx, val) - sid = symbols.index(symbol) + islval = str(coefficient).encode() + islval = libisl.isl_val_read_from_str(mainctx, islval) + index = indices[symbol] isleq = libisl.isl_constraint_set_coefficient_val(isleq, - libisl.isl_dim_set, sid, val) + libisl.isl_dim_set, index, islval) if equality.constant != 0: - val = str(equality.constant).encode() - val = libisl.isl_val_read_from_str(mainctx, val) - isleq = libisl.isl_constraint_set_constant_val(isleq, val) + islval = str(equality.constant).encode() + islval = libisl.isl_val_read_from_str(mainctx, islval) + isleq = libisl.isl_constraint_set_constant_val(isleq, islval) islbset = libisl.isl_basic_set_add_constraint(islbset, isleq) for inequality in inequalities: islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls)) for symbol, coefficient in inequality.coefficients(): - val = str(coefficient).encode() - val = libisl.isl_val_read_from_str(mainctx, val) - sid = symbols.index(symbol) + islval = str(coefficient).encode() + islval = libisl.isl_val_read_from_str(mainctx, islval) + index = indices[symbol] islin = libisl.isl_constraint_set_coefficient_val(islin, - libisl.isl_dim_set, sid, val) + libisl.isl_dim_set, index, islval) if inequality.constant != 0: - val = str(inequality.constant).encode() - val = libisl.isl_val_read_from_str(mainctx, val) - islin = libisl.isl_constraint_set_constant_val(islin, val) + islval = str(inequality.constant).encode() + islval = libisl.isl_val_read_from_str(mainctx, islval) + islin = libisl.isl_constraint_set_constant_val(islin, islval) islbset = libisl.isl_basic_set_add_constraint(islbset, islin) return islbset - @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) + domain = Domain.fromstring(string) + if not isinstance(domain, Polyhedron): + raise ValueError('non-polyhedral expression: {!r}'.format(string)) + return domain def __repr__(self): - if self.isempty(): - return 'Empty' - elif self.isuniverse(): - return 'Universe' + strings = [] + for equality in self.equalities: + strings.append('Eq({}, 0)'.format(equality)) + for inequality in self.inequalities: + strings.append('Ge({}, 0)'.format(inequality)) + if len(strings) == 1: + return strings[0] else: - strings = [] - for equality in self.equalities: - strings.append('Eq({}, 0)'.format(equality)) - for inequality in self.inequalities: - strings.append('Ge({}, 0)'.format(inequality)) - if len(strings) == 1: - return strings[0] - else: - return 'And({})'.format(', '.join(strings)) + return 'And({})'.format(', '.join(strings)) - @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 + + def _repr_latex_(self): + strings = [] + for equality in self.equalities: + strings.append('{} = 0'.format(equality._repr_latex_().strip('$'))) + for inequality in self.inequalities: + strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('$'))) + return '$${}$$'.format(' \\wedge '.join(strings)) @classmethod def fromsympy(cls, expr): - import sympy - equalities, inequalities = cls._fromsympy(expr) - return cls(equalities, inequalities) + """ + Convert a sympy object to an expression. + """ + domain = Domain.fromsympy(expr) + if not isinstance(domain, Polyhedron): + raise ValueError('non-polyhedral expression: {!r}'.format(expr)) + return domain def tosympy(self): + """ + Return an expression as a sympy object. + """ import sympy constraints = [] for equality in self.equalities: @@ -257,48 +262,112 @@ class Polyhedron(Domain): constraints.append(sympy.Ge(inequality.tosympy(), 0)) return sympy.And(*constraints) +class EmptyType(Polyhedron): + + __slots__ = Polyhedron.__slots__ + + def __new__(cls): + self = object().__new__(cls) + self._equalities = (Rational(1),) + self._inequalities = () + self._constraints = self._equalities + self._symbols = () + self._dimension = 0 + return self + + def widen(self, other): + if not isinstance(other, Polyhedron): + raise ValueError('argument must be a Polyhedron instance') + return other + + def __repr__(self): + return 'Empty' + + def _repr_latex_(self): + return '$$\\emptyset$$' + +Empty = EmptyType() + + +class UniverseType(Polyhedron): + + __slots__ = Polyhedron.__slots__ + + def __new__(cls): + self = object().__new__(cls) + self._equalities = () + self._inequalities = () + self._constraints = () + self._symbols = () + self._dimension = () + return self + + def __repr__(self): + return 'Universe' + + def _repr_latex_(self): + return '$$\\Omega$$' + +Universe = UniverseType() + def _polymorphic(func): @functools.wraps(func) def wrapper(left, right): - if isinstance(left, numbers.Rational): - left = Constant(left) - elif not isinstance(left, Expression): - raise TypeError('left must be a a rational number ' - 'or a linear expression') - if isinstance(right, numbers.Rational): - right = Constant(right) - elif not isinstance(right, Expression): - raise TypeError('right must be a a rational number ' - 'or a linear expression') + if not isinstance(left, Expression): + if isinstance(left, numbers.Rational): + left = Rational(left) + else: + raise TypeError('left must be a a rational number ' + 'or a linear expression') + if not isinstance(right, Expression): + if isinstance(right, numbers.Rational): + right = Rational(right) + else: + raise TypeError('right must be a a rational number ' + 'or a linear expression') return func(left, right) return wrapper @_polymorphic def Lt(left, right): + """ + Assert first set is less than the second set. + """ return Polyhedron([], [right - left - 1]) @_polymorphic def Le(left, right): + """ + Assert first set is less than or equal to the second set. + """ return Polyhedron([], [right - left]) @_polymorphic def Eq(left, right): + """ + Assert first set is equal to the second set. + """ return Polyhedron([left - right], []) @_polymorphic def Ne(left, right): + """ + Assert first set is not equal to the second set. + """ return ~Eq(left, right) @_polymorphic def Gt(left, right): + """ + Assert first set is greater than the second set. + """ return Polyhedron([], [left - right - 1]) @_polymorphic def Ge(left, right): + """ + Assert first set is greater than or equal to the second set. + """ return Polyhedron([], [left - right]) - -Empty = Eq(1, 0) - -Universe = Polyhedron([])