<commit_before>"""Tools for solving inequalities and systems of inequalities."""

import collections
import itertools

from ..core import Dummy, Eq, Ge, Gt, Integer, Le, Lt, Ne, S, Symbol, oo
from ..core.compatibility import iterable
from ..core.relational import Relational
from ..functions import Abs, Max, Min, Piecewise
from ..logic import And, Or, false, true
from ..matrices import Matrix, diag
from ..polys import PolificationFailed, Poly, parallel_poly_from_expr
from ..polys.polyutils import _nsort
from ..sets import FiniteSet, Interval, Union
from ..utilities import filldedent, ordered


__all__ = 'reduce_inequalities',


def canonicalize_inequalities(eqs):
    """Canonicalize system of inequalities to have only Lt/Le."""
    eqs = set(eqs)

    # Canonicalize constraints, Ne -> pair Lt, Eq -> pair Le
    eqs |= {Lt(*e.args) for e in eqs if isinstance(e, Ne)}
    eqs |= {Lt(e.rhs, e.lhs) for e in eqs if isinstance(e, Ne)}
    eqs |= {Le(*e.args) for e in eqs if isinstance(e, Eq)}
    eqs |= {Le(e.rhs, e.lhs) for e in eqs if isinstance(e, Eq)}
    eqs -= {e for e in eqs if isinstance(e, (Ne, Eq))}

    # Gt/Ge -> Lt, Le
    eqs = {e.reversed if e.func in (Gt, Ge) else e for e in eqs}

    # Now we have only Lt/Le
    return list(ordered(e.func(e.lhs - e.rhs, 0) for e in eqs))


def fourier_motzkin(A, b, c, j):
    """
    Fourier-Motzkin elimination for `j`-th variable.

    Parameters
    ==========

    A : Matrix
        The coefficients of the system.
    b : Matrix
        The constant terms in the right hand side of relations.
    c : Matrix
        The vector of boolean elements, which determine the
        type of relation (1 for Le and 0 - for Lt).
    j : int
        The variable index.

    Example
    =======

    >>> A = Matrix([[-1, 0], [2, 4], [1, -2]])
    >>> b = Matrix([-1, 14, -1])
    >>> c = Matrix([1, 1, 1])
    >>> fourier_motzkin(A, b, c, 0)
    (Matrix([
    [0,  4],
    [0, -2]]), Matrix([
    [12],
    [-2]]), Matrix([
    [1],
    [1]]))

    References
    ==========

    * :cite:`Schrijver1998theory`, pp. 155–156.

    """
    m = A.rows
    Z, N, P = [], [], []
    D, d, k = [Matrix()]*3

    assert m == b.rows == c.rows
    assert all(_.is_comparable for _ in A)

    for i, a in enumerate(A[:, j]):
        if a > 0:
            P.append(i)
        elif a < 0:
            N.append(i)
        else:
            Z.append(i)

    for p in itertools.chain(Z, itertools.product(N, P)):
        if p in Z:
            D = D.col_join(A[p, :])
            d = d.col_join(Matrix([b[p]]))
            k = k.col_join(Matrix([c[p]]))
        else:
            s, t = p
            D = D.col_join(A[t, j]*A[s, :] - A[s, j]*A[t, :])
            d = d.col_join(Matrix([A[t, j]*b[s] - A[s, j]*b[t]]))
            k = k.col_join(Matrix([c[s] and c[t]]))

    return D, d, k


