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