linpy/polyhedra.py

   1 # Copyright 2014 MINES ParisTech
   2 #
   3 # This file is part of LinPy.
   4 #
   5 # LinPy is free software: you can redistribute it and/or modify
   6 # it under the terms of the GNU General Public License as published by
   7 # the Free Software Foundation, either version 3 of the License, or
   8 # (at your option) any later version.
   9 #
  10 # LinPy is distributed in the hope that it will be useful,
  11 # but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13 # GNU General Public License for more details.
  14 #
  15 # You should have received a copy of the GNU General Public License
  16 # along with LinPy.  If not, see <http://www.gnu.org/licenses/>.
  17
  18 import functools
  19 import math
  20 import numbers
  21
  22 from . import islhelper
  23
  24 from .islhelper import mainctx, libisl
  25 from .geometry import GeometricObject, Point
  26 from .linexprs import LinExpr, Rational
  27 from .domains import Domain
  28
  29
  30 __all__ = [
  31     'Polyhedron',
  32     'Lt', 'Le', 'Eq', 'Ne', 'Ge', 'Gt',
  33     'Empty', 'Universe',
  34 ]
  35
  36
  37 class Polyhedron(Domain):
  38     """
  39     A convex polyhedron (or simply "polyhedron") is the space defined by a
  40     system of linear equalities and inequalities. This space can be
  41     unbounded.
  42     """
  43
  44     __slots__ = (
  45         '_equalities',
  46         '_inequalities',
  47         '_constraints',
  48         '_symbols',
  49         '_dimension',
  50     )
  51
  52     def __new__(cls, equalities=None, inequalities=None):
  53         """
  54         Return a polyhedron from two sequences of linear expressions: equalities
  55         is a list of expressions equal to 0, and inequalities is a list of
  56         expressions greater or equal to 0. For example, the polyhedron
  57         0 <= x <= 2, 0 <= y <= 2 can be constructed with:
  58
  59         >>> x, y = symbols('x y')
  60         >>> square = Polyhedron([], [x, 2 - x, y, 2 - y])
  61
  62         It may be easier to use comparison operators LinExpr.__lt__(),
  63         LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
  64         Le(), Eq(), Ge() and Gt(), using one of the following instructions:
  65
  66         >>> x, y = symbols('x y')
  67         >>> square = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
  68         >>> square = Le(0, x, 2) & Le(0, y, 2)
  69
  70         It is also possible to build a polyhedron from a string.
  71
  72         >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
  73
  74         Finally, a polyhedron can be constructed from a GeometricObject
  75         instance, calling the GeometricObject.aspolyedron() method. This way, it
  76         is possible to compute the polyhedral hull of a Domain instance, i.e.,
  77         the convex hull of two polyhedra:
  78
  79         >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
  80         >>> square2 = Polyhedron('2 <= x <= 4, 2 <= y <= 4')
  81         >>> Polyhedron(square | square2)
  82         """
  83         if isinstance(equalities, str):
  84             if inequalities is not None:
  85                 raise TypeError('too many arguments')
  86             return cls.fromstring(equalities)
  87         elif isinstance(equalities, GeometricObject):
  88             if inequalities is not None:
  89                 raise TypeError('too many arguments')
  90             return equalities.aspolyhedron()
  91         if equalities is None:
  92             equalities = []
  93         else:
  94             for i, equality in enumerate(equalities):
  95                 if not isinstance(equality, LinExpr):
  96                     raise TypeError('equalities must be linear expressions')
  97                 equalities[i] = equality.scaleint()
  98         if inequalities is None:
  99             inequalities = []
 100         else:
 101             for i, inequality in enumerate(inequalities):
 102                 if not isinstance(inequality, LinExpr):
 103                     raise TypeError('inequalities must be linear expressions')
 104                 inequalities[i] = inequality.scaleint()
 105         symbols = cls._xsymbols(equalities + inequalities)
 106         islbset = cls._toislbasicset(equalities, inequalities, symbols)
 107         return cls._fromislbasicset(islbset, symbols)
 108
 109     @property
 110     def equalities(self):
 111         """
 112         The tuple of equalities. This is a list of LinExpr instances that are
 113         equal to 0 in the polyhedron.
 114         """
 115         return self._equalities
 116
 117     @property
 118     def inequalities(self):
 119         """
 120         The tuple of inequalities. This is a list of LinExpr instances that are
 121         greater or equal to 0 in the polyhedron.
 122         """
 123         return self._inequalities
 124
 125     @property
 126     def constraints(self):
 127         """
 128         The tuple of constraints, i.e., equalities and inequalities. This is
 129         semantically equivalent to: equalities + inequalities.
 130         """
 131         return self._constraints
 132
 133     @property
 134     def polyhedra(self):
 135         return self,
 136
 137     def make_disjoint(self):
 138         return self
 139
 140     def isuniverse(self):
 141         islbset = self._toislbasicset(self.equalities, self.inequalities,
 142             self.symbols)
 143         universe = bool(libisl.isl_basic_set_is_universe(islbset))
 144         libisl.isl_basic_set_free(islbset)
 145         return universe
 146
 147     def aspolyhedron(self):
 148         return self
 149
 150     def __contains__(self, point):
 151         if not isinstance(point, Point):
 152             raise TypeError('point must be a Point instance')
 153         if self.symbols != point.symbols:
 154             raise ValueError('arguments must belong to the same space')
 155         for equality in self.equalities:
 156             if equality.subs(point.coordinates()) != 0:
 157                 return False
 158         for inequality in self.inequalities:
 159             if inequality.subs(point.coordinates()) < 0:
 160                 return False
 161         return True
 162
 163     def subs(self, symbol, expression=None):
 164         equalities = [equality.subs(symbol, expression)
 165             for equality in self.equalities]
 166         inequalities = [inequality.subs(symbol, expression)
 167             for inequality in self.inequalities]
 168         return Polyhedron(equalities, inequalities)
 169
 170     def _asinequalities(self):
 171         inequalities = list(self.equalities)
 172         inequalities.extend([-expression for expression in self.equalities])
 173         inequalities.extend(self.inequalities)
 174         return inequalities
 175
 176     def widen(self, other):
 177         """
 178         Compute the standard widening of two polyhedra, à la Halbwachs.
 179         """
 180         if not isinstance(other, Polyhedron):
 181             raise ValueError('argument must be a Polyhedron instance')
 182         inequalities1 = self._asinequalities()
 183         inequalities2 = other._asinequalities()
 184         inequalities = []
 185         for inequality1 in inequalities1:
 186             if other <= Polyhedron(inequalities=[inequality1]):
 187                 inequalities.append(inequality1)
 188         for inequality2 in inequalities2:
 189             for i in range(len(inequalities1)):
 190                 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
 191                 inequalities3.append(inequality2)
 192                 polyhedron3 = Polyhedron(inequalities=inequalities3)
 193                 if self == polyhedron3:
 194                     inequalities.append(inequality2)
 195                     break
 196         return Polyhedron(inequalities=inequalities)
 197
 198     @classmethod
 199     def _fromislbasicset(cls, islbset, symbols):
 200         islconstraints = islhelper.isl_basic_set_constraints(islbset)
 201         equalities = []
 202         inequalities = []
 203         for islconstraint in islconstraints:
 204             constant = libisl.isl_constraint_get_constant_val(islconstraint)
 205             constant = islhelper.isl_val_to_int(constant)
 206             coefficients = {}
 207             for index, symbol in enumerate(symbols):
 208                 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
 209                     libisl.isl_dim_set, index)
 210                 coefficient = islhelper.isl_val_to_int(coefficient)
 211                 if coefficient != 0:
 212                     coefficients[symbol] = coefficient
 213             expression = LinExpr(coefficients, constant)
 214             if libisl.isl_constraint_is_equality(islconstraint):
 215                 equalities.append(expression)
 216             else:
 217                 inequalities.append(expression)
 218         libisl.isl_basic_set_free(islbset)
 219         self = object().__new__(Polyhedron)
 220         self._equalities = tuple(equalities)
 221         self._inequalities = tuple(inequalities)
 222         self._constraints = tuple(equalities + inequalities)
 223         self._symbols = cls._xsymbols(self._constraints)
 224         self._dimension = len(self._symbols)
 225         return self
 226
 227     @classmethod
 228     def _toislbasicset(cls, equalities, inequalities, symbols):
 229         dimension = len(symbols)
 230         indices = {symbol: index for index, symbol in enumerate(symbols)}
 231         islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
 232         islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
 233         islls = libisl.isl_local_space_from_space(islsp)
 234         for equality in equalities:
 235             isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
 236             for symbol, coefficient in equality.coefficients():
 237                 islval = str(coefficient).encode()
 238                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 239                 index = indices[symbol]
 240                 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
 241                     libisl.isl_dim_set, index, islval)
 242             if equality.constant != 0:
 243                 islval = str(equality.constant).encode()
 244                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 245                 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
 246             islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
 247         for inequality in inequalities:
 248             islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
 249             for symbol, coefficient in inequality.coefficients():
 250                 islval = str(coefficient).encode()
 251                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 252                 index = indices[symbol]
 253                 islin = libisl.isl_constraint_set_coefficient_val(islin,
 254                     libisl.isl_dim_set, index, islval)
 255             if inequality.constant != 0:
 256                 islval = str(inequality.constant).encode()
 257                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 258                 islin = libisl.isl_constraint_set_constant_val(islin, islval)
 259             islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
 260         return islbset
 261
 262     @classmethod
 263     def fromstring(cls, string):
 264         domain = Domain.fromstring(string)
 265         if not isinstance(domain, Polyhedron):
 266             raise ValueError('non-polyhedral expression: {!r}'.format(string))
 267         return domain
 268
 269     def __repr__(self):
 270         strings = []
 271         for equality in self.equalities:
 272             strings.append('Eq({}, 0)'.format(equality))
 273         for inequality in self.inequalities:
 274             strings.append('Ge({}, 0)'.format(inequality))
 275         if len(strings) == 1:
 276             return strings[0]
 277         else:
 278             return 'And({})'.format(', '.join(strings))
 279
 280     def _repr_latex_(self):
 281         strings = []
 282         for equality in self.equalities:
 283             strings.append('{} = 0'.format(equality._repr_latex_().strip('$')))
 284         for inequality in self.inequalities:
 285             strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('$')))
 286         return '$${}$$'.format(' \\wedge '.join(strings))
 287
 288     @classmethod
 289     def fromsympy(cls, expr):
 290         domain = Domain.fromsympy(expr)
 291         if not isinstance(domain, Polyhedron):
 292             raise ValueError('non-polyhedral expression: {!r}'.format(expr))
 293         return domain
 294
 295     def tosympy(self):
 296         import sympy
 297         constraints = []
 298         for equality in self.equalities:
 299             constraints.append(sympy.Eq(equality.tosympy(), 0))
 300         for inequality in self.inequalities:
 301             constraints.append(sympy.Ge(inequality.tosympy(), 0))
 302         return sympy.And(*constraints)
 303
 304
 305 class EmptyType(Polyhedron):
 306     """
 307     The empty polyhedron, whose set of constraints is not satisfiable.
 308     """
 309
 310     __slots__ = Polyhedron.__slots__
 311
 312     def __new__(cls):
 313         self = object().__new__(cls)
 314         self._equalities = (Rational(1),)
 315         self._inequalities = ()
 316         self._constraints = self._equalities
 317         self._symbols = ()
 318         self._dimension = 0
 319         return self
 320
 321     def widen(self, other):
 322         if not isinstance(other, Polyhedron):
 323             raise ValueError('argument must be a Polyhedron instance')
 324         return other
 325
 326     def __repr__(self):
 327         return 'Empty'
 328
 329     def _repr_latex_(self):
 330         return '$$\\emptyset$$'
 331
 332 Empty = EmptyType()
 333
 334
 335 class UniverseType(Polyhedron):
 336     """
 337     The universe polyhedron, whose set of constraints is always satisfiable,
 338     i.e. is empty.
 339     """
 340
 341     __slots__ = Polyhedron.__slots__
 342
 343     def __new__(cls):
 344         self = object().__new__(cls)
 345         self._equalities = ()
 346         self._inequalities = ()
 347         self._constraints = ()
 348         self._symbols = ()
 349         self._dimension = ()
 350         return self
 351
 352     def __repr__(self):
 353         return 'Universe'
 354
 355     def _repr_latex_(self):
 356         return '$$\\Omega$$'
 357
 358 Universe = UniverseType()
 359
 360
 361 def _polymorphic(func):
 362     @functools.wraps(func)
 363     def wrapper(left, right):
 364         if not isinstance(left, LinExpr):
 365             if isinstance(left, numbers.Rational):
 366                 left = Rational(left)
 367             else:
 368                 raise TypeError('left must be a a rational number '
 369                     'or a linear expression')
 370         if not isinstance(right, LinExpr):
 371             if isinstance(right, numbers.Rational):
 372                 right = Rational(right)
 373             else:
 374                 raise TypeError('right must be a a rational number '
 375                     'or a linear expression')
 376         return func(left, right)
 377     return wrapper
 378
 379 @_polymorphic
 380 def Lt(left, right):
 381     """
 382     Create the polyhedron with constraints expr1 < expr2 < expr3 ...
 383     """
 384     return Polyhedron([], [right - left - 1])
 385
 386 @_polymorphic
 387 def Le(left, right):
 388     """
 389     Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
 390     """
 391     return Polyhedron([], [right - left])
 392
 393 @_polymorphic
 394 def Eq(left, right):
 395     """
 396     Create the polyhedron with constraints expr1 == expr2 == expr3 ...
 397     """
 398     return Polyhedron([left - right], [])
 399
 400 @_polymorphic
 401 def Ne(left, right):
 402     """
 403     Create the domain such that expr1 != expr2 != expr3 ... The result is a
 404     Domain, not a Polyhedron.
 405     """
 406     return ~Eq(left, right)
 407
 408 @_polymorphic
 409 def Gt(left, right):
 410     """
 411     Create the polyhedron with constraints expr1 > expr2 > expr3 ...
 412     """
 413     return Polyhedron([], [left - right - 1])
 414
 415 @_polymorphic
 416 def Ge(left, right):
 417     """
 418     Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
 419     """
 420     return Polyhedron([], [left - right])