def solve_linear_inequalities(eqs, *gens, **args):
    """
    Solve system of linear inequalities.

    Examples
    ========

    >>> solve_linear_inequalities([x >= 0, 2*x + 4*y <= 14, x - 2*y <= 1])
    (x >= 0) & (x <= 4) & (y >= x/2 - 1/2) & (y <= -x/2 + 7/2)

    """
    assert all(e.is_Relational for e in eqs)

    eqs = canonicalize_inequalities(eqs)

    polys, opt = parallel_poly_from_expr([e.lhs for e in eqs], *gens, **args)

    if not all(p.is_linear for p in polys):
        raise ValueError(f'Got non-linear inequality in {eqs}')

    gens = Matrix(opt.gens)
    A = Matrix([[p.coeff_monomial(x) for x in gens] for p in polys])
    b = Matrix([-p.coeff_monomial(1) for p in polys])
    c = Matrix([e.func is Le for e in eqs])
    res = []
    failed = []

    for i, g in reversed(list(enumerate(gens))):
        D, d, e = fourier_motzkin(A, b, c, i)

        if not D:
            failed.append(i)
            continue

        gens_g = gens.copy()
        gens_g[i] = 0

        for j, (r, x) in enumerate(zip(b - A*gens_g, c)):
            gc = A[j, i]
            op = Le if x else Lt

            if gc > 0:
                res.append(op(g, r/gc))
            elif gc < 0:
                res.append(op(r/gc, g).reversed)

        A, b, c = D, d, e

    if not A.is_zero:
        i = failed.pop(0)
        g = gens[i]
        gens_g = gens.copy()
        gens_g[i] = 0
        strict = []
        non_strict = []

        for r, x in zip(diag(*A[:, i])**-1*(b - A*gens_g), c):
            non_strict.append(r) if x else strict.append(r)

        if A[0, i] > 0:
            if strict and non_strict:
                a, b = Min(*non_strict), Min(*strict)
                res.append(Or(And(Le(g, a), Lt(a, b)), And(Lt(g, b), Le(b, a))))
            else:
                res.append((Lt if strict else Le)(g, Min(*(non_strict + strict))))
        else:
            if strict and non_strict:
                a, b = Max(*non_strict), Max(*strict)
                res.append(Or(And(Le(a, g).reversed, Lt(b, a).reversed),
                              And(Lt(b, g).reversed, Le(a, b).reversed)))
            else:
                res.append((Lt if strict else Le)(Max(*(non_strict + strict)), g).reversed)
    elif any(_ < 0 for _ in b):
        return false

    return And(*res)<commit_msg>solvers: simplify fourier_motzkin() & solve_linear_inequalities()<commit_after>"""Tools for solving inequalities and systems of inequalities."""

import collections
import itertools

from ..core import Dummy, Eq, Ge, Gt, Integer, Le, Lt, Ne, S, Symbol, oo
from ..core.compatibility import iterable
from ..core.relational import Relational
from ..functions import Abs, Max, Min, Piecewise, sign
from ..logic import And, Or, false, true
from ..matrices import Matrix, diag
from ..polys import PolificationFailed, Poly, parallel_poly_from_expr
from ..polys.polyutils import _nsort
from ..sets import FiniteSet, Interval, Union
from ..utilities import filldedent, ordered


__all__ = 'reduce_inequalities',


def canonicalize_inequalities(eqs):
    """Canonicalize system of inequalities to have only Lt/Le."""
    eqs = set(eqs)

    # Canonicalize constraints, Ne -> pair Lt, Eq -> pair Le
    eqs |= {Lt(*e.args) for e in eqs if isinstance(e, Ne)}
    eqs |= {Lt(e.rhs, e.lhs) for e in eqs if isinstance(e, Ne)}
    eqs |= {Le(*e.args) for e in eqs if isinstance(e, Eq)}
    eqs |= {Le(e.rhs, e.lhs) for e in eqs if isinstance(e, Eq)}
    eqs -= {e for e in eqs if isinstance(e, (Ne, Eq))}

    # Gt/Ge -> Lt, Le
    eqs = {e.reversed if e.func in (Gt, Ge) else e for e in eqs}

    # Now we have only Lt/Le
    return list(ordered(e.func(e.lhs - e.rhs, 0) for e in eqs))


