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