# 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 <http://www.gnu.org/licenses/>.

import functools
import numbers

from . import islhelper

from .domains import Domain
from .geometry import GeometricObject, Point
from .islhelper import libisl, mainctx
from .linexprs import LinExpr, Rational


__all__ = [
    'Empty',
    'Eq',
    'Ge',
    'Gt',
    'Le',
    'Lt',
    'Ne',
    'Polyhedron',
    '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)