def fourier_motzkin(A, b, c, j):
    """
    Fourier-Motzkin elimination for `j`-th variable.

    Parameters
    ==========

    A : Matrix
        The coefficients of the system.
    b : Matrix
        The constant terms in the right hand side of relations.
    c : Matrix
        The vector of boolean elements, which determine the
        type of relation (1 for Le and 0 - for Lt).
    j : int
        The variable index.

    Example
    =======

    >>> A = Matrix([[-1, 0], [2, 4], [1, -2]])
    >>> b = Matrix([-1, 14, -1])
    >>> c = Matrix([1, 1, 1])
    >>> fourier_motzkin(A, b, c, 0)
    (Matrix([
    [0,  4],
    [0, -2]]), Matrix([
    [12],
    [-2]]), Matrix([
    [1],
    [1]]))

    References
    ==========

    * :cite:`Schrijver1998theory`, pp. 155–156.

    """
    m = A.rows
    rows = [[], [], []]
    D, d, k = [Matrix()]*3

    assert m == b.rows == c.rows
    assert all(_.is_comparable for _ in A)

    for i, a in enumerate(A[:, j]):
        rows[int(sign(a) + 1)].append(i)

    for p in itertools.chain(rows[1], itertools.product(*rows[::2])):
        if p in rows[1]:
            D = D.col_join(A[p, :])
            d = d.col_join(Matrix([b[p]]))
            k = k.col_join(Matrix([c[p]]))
        else:
            s, t = p
            D = D.col_join(A[t, j]*A[s, :] - A[s, j]*A[t, :])
            d = d.col_join(Matrix([A[t, j]*b[s] - A[s, j]*b[t]]))
            k = k.col_join(Matrix([c[s] and c[t]]))

    return D, d, k


def solve_linear_inequalities(eqs, *gens, **args):
    """
    Solve system of linear inequalities.

    Examples
    ========

    >>> solve_linear_inequalities([x >= 0, 2*x + 4*y <= 14, x - 2*y <= 1])
    (x >= 0) & (x <= 4) & (y >= x/2 - 1/2) & (y <= -x/2 + 7/2)

    """
    assert all(e.is_Relational for e in eqs)

    eqs = canonicalize_inequalities(eqs)

    polys, opt = parallel_poly_from_expr([e.lhs for e in eqs], *gens, **args)

    if not all(p.is_linear for p in polys):
        raise ValueError(f'Got non-linear inequality in {eqs}')

    gens = Matrix(opt.gens)
    A = Matrix([[p.coeff_monomial(x) for x in gens] for p in polys])
    b = Matrix([-p.coeff_monomial(1) for p in polys])
    c = Matrix([e.func is Le for e in eqs])
    res = []
    failed = []
    op_map = {(1, 1): Le, (1, 0): Lt, (0, 1): Ge, (0, 0): Gt}

    for i, g in reversed(list(enumerate(gens))):
        D, d, e = fourier_motzkin(A, b, c, i)

        if not D:
            failed.append(i)
            continue

        gens_g = gens.copy()
        gens_g[i] = 0

        for j, (r, x) in enumerate(zip(b - A*gens_g, c)):
            gc = A[j, i]
            if not gc:
                continue

            res.append(op_map[(int(gc > 0), int(x))](g, r/gc))

        A, b, c = D, d, e

    if not A.is_zero:
        i = failed.pop(0)
        g = gens[i]
        gens_g = gens.copy()
        gens_g[i] = 0
        strict = []
        non_strict = []

        for r, x in zip(diag(*A[:, i])**-1*(b - A*gens_g), c):
            non_strict.append(r) if x else strict.append(r)

        pos = int(A[0, i] > 0)
        other_op = Min if pos else Max

        if strict and non_strict:
            a, b = other_op(*non_strict), other_op(*strict)
            opn, ops = op_map[(pos, 1)], op_map[(pos, 0)]
            res.append(Or(And(opn(g, a), ops(a, b)), And(ops(g, b), opn(b, a))))
        else:
            both = non_strict + strict
            res.append(op_map[(pos, int(strict == []))](g, other_op(*(both))))
    elif any(_ < 0 for _ in b):
        return false

    return And(*res)
{'fraction_non_alphanumeric': 0.16461232604373757, 'fraction_numerical': 0.013817097415506959, 'mean_word_length': 2.0985525100092395, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 50, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4128191', 'n_tokens_mistral': 3896, 'n_tokens_neox': 3652, 'n_words': 1112}