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         '_symbols',
  48         '_dimension',
  49     )
  50
  51     def __new__(cls, equalities=None, inequalities=None):
  52         """
  53         Return a polyhedron from two sequences of linear expressions: equalities
  54         is a list of expressions equal to 0, and inequalities is a list of
  55         expressions greater or equal to 0. For example, the polyhedron
  56         0 <= x <= 2, 0 <= y <= 2 can be constructed with:
  57
  58         >>> x, y = symbols('x y')
  59         >>> square = Polyhedron([], [x, 2 - x, y, 2 - y])
  60
  61         It may be easier to use comparison operators LinExpr.__lt__(),
  62         LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
  63         Le(), Eq(), Ge() and Gt(), using one of the following instructions:
  64
  65         >>> x, y = symbols('x y')
  66         >>> square = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
  67         >>> square = Le(0, x, 2) & Le(0, y, 2)
  68
  69         It is also possible to build a polyhedron from a string.
  70
  71         >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
  72
  73         Finally, a polyhedron can be constructed from a GeometricObject
  74         instance, calling the GeometricObject.aspolyedron() method. This way, it
  75         is possible to compute the polyhedral hull of a Domain instance, i.e.,
  76         the convex hull of two polyhedra:
  77
  78         >>> square = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
  79         >>> square2 = Polyhedron('2 <= x <= 4, 2 <= y <= 4')
  80         >>> Polyhedron(square | square2)
  81         """
  82         if isinstance(equalities, str):
  83             if inequalities is not None:
  84                 raise TypeError('too many arguments')
  85             return cls.fromstring(equalities)
  86         elif isinstance(equalities, GeometricObject):
  87             if inequalities is not None:
  88                 raise TypeError('too many arguments')
  89             return equalities.aspolyhedron()
  90         sc_equalities = []
  91         if equalities is not None:
  92             for equality in equalities:
  93                 if not isinstance(equality, LinExpr):
  94                     raise TypeError('equalities must be linear expressions')
  95                 sc_equalities.append(equality.scaleint())
  96         sc_inequalities = []
  97         if inequalities is not None:
  98             for inequality in inequalities:
  99                 if not isinstance(inequality, LinExpr):
 100                     raise TypeError('inequalities must be linear expressions')
 101                 sc_inequalities.append(inequality.scaleint())
 102         symbols = cls._xsymbols(sc_equalities + sc_inequalities)
 103         islbset = cls._toislbasicset(sc_equalities, sc_inequalities, symbols)
 104         return cls._fromislbasicset(islbset, symbols)
 105
 106     @property
 107     def equalities(self):
 108         """
 109         The tuple of equalities. This is a list of LinExpr instances that are
 110         equal to 0 in the polyhedron.
 111         """
 112         return self._equalities
 113
 114     @property
 115     def inequalities(self):
 116         """
 117         The tuple of inequalities. This is a list of LinExpr instances that are
 118         greater or equal to 0 in the polyhedron.
 119         """
 120         return self._inequalities
 121
 122     @property
 123     def constraints(self):
 124         """
 125         The tuple of constraints, i.e., equalities and inequalities. This is
 126         semantically equivalent to: equalities + inequalities.
 127         """
 128         return self._equalities + self._inequalities
 129
 130     @property
 131     def polyhedra(self):
 132         return self,
 133
 134     def make_disjoint(self):
 135         return self
 136
 137     def isuniverse(self):
 138         islbset = self._toislbasicset(self.equalities, self.inequalities,
 139             self.symbols)
 140         universe = bool(libisl.isl_basic_set_is_universe(islbset))
 141         libisl.isl_basic_set_free(islbset)
 142         return universe
 143
 144     def aspolyhedron(self):
 145         return self
 146
 147     def convex_union(self, *others):
 148         """
 149         Return the convex union of two or more polyhedra.
 150         """
 151         for other in others:
 152             if not isinstance(other, Polyhedron):
 153                 raise TypeError('arguments must be Polyhedron instances')
 154         return Polyhedron(self.union(*others))
 155
 156     def __contains__(self, point):
 157         if not isinstance(point, Point):
 158             raise TypeError('point must be a Point instance')
 159         if self.symbols != point.symbols:
 160             raise ValueError('arguments must belong to the same space')
 161         for equality in self.equalities:
 162             if equality.subs(point.coordinates()) != 0:
 163                 return False
 164         for inequality in self.inequalities:
 165             if inequality.subs(point.coordinates()) < 0:
 166                 return False
 167         return True
 168
 169     def subs(self, symbol, expression=None):
 170         equalities = [equality.subs(symbol, expression)
 171             for equality in self.equalities]
 172         inequalities = [inequality.subs(symbol, expression)
 173             for inequality in self.inequalities]
 174         return Polyhedron(equalities, inequalities)
 175
 176     def asinequalities(self):
 177         """
 178         Express the polyhedron using inequalities, given as a list of
 179         expressions greater or equal to 0.
 180         """
 181         inequalities = list(self.equalities)
 182         inequalities.extend([-expression for expression in self.equalities])
 183         inequalities.extend(self.inequalities)
 184         return inequalities
 185
 186     def widen(self, other):
 187         """
 188         Compute the standard widening of two polyhedra, à la Halbwachs.
 189
 190         In its current implementation, this method is slow and should not be
 191         used on large polyhedra.
 192         """
 193         if not isinstance(other, Polyhedron):
 194             raise TypeError('argument must be a Polyhedron instance')
 195         inequalities1 = self.asinequalities()
 196         inequalities2 = other.asinequalities()
 197         inequalities = []
 198         for inequality1 in inequalities1:
 199             if other <= Polyhedron(inequalities=[inequality1]):
 200                 inequalities.append(inequality1)
 201         for inequality2 in inequalities2:
 202             for i in range(len(inequalities1)):
 203                 inequalities3 = inequalities1[:i] + inequalities[i + 1:]
 204                 inequalities3.append(inequality2)
 205                 polyhedron3 = Polyhedron(inequalities=inequalities3)
 206                 if self == polyhedron3:
 207                     inequalities.append(inequality2)
 208                     break
 209         return Polyhedron(inequalities=inequalities)
 210
 211     @classmethod
 212     def _fromislbasicset(cls, islbset, symbols):
 213         islconstraints = islhelper.isl_basic_set_constraints(islbset)
 214         equalities = []
 215         inequalities = []
 216         for islconstraint in islconstraints:
 217             constant = libisl.isl_constraint_get_constant_val(islconstraint)
 218             constant = islhelper.isl_val_to_int(constant)
 219             coefficients = {}
 220             for index, symbol in enumerate(symbols):
 221                 coefficient = libisl.isl_constraint_get_coefficient_val(islconstraint,
 222                     libisl.isl_dim_set, index)
 223                 coefficient = islhelper.isl_val_to_int(coefficient)
 224                 if coefficient != 0:
 225                     coefficients[symbol] = coefficient
 226             expression = LinExpr(coefficients, constant)
 227             if libisl.isl_constraint_is_equality(islconstraint):
 228                 equalities.append(expression)
 229             else:
 230                 inequalities.append(expression)
 231         libisl.isl_basic_set_free(islbset)
 232         self = object().__new__(Polyhedron)
 233         self._equalities = tuple(equalities)
 234         self._inequalities = tuple(inequalities)
 235         self._symbols = cls._xsymbols(self.constraints)
 236         self._dimension = len(self._symbols)
 237         return self
 238
 239     @classmethod
 240     def _toislbasicset(cls, equalities, inequalities, symbols):
 241         dimension = len(symbols)
 242         indices = {symbol: index for index, symbol in enumerate(symbols)}
 243         islsp = libisl.isl_space_set_alloc(mainctx, 0, dimension)
 244         islbset = libisl.isl_basic_set_universe(libisl.isl_space_copy(islsp))
 245         islls = libisl.isl_local_space_from_space(islsp)
 246         for equality in equalities:
 247             isleq = libisl.isl_equality_alloc(libisl.isl_local_space_copy(islls))
 248             for symbol, coefficient in equality.coefficients():
 249                 islval = str(coefficient).encode()
 250                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 251                 index = indices[symbol]
 252                 isleq = libisl.isl_constraint_set_coefficient_val(isleq,
 253                     libisl.isl_dim_set, index, islval)
 254             if equality.constant != 0:
 255                 islval = str(equality.constant).encode()
 256                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 257                 isleq = libisl.isl_constraint_set_constant_val(isleq, islval)
 258             islbset = libisl.isl_basic_set_add_constraint(islbset, isleq)
 259         for inequality in inequalities:
 260             islin = libisl.isl_inequality_alloc(libisl.isl_local_space_copy(islls))
 261             for symbol, coefficient in inequality.coefficients():
 262                 islval = str(coefficient).encode()
 263                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 264                 index = indices[symbol]
 265                 islin = libisl.isl_constraint_set_coefficient_val(islin,
 266                     libisl.isl_dim_set, index, islval)
 267             if inequality.constant != 0:
 268                 islval = str(inequality.constant).encode()
 269                 islval = libisl.isl_val_read_from_str(mainctx, islval)
 270                 islin = libisl.isl_constraint_set_constant_val(islin, islval)
 271             islbset = libisl.isl_basic_set_add_constraint(islbset, islin)
 272         return islbset
 273
 274     @classmethod
 275     def fromstring(cls, string):
 276         domain = Domain.fromstring(string)
 277         if not isinstance(domain, Polyhedron):
 278             raise ValueError('non-polyhedral expression: {!r}'.format(string))
 279         return domain
 280
 281     def __repr__(self):
 282         strings = []
 283         for equality in self.equalities:
 284             left, right, swap = 0, 0, False
 285             for i, (symbol, coefficient) in enumerate(equality.coefficients()):
 286                 if coefficient > 0:
 287                     left += coefficient * symbol
 288                 else:
 289                     right -= coefficient * symbol
 290                     if i == 0:
 291                         swap = True
 292             if equality.constant > 0:
 293                 left += equality.constant
 294             else:
 295                 right -= equality.constant
 296             if swap:
 297                 left, right = right, left
 298             strings.append('{} == {}'.format(left, right))
 299         for inequality in self.inequalities:
 300             left, right = 0, 0
 301             for symbol, coefficient in inequality.coefficients():
 302                 if coefficient < 0:
 303                     left -= coefficient * symbol
 304                 else:
 305                     right += coefficient * symbol
 306             if inequality.constant < 0:
 307                 left -= inequality.constant
 308             else:
 309                 right += inequality.constant
 310             strings.append('{} <= {}'.format(left, right))
 311         if len(strings) == 1:
 312             return strings[0]
 313         else:
 314             return 'And({})'.format(', '.join(strings))
 315
 316     def _repr_latex_(self):
 317         strings = []
 318         for equality in self.equalities:
 319             strings.append('{} = 0'.format(equality._repr_latex_().strip('$')))
 320         for inequality in self.inequalities:
 321             strings.append('{} \\ge 0'.format(inequality._repr_latex_().strip('$')))
 322         return '$${}$$'.format(' \\wedge '.join(strings))
 323
 324     @classmethod
 325     def fromsympy(cls, expr):
 326         domain = Domain.fromsympy(expr)
 327         if not isinstance(domain, Polyhedron):
 328             raise ValueError('non-polyhedral expression: {!r}'.format(expr))
 329         return domain
 330
 331     def tosympy(self):
 332         import sympy
 333         constraints = []
 334         for equality in self.equalities:
 335             constraints.append(sympy.Eq(equality.tosympy(), 0))
 336         for inequality in self.inequalities:
 337             constraints.append(sympy.Ge(inequality.tosympy(), 0))
 338         return sympy.And(*constraints)
 339
 340
 341 class EmptyType(Polyhedron):
 342     """
 343     The empty polyhedron, whose set of constraints is not satisfiable.
 344     """
 345
 346     def __new__(cls):
 347         self = object().__new__(cls)
 348         self._equalities = (Rational(1),)
 349         self._inequalities = ()
 350         self._symbols = ()
 351         self._dimension = 0
 352         return self
 353
 354     def widen(self, other):
 355         if not isinstance(other, Polyhedron):
 356             raise ValueError('argument must be a Polyhedron instance')
 357         return other
 358
 359     def __repr__(self):
 360         return 'Empty'
 361
 362     def _repr_latex_(self):
 363         return '$$\\emptyset$$'
 364
 365 Empty = EmptyType()
 366
 367
 368 class UniverseType(Polyhedron):
 369     """
 370     The universe polyhedron, whose set of constraints is always satisfiable,
 371     i.e. is empty.
 372     """
 373
 374     def __new__(cls):
 375         self = object().__new__(cls)
 376         self._equalities = ()
 377         self._inequalities = ()
 378         self._symbols = ()
 379         self._dimension = ()
 380         return self
 381
 382     def __repr__(self):
 383         return 'Universe'
 384
 385     def _repr_latex_(self):
 386         return '$$\\Omega$$'
 387
 388 Universe = UniverseType()
 389
 390
 391 def _pseudoconstructor(func):
 392     @functools.wraps(func)
 393     def wrapper(expr1, expr2, *exprs):
 394         exprs = (expr1, expr2) + exprs
 395         for expr in exprs:
 396             if not isinstance(expr, LinExpr):
 397                 if isinstance(expr, numbers.Rational):
 398                     expr = Rational(expr)
 399                 else:
 400                     raise TypeError('arguments must be rational numbers '
 401                         'or linear expressions')
 402         return func(*exprs)
 403     return wrapper
 404
 405 @_pseudoconstructor
 406 def Lt(*exprs):
 407     """
 408     Create the polyhedron with constraints expr1 < expr2 < expr3 ...
 409     """
 410     inequalities = []
 411     for left, right in zip(exprs, exprs[1:]):
 412         inequalities.append(right - left - 1)
 413     return Polyhedron([], inequalities)
 414
 415 @_pseudoconstructor
 416 def Le(*exprs):
 417     """
 418     Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
 419     """
 420     inequalities = []
 421     for left, right in zip(exprs, exprs[1:]):
 422         inequalities.append(right - left)
 423     return Polyhedron([], inequalities)
 424
 425 @_pseudoconstructor
 426 def Eq(*exprs):
 427     """
 428     Create the polyhedron with constraints expr1 == expr2 == expr3 ...
 429     """
 430     equalities = []
 431     for left, right in zip(exprs, exprs[1:]):
 432         equalities.append(left - right)
 433     return Polyhedron(equalities, [])
 434
 435 @_pseudoconstructor
 436 def Ne(*exprs):
 437     """
 438     Create the domain such that expr1 != expr2 != expr3 ... The result is a
 439     Domain object, not a Polyhedron.
 440     """
 441     domain = Universe
 442     for left, right in zip(exprs, exprs[1:]):
 443         domain &= ~Eq(left, right)
 444     return domain
 445
 446 @_pseudoconstructor
 447 def Ge(*exprs):
 448     """
 449     Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
 450     """
 451     inequalities = []
 452     for left, right in zip(exprs, exprs[1:]):
 453         inequalities.append(left - right)
 454     return Polyhedron([], inequalities)
 455
 456 @_pseudoconstructor
 457 def Gt(*exprs):
 458     """
 459     Create the polyhedron with constraints expr1 > expr2 > expr3 ...
 460     """
 461     inequalities = []
 462     for left, right in zip(exprs, exprs[1:]):
 463         inequalities.append(left - right - 1)
 464     return Polyhedron([], inequalities)