# Copyright 2014 MINES ParisTech
#
# This file is part of LinPy.
#
# LinPy is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# LinPy is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with LinPy. If not, see .
import functools
import math
import numbers
from . import islhelper
from .islhelper import mainctx, libisl
from .geometry import GeometricObject, Point
from .linexprs import LinExpr, Rational
from .domains import Domain
__all__ = [
'Polyhedron',
'Lt', 'Le', 'Eq', 'Ne', 'Ge', 'Gt',
'Empty', 'Universe',
]
class Polyhedron(Domain):
"""
A convex polyhedron (or simply "polyhedron") is the space defined by a
system of linear equalities and inequalities. This space can be unbounded. A
Z-polyhedron (simply called "polyhedron" in LinPy) is the set of integer
points in a convex polyhedron.
"""
__slots__ = (
'_equalities',
'_inequalities',
'_symbols',
'_dimension',
)
def __new__(cls, equalities=None, inequalities=None):
"""
Return a polyhedron from two sequences of linear expressions: equalities
is a list of expressions equal to 0, and inequalities is a list of
expressions greater or equal to 0. For example, the polyhedron
0 <= x <= 2, 0 <= y <= 2 can be constructed with:
>>> x, y = symbols('x y')
>>> square1 = Polyhedron([], [x, 2 - x, y, 2 - y])
>>> square1
And(0 <= x, x <= 2, 0 <= y, y <= 2)
It may be easier to use comparison operators LinExpr.__lt__(),
LinExpr.__le__(), LinExpr.__ge__(), LinExpr.__gt__(), or functions Lt(),
Le(), Eq(), Ge() and Gt(), using one of the following instructions:
>>> x, y = symbols('x y')
>>> square1 = (0 <= x) & (x <= 2) & (0 <= y) & (y <= 2)
>>> square1 = Le(0, x, 2) & Le(0, y, 2)
It is also possible to build a polyhedron from a string.
>>> square1 = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
Finally, a polyhedron can be constructed from a GeometricObject
instance, calling the GeometricObject.aspolyedron() method. This way, it
is possible to compute the polyhedral hull of a Domain instance, i.e.,
the convex hull of two polyhedra:
>>> square1 = Polyhedron('0 <= x <= 2, 0 <= y <= 2')
>>> square2 = Polyhedron('1 <= x <= 3, 1 <= y <= 3')
>>> Polyhedron(square1 | square2)
And(0 <= x, 0 <= y, x <= y + 2, y <= x + 2, x <= 3, y <= 3)
"""
if isinstance(equalities, str):
if inequalities is not None:
raise TypeError('too many arguments')
return cls.fromstring(equalities)
elif isinstance(equalities, GeometricObject):
if inequalities is not None:
raise TypeError('too many arguments')
return equalities.aspolyhedron()
sc_equalities = []
if equalities is not None:
for equality in equalities:
if isinstance(equality, LinExpr):
sc_equalities.append(equality.scaleint())
elif isinstance(equality, numbers.Rational):
sc_equalities.append(Rational(equality).scaleint())
else:
raise TypeError('equalities must be linear expressions '
'or rational numbers')
sc_inequalities = []
if inequalities is not None:
for inequality in inequalities:
if isinstance(inequality, LinExpr):
sc_inequalities.append(inequality.scaleint())
elif isinstance(inequality, numbers.Rational):
sc_inequalities.append(Rational(inequality).scaleint())
else:
raise TypeError('inequalities must be linear expressions '
'or rational numbers')
symbols = cls._xsymbols(sc_equalities + sc_inequalities)
islbset = cls._toislbasicset(sc_equalities, sc_inequalities, symbols)
return cls._fromislbasicset(islbset, symbols)
@property
def equalities(self):
"""
The tuple of equalities. This is a list of LinExpr instances that are
equal to 0 in the polyhedron.
"""
return self._equalities
@property
def inequalities(self):
"""
The tuple of inequalities. This is a list of LinExpr instances that are
greater or equal to 0 in the polyhedron.
"""
return self._inequalities
@property
def constraints(self):
"""
The tuple of constraints, i.e., equalities and inequalities. This is
semantically equivalent to: equalities + inequalities.
"""
return self._equalities + self._inequalities
@property
def polyhedra(self):
return self,
def make_disjoint(self):
return self
def isuniverse(self):
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 aspolyhedron(self):
return self
def convex_union(self, *others):
"""
Return the convex union of two or more polyhedra.
"""
for other in others:
if not isinstance(other, Polyhedron):
raise TypeError('arguments must be Polyhedron instances')
return Polyhedron(self.union(*others))
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):
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):
"""
Express the polyhedron using inequalities, given as a list of
expressions greater or equal to 0.
"""
inequalities = list(self.equalities)
inequalities.extend([-expression for expression in self.equalities])
inequalities.extend(self.inequalities)
return inequalities
def widen(self, other):
"""
Compute the standard widening of two polyhedra, à la Halbwachs.
In its current implementation, this method is slow and should not be
used on large polyhedra.
"""
if not isinstance(other, Polyhedron):
raise TypeError('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):
if bool(libisl.isl_basic_set_is_empty(islbset)):
return Empty
if bool(libisl.isl_basic_set_is_universe(islbset)):
return Universe
islconstraints = islhelper.isl_basic_set_constraints(islbset)
equalities = []
inequalities = []
for islconstraint in islconstraints:
constant = libisl.isl_constraint_get_constant_val(islconstraint)
constant = islhelper.isl_val_to_int(constant)
coefficients = {}
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
expression = LinExpr(coefficients, constant)
if libisl.isl_constraint_is_equality(islconstraint):
equalities.append(expression)
else:
inequalities.append(expression)
libisl.isl_basic_set_free(islbset)
self = object().__new__(Polyhedron)
self._equalities = tuple(equalities)
self._inequalities = tuple(inequalities)
self._symbols = cls._xsymbols(self.constraints)
self._dimension = len(self._symbols)
return self
@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():
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, index, islval)
if equality.constant != 0:
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():
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, index, islval)
if inequality.constant != 0:
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 fromstring(cls, string):
domain = Domain.fromstring(string)
if not isinstance(domain, Polyhedron):
raise ValueError('non-polyhedral expression: {!r}'.format(string))
return domain
def __repr__(self):
strings = []
for equality in self.equalities:
left, right, swap = 0, 0, False
for i, (symbol, coefficient) in enumerate(equality.coefficients()):
if coefficient > 0:
left += coefficient * symbol
else:
right -= coefficient * symbol
if i == 0:
swap = True
if equality.constant > 0:
left += equality.constant
else:
right -= equality.constant
if swap:
left, right = right, left
strings.append('{} == {}'.format(left, right))
for inequality in self.inequalities:
left, right = 0, 0
for symbol, coefficient in inequality.coefficients():
if coefficient < 0:
left -= coefficient * symbol
else:
right += coefficient * symbol
if inequality.constant < 0:
left -= inequality.constant
else:
right += inequality.constant
strings.append('{} <= {}'.format(left, right))
if len(strings) == 1:
return strings[0]
else:
return 'And({})'.format(', '.join(strings))
@classmethod
def fromsympy(cls, expression):
domain = Domain.fromsympy(expression)
if not isinstance(domain, Polyhedron):
raise ValueError('non-polyhedral expression: {!r}'.format(expression))
return domain
def tosympy(self):
import sympy
constraints = []
for equality in self.equalities:
constraints.append(sympy.Eq(equality.tosympy(), 0))
for inequality in self.inequalities:
constraints.append(sympy.Ge(inequality.tosympy(), 0))
return sympy.And(*constraints)
class EmptyType(Polyhedron):
"""
The empty polyhedron, whose set of constraints is not satisfiable.
"""
def __new__(cls):
self = object().__new__(cls)
self._equalities = (Rational(1),)
self._inequalities = ()
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'
Empty = EmptyType()
class UniverseType(Polyhedron):
"""
The universe polyhedron, whose set of constraints is always satisfiable,
i.e. is empty.
"""
def __new__(cls):
self = object().__new__(cls)
self._equalities = ()
self._inequalities = ()
self._symbols = ()
self._dimension = ()
return self
def __repr__(self):
return 'Universe'
Universe = UniverseType()
def _pseudoconstructor(func):
@functools.wraps(func)
def wrapper(expression1, expression2, *expressions):
expressions = (expression1, expression2) + expressions
for expression in expressions:
if not isinstance(expression, LinExpr):
if isinstance(expression, numbers.Rational):
expression = Rational(expression)
else:
raise TypeError('arguments must be rational numbers '
'or linear expressions')
return func(*expressions)
return wrapper
@_pseudoconstructor
def Lt(*expressions):
"""
Create the polyhedron with constraints expr1 < expr2 < expr3 ...
"""
inequalities = []
for left, right in zip(expressions, expressions[1:]):
inequalities.append(right - left - 1)
return Polyhedron([], inequalities)
@_pseudoconstructor
def Le(*expressions):
"""
Create the polyhedron with constraints expr1 <= expr2 <= expr3 ...
"""
inequalities = []
for left, right in zip(expressions, expressions[1:]):
inequalities.append(right - left)
return Polyhedron([], inequalities)
@_pseudoconstructor
def Eq(*expressions):
"""
Create the polyhedron with constraints expr1 == expr2 == expr3 ...
"""
equalities = []
for left, right in zip(expressions, expressions[1:]):
equalities.append(left - right)
return Polyhedron(equalities, [])
@_pseudoconstructor
def Ne(*expressions):
"""
Create the domain such that expr1 != expr2 != expr3 ... The result is a
Domain object, not a Polyhedron.
"""
domain = Universe
for left, right in zip(expressions, expressions[1:]):
domain &= ~Eq(left, right)
return domain
@_pseudoconstructor
def Ge(*expressions):
"""
Create the polyhedron with constraints expr1 >= expr2 >= expr3 ...
"""
inequalities = []
for left, right in zip(expressions, expressions[1:]):
inequalities.append(left - right)
return Polyhedron([], inequalities)
@_pseudoconstructor
def Gt(*expressions):
"""
Create the polyhedron with constraints expr1 > expr2 > expr3 ...
"""
inequalities = []
for left, right in zip(expressions, expressions[1:]):
inequalities.append(left - right - 1)
return Polyhedron([], inequalities)