ronantakizawa/codereview-bench huggingface dataset:
Repository: sympy/sympy
File: sympy/polys/densebasic.py (Python)

Code before:
    True

    """
    return K.is_negative(dmp_ground_LC(f, u, K))


def dmp_positive_p(f: dmp[Er], u: int, K: Domain[Er]) -> bool:
    """
    Return ``True`` if ``LC(f)`` is positive.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dmp_positive_p

    >>> dmp_positive_p([[ZZ(1)], [-ZZ(1)]], 1, ZZ)
    True
    >>> dmp_positive_p([[-ZZ(1)], [ZZ(1)]], 1, ZZ)
    False

    """
    return K.is_positive(dmp_ground_LC(f, u, K))


def dup_from_dict(f: dict[tuple[int], Er] | dict[int, Er], K: Domain[Er]) -> dup[Er]:
    """
    Create a ``K[x]`` polynomial from a ``dict``.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dup_from_dict

    >>> dup_from_dict({(0,): ZZ(7), (2,): ZZ(5), (4,): ZZ(1)}, ZZ)
    [1, 0, 5, 0, 7]
    >>> dup_from_dict({}, ZZ)
    []

    """
    if not f:
        return []

    n, h = max(f.keys()), []

    if isinstance(n, int):
        for k in range(n, -1, -1):
            h.append(f.get(k, K.zero))  # type: ignore
    else:
        (n,) = n

Review comment (suggestion):
This change is the whole purpose of this PR. The type here should be well defined but enforcing that propagates outwards.

Code after:
    True

    """
    return K.is_negative(dmp_ground_LC(f, u, K))


def dmp_positive_p(f: dmp[Er], u: int, K: Domain[Er]) -> bool:
    """
    Return ``True`` if ``LC(f)`` is positive.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dmp_positive_p

    >>> dmp_positive_p([[ZZ(1)], [-ZZ(1)]], 1, ZZ)
    True
    >>> dmp_positive_p([[-ZZ(1)], [ZZ(1)]], 1, ZZ)
    False

    """
    return K.is_positive(dmp_ground_LC(f, u, K))


def dup_from_dict(f: dict[tuple[int], Er], K: Domain[Er]) -> dup[Er]:
    """
    Create a ``K[x]`` polynomial from a ``dict``.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dup_from_dict

    >>> dup_from_dict({(0,): ZZ(7), (2,): ZZ(5), (4,): ZZ(1)}, ZZ)
    [1, 0, 5, 0, 7]
    >>> dup_from_dict({}, ZZ)
    []

    """
    if not f:
        return []

    n, h = max(f.keys()), []

    (N,) = n

    for k in range(N, -1, -1):
        h.append(f.get((k,), K.zero))
Repository: sympy/sympy
File: sympy/polys/densebasic.py (Python)

Code before:
    if not f:
        return "0"

    deg = dup_degree(f)

    def format_term(coeff, exp):
        if coeff == 0:
            return None
        if exp == 0:
            return str(coeff)
        elif exp == 1:
            base = sym
        else:
            base = f"{sym}**{exp}"

        if coeff == 1:
            return base
        elif coeff == -1:
            return f"-{base}"
        else:
            return f"{coeff}*{base}"

    terms = [
    t for i, coeff in enumerate(f)
    if (t := format_term(coeff, deg - i)) is not None
    ]

    if ascending:
        terms.reverse()

    return " + ".join(terms).replace("+ -", "- ")


def dup_print(f: dup[Er], sym: str | Symbol, *, ascending: bool = False) -> None:
    """
    Print a polynomial in ``K[x]``.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dup_print, dup_from_list
    >>> f = dup_from_list([1, 0, 5, 0, 7], ZZ)
    >>> dup_print(f, 'x')
    x**4 + 5*x**2 + 7
    >>> dup_print(f, 'x', ascending=True)
    7 + 5*x**2 + x**4
    """
    print(dup_pretty(f, sym, ascending=ascending))


Review comment (suggestion):
When it comes out looking like this it means that it is better not to use a list comprehension and just write a normal loop.

Code after:
    dup_print
    """

    if not f:
        return "0"

    deg = dup_degree(f)

    def format_term(coeff, exp):
        if coeff == 0:
            return None
        if exp == 0:
            return str(coeff)
        elif exp == 1:
            base = sym
        else:
            base = f"{sym}**{exp}"

        if coeff == 1:
            return base
        elif coeff == -1:
            return f"-{base}"
        else:
            return f"{coeff}*{base}"

    terms = []
    for i, coeff in enumerate(f):
        t = format_term(coeff, deg - i)
        if t is not None:
            terms.append(t)

    if ascending:
        terms.reverse()

    return " + ".join(terms).replace("+ -", "- ")


def dup_print(f: dup[Er], sym: str, *, ascending: bool = False) -> None:
    """
    Print a polynomial in ``K[x]``.

    Examples
    ========

    >>> from sympy.polys.domains import ZZ
    >>> from sympy.polys.densebasic import dup_print, dup_from_list
    >>> f = dup_from_list([1, 0, 5, 0, 7], ZZ)
    >>> dup_print(f, 'x')
    x**4 + 5*x**2 + 7
    >>> dup_print(f, 'x', ascending=True)
    7 + 5*x**2 + x**4
Repository: sympy/sympy
File: sympy/logic/algorithms/z3_wrapper.py (Python)

Code before:
    uf_arity = {}

    # Handle bare function heads (symbols that are functions but not called)
    for head in expr.atoms(UndefinedFunction):
        uf_arity.setdefault(str(head), None)

    # Handle function calls like f(a), g(x,y)
    if AppliedUndef is not None:
        calls = expr.atoms(AppliedUndef)
    else:
        calls = [c for c in expr.atoms(Function) if isinstance(c.func, UndefinedFunction)]

    for call in calls:
        name = str(call.func)
        arity = len(call.args)
        prev = uf_arity.get(name)
        uf_arity[name] = arity if prev is None else max(prev or 0, arity)

    return uf_arity


def collect_all_uninterpreted_functions(enc_cnf):
    uf_table = {}
    
    for pred, enc in enc_cnf.encoding.items():
        if not is_supported_predicate(pred):
            continue
            
        pred_ufs = find_uninterpreted_functions(pred)
        # Merge with existing, taking maximum arity for each function
        for name, arity in pred_ufs.items():
            if name in uf_table:
                if uf_table[name] is None or arity is None:
                    uf_table[name] = max(uf_table[name] or 0, arity or 0)
                else:
                    uf_table[name] = max(uf_table[name], arity)
            else:
                uf_table[name] = arity
                
    return uf_table


def collect_all_free_symbols(enc_cnf):
    """Collect all free symbols from all predicates in the CNF."""
    free_symbols = set()
    
    for pred, enc in enc_cnf.encoding.items():
        if not is_supported_predicate(pred):
            continue
            
        free_symbols |= pred.free_symbols

Review comment (refactor):
You don't need a function here. This would probably be better:
```python
if not isinstance(pred, AppliedPredicate) or pred.function not in supported_predicates:
   continue
```
Single line helper functions are generally not a good idea as they make the code less readable.

Code after:
        declarations.append(f"(declare-fun {f} ({arg_types}) Real)")

    declarations = "\n".join(declarations)
    assertions = "\n".join(assertions)
    s.from_string(declarations)
    s.from_string(assertions)

    return s


known_functions = {
            Add: '+',
            Mul: '*',

            Equality: '=',
            LessThan: '<=',
            GreaterThan: '>=',
            StrictLessThan: '<',
            StrictGreaterThan: '>',

            EqualityPredicate(): '=',
            LessThanPredicate(): '<=',
            GreaterThanPredicate(): '>=',
            StrictLessThanPredicate(): '<',
            StrictGreaterThanPredicate(): '>',

            Abs: 'abs',
            Min: 'min',
            Max: 'max',
            Pow: '^',

            And: 'and',
            Or: 'or',
            Xor: 'xor',
            Not: 'not',
            ITE: 'ite',
            Implies: '=>',
        }
Repository: sympy/sympy
File: sympy/logic/tests/test_inference.py (Python)

Code before:
    z3 = import_module("z3")

    if not z3:
        skip("z3 not installed.")
    A, B, C = symbols('A,B,C')
    x, y, z = symbols('x,y,z')
    assert z3_satisfiable((x >= 2) & (x < 1)) is False
    assert z3_satisfiable( A & ~A ) is False

    model = z3_satisfiable(A & (~A | B | C))
    assert bool(model) is True
    assert model[A] is True

    # test nonlinear function
    assert z3_satisfiable((x ** 2 >= 2) & (x < 1) & (x > -1)) is False

    f = symbols('f1', cls=Function)
    model = z3_satisfiable(f(A))
    assert bool(model) is True

    f,h = symbols('f h', cls=Function)
    x,y,c2 = symbols('x y c2')

    assert z3_satisfiable(Equality(h(x, y), h(y, x))) is True
    assert z3_satisfiable(Equality(f(h(x, y)), h(f(x), f(y)))) is True
    assert z3_satisfiable(Unequality(f(c2), x)) is True

    expr = And(
        Unequality(x, y),
        Equality(f(x), f(y)),
        Unequality(h(f(x)), h(f(y)))
    )
    assert z3_satisfiable(expr) is False

    expr = And(
        Equality(x, y),
        Unequality(f(x), f(y))
    )
    assert z3_satisfiable(expr) is False


def test_z3_vs_lra_dpll2():
    z3 = import_module("z3")
    if z3 is None:
        skip("z3 not installed.")

    def boolean_formula_to_encoded_cnf(bf):
        cnf = CNF.from_prop(bf)
        enc = EncodedCNF()
        enc.from_cnf(cnf)
        return enc

Review comment (suggestion):
You should use Eq and Ne which you can import from `from sympy.core.relational`

Code after:


def test_z3():
    z3 = import_module("z3")

    if not z3:
        skip("z3 not installed.")
    A, B, C = symbols('A,B,C')
    x, y, z = symbols('x,y,z')
    assert z3_satisfiable((x >= 2) & (x < 1)) is False
    assert z3_satisfiable( A & ~A ) is False

    model = z3_satisfiable(A & (~A | B | C))
    assert bool(model) is True
    assert model[A] is True

    # test nonlinear function
    assert z3_satisfiable((x ** 2 >= 2) & (x < 1) & (x > -1)) is False

    f = symbols('f1', cls=Function)
    model = z3_satisfiable(f(A))
    assert bool(model) is True

    f,h = symbols('f h', cls=Function)
    x,y,c2 = symbols('x y c2')

    assert z3_satisfiable(Eq(h(x, y), h(y, x))) == {Q.eq(h(x, y), h(y, x)): True}

    expr = And(
        Ne(x, y),
        Eq(f(x), f(y)),
        Ne(h(f(x)), h(f(y)))
    )
    assert z3_satisfiable(expr) is False

    expr = And(
        Eq(x, y),
        Ne(f(x), f(y))
    )
    assert z3_satisfiable(expr) is False


def test_z3_vs_lra_dpll2():
    z3 = import_module("z3")
    if z3 is None:
        skip("z3 not installed.")

    def boolean_formula_to_encoded_cnf(bf):
        cnf = CNF.from_prop(bf)
        enc = EncodedCNF()
        enc.from_cnf(cnf)
Repository: sympy/sympy
File: sympy/integrals/tests/test_failing_integrals.py (Python)

Code before:
    assert not i.has(Integral)
    # assert i == -5*zeta(3)/4


@XFAIL
@slow
def test_issue_14716():
    i = integrate(log(x + 5)*cos(pi*x),(x, S.Half, 1))
    assert not i.has(Integral)
    # Mathematica can not solve it either, but
    # integrate(log(x + 5)*cos(pi*x),(x, S.Half, 1)).transform(x, y - 5).doit()
    # works
    # assert i == -log(Rational(11, 2))/pi - Si(pi*Rational(11, 2))/pi + Si(6*pi)/pi


@XFAIL
def test_issue_14709a():
    i = integrate(x*acos(1 - 2*x/h), (x, 0, h))
    assert not i.has(Integral)
    # assert i == 5*h**2*pi/16


@slow
@XFAIL
def test_issue_14398():
    assert not integrate(exp(x**2)*cos(x), x).has(Integral)


@XFAIL
def test_issue_14074():
    i = integrate(log(sin(x)), (x, 0, pi/2))
    assert not i.has(Integral)
    # assert i == -pi*log(2)/2


@XFAIL
@slow
def test_issue_14078b():
    i = integrate((atan(4*x)-atan(2*x))/x, (x, 0, oo))
    assert not i.has(Integral)
    # assert i == pi*log(2)/2


@XFAIL
def test_issue_13792():
    i =  integrate(log(1/x) / (1 - x), (x, 0, 1))
    assert not i.has(Integral)
    # assert i in [polylog(2, -exp_polar(I*pi)), pi**2/6]


@XFAIL

Review comment (suggestion):
This doesn't seem to be passing now:
```python
In [1]: integrate(exp(x**2)*cos(x), x)
Out[1]: 
⌠                
⎮  ⎛ 2⎞          
⎮  ⎝x ⎠          
⎮ ℯ    ⋅cos(x) dx
⌡  
```

Code after:
def test_issue_14716():
    i = integrate(log(x + 5)*cos(pi*x),(x, S.Half, 1))
    assert not i.has(Integral)
    # Mathematica can not solve it either, but
    # integrate(log(x + 5)*cos(pi*x),(x, S.Half, 1)).transform(x, y - 5).doit()
    # works
    # assert i == -log(Rational(11, 2))/pi - Si(pi*Rational(11, 2))/pi + Si(6*pi)/pi


@XFAIL
def test_issue_14709a():
    i = integrate(x*acos(1 - 2*x/h), (x, 0, h))
    assert not i.has(Integral)
    # assert i == 5*h**2*pi/16


@XFAIL
def test_issue_14074():
    i = integrate(log(sin(x)), (x, 0, pi/2))
    assert not i.has(Integral)
    # assert i == -pi*log(2)/2


@XFAIL
@slow
def test_issue_14078b():
    i = integrate((atan(4*x)-atan(2*x))/x, (x, 0, oo))
    assert not i.has(Integral)
    # assert i == pi*log(2)/2


@XFAIL
def test_issue_13792():
    i =  integrate(log(1/x) / (1 - x), (x, 0, 1))
    assert not i.has(Integral)
    # assert i in [polylog(2, -exp_polar(I*pi)), pi**2/6]


@XFAIL
def test_issue_11845a():
    assert not integrate(exp(y - x**3), (x, 0, 1)).has(Integral)


@XFAIL
def test_issue_11845b():
    assert not integrate(exp(-y - x**3), (x, 0, 1)).has(Integral)


@XFAIL
def test_issue_11813():
    assert not integrate((a - x)**Rational(-1, 2)*x, (x, 0, a)).has(Integral)
Repository: sympy/sympy
File: sympy/core/mul.py (Python)

Code before:
from __future__ import annotations
from typing import TYPE_CHECKING, ClassVar, overload, Literal

from collections import defaultdict
from functools import reduce
from itertools import product
import operator

from .sympify import sympify
from .basic import Basic, _args_sortkey
from .singleton import S
from .operations import AssocOp, AssocOpDispatcher
from .cache import cacheit
from .intfunc import integer_nthroot, trailing
from .logic import fuzzy_not, _fuzzy_group
from .expr import Expr
from .parameters import global_parameters
from .kind import KindDispatcher
from .traversal import bottom_up
from sympy.utilities.iterables import sift

if TYPE_CHECKING:
    from .numbers import Number

# internal marker to indicate:
#   "there are still non-commutative objects -- don't forget to process them"
class NC_Marker:
    is_Order = False
    is_Mul = False
    is_Number = False
    is_Poly = False

    is_commutative = False


def _mulsort(args):
    # in-place sorting of args
    args.sort(key=_args_sortkey)


def _unevaluated_Mul(*args):
    """Return a well-formed unevaluated Mul: Numbers are collected and
    put in slot 0, any arguments that are Muls will be flattened, and args
    are sorted. Use this when args have changed but you still want to return
    an unevaluated Mul.

    Examples
    ========

    >>> from sympy.core.mul import _unevaluated_Mul as uMul

Review comment (suggestion):
There should be two blank lines above and below. Generally at top-level things should be separated by two blank lines.

Code after:
from __future__ import annotations
from typing import TYPE_CHECKING, ClassVar, overload, Literal

from collections import defaultdict
from functools import reduce
from itertools import product
import operator

from .sympify import sympify
from .basic import Basic, _args_sortkey
from .singleton import S
from .operations import AssocOp, AssocOpDispatcher
from .cache import cacheit
from .intfunc import integer_nthroot, trailing
from .logic import fuzzy_not, _fuzzy_group
from .expr import Expr
from .parameters import global_parameters
from .kind import KindDispatcher
from .traversal import bottom_up
from sympy.utilities.iterables import sift


if TYPE_CHECKING:
    from .numbers import Number


# internal marker to indicate:
#   "there are still non-commutative objects -- don't forget to process them"
class NC_Marker:
    is_Order = False
    is_Mul = False
    is_Number = False
    is_Poly = False

    is_commutative = False


def _mulsort(args):
    # in-place sorting of args
    args.sort(key=_args_sortkey)


def _unevaluated_Mul(*args):
    """Return a well-formed unevaluated Mul: Numbers are collected and
    put in slot 0, any arguments that are Muls will be flattened, and args
    are sorted. Use this when args have changed but you still want to return
    an unevaluated Mul.

    Examples
    ========
Repository: sympy/sympy
File: sympy/polys/rootconditions.py (Python)

Code before:
    for all ``i``.

    References
    ==========

    .. [1] https://faculty.washington.edu/chx/teaching/me547/2_1_stability.pdf#:~:text=2.6%20Routh,plane%20Real

    """
    if not f:
        raise ValueError("zero polynomial")

    excluded_domains = [EX, EXRAW]
    if not K in excluded_domains and I in K:
        raise NotImplementedError(
            "Schur conditions is not implemented for complex domains"
        )

    # Check if -1 is a root, since the transformation is not defined in this case
    evaluation = K.to_sympy(dup_eval(f, -K.one, K))
    if evaluation.is_Number:
        if K not in excluded_domains and K.is_Exact:
            if K.is_zero(K.from_sympy(evaluation)):
                return [-K.one]
        else:
            if math.isclose(evaluation, 0.0):
                return [-K.one]

    if not K.is_Exact:
        K_exact = K.get_exact()
        pe = dup_convert(f, K, K_exact)
        p_transformed: list = dup_transform(pe, [K_exact.one, K_exact.one],
                                    [-K_exact.one, K_exact.one], K_exact)
        conds: list = dup_routh_hurwitz(p_transformed, K_exact)

        return [K.convert_from(c, K_exact) for c in conds]

    p_transformed = dup_transform(f, [K.one, K.one], [-K.one, K.one], K)
    return dup_routh_hurwitz(p_transformed, K)


Review comment (suggestion):
Maybe this should be replaced with a check that `x + 1` divides the polynomial with no remainder.

Code after:
    References
    ==========

    .. [1] https://faculty.washington.edu/chx/teaching/me547/2_1_stability.pdf#:~:text=2.6%20Routh,plane%20Real

    """
    if not f:
        raise ValueError("zero polynomial")

    excluded_domains = [EX, EXRAW]
    if not K in excluded_domains and I in K:
        raise NotImplementedError(
            "Schur conditions is not implemented for complex domains"
        )

    if K.is_Exact:
        return _dup_schur_conditions(f, K)
    else:
        K_exact = K.get_exact()
        pe = dup_convert(f, K, K_exact)

        conds = _dup_schur_conditions(pe, K_exact)
        return [K.convert_from(c, K_exact) for c in conds]


def _dup_schur_conditions(f: dup[Er], K: Domain[Er]) -> list[Er]:
    """
    Computes the Schur stability conditions, mapping the unit circle to the left
    half plane, transforming the problem into a Routh-Hurwitz stability problem.

    The transformation is done via ``z = (1 + s)/(1 - s)`` to the polynomial
    ``f``.

    """
    # Check if -1 is a root, since the transformation is not defined in this case
    if K.is_zero(dup_eval(f, -K.one, K)):
        return [-K.one]

    f_t = dup_transform(f, [K.one, K.one], [-K.one, K.one], K)
    return dup_routh_hurwitz(f_t, K)
Repository: sympy/sympy
File: sympy/polys/rootconditions.py (Python)

Code before:
    if not f:
        raise ValueError("zero polynomial")

    excluded_domains = [EX, EXRAW]
    if not K in excluded_domains and I in K:
        raise NotImplementedError(
            "Schur conditions is not implemented for complex domains"
        )

    if not K.is_Exact:
        K_exact = K.get_exact()
        pe = dup_convert(f, K, K_exact)

        # Check if -1 is a root, since the transformation is not defined in this case
        if K_exact.is_zero(dup_eval(pe, -K_exact.one, K_exact)):
                    return [-K.one]

        conds: list = dup_routh_hurwitz(_schur_to_hurwitz(pe, K_exact), K_exact)

        return [K.convert_from(c, K_exact) for c in conds]

    # Check if -1 is a root, since the transformation is not defined in this case
    if K.is_zero(dup_eval(f, -K.one, K)):
                return [-K.one]

    return dup_routh_hurwitz(_schur_to_hurwitz(f, K), K)


def _schur_to_hurwitz(f: dup[Er], K: Domain[Er]) -> dup[Er]:
    """
    Apply the bilinear transformation ``z = (1 + s)/(1 - s)`` to the
    polynomial ``f`` in order to map the unit circle to the left half plane,
    transforming the problem of Schur stability to the problem of Routh-Hurwitz
    stability.

    Note
    ====
    The transformation is not defined if -1 is a root of the polynomial.

    """

    return dup_transform(f, [K.one, K.one], [-K.one, K.one], K)


Review comment (suggestion):
The code here is poorly organised.

It would be better to write this as:
```
if K.is_Exact:
    return _dup_schur_conditions(...)
else:
    pe = dup_convert(f, K, K_exact)
    conds = _dup_schur_conditions(...)
    return [...]
```

Code after:
        )

    if K.is_Exact:
        return _dup_schur_conditions(f, K)
    else:
        K_exact = K.get_exact()
        pe = dup_convert(f, K, K_exact)

        conds = _dup_schur_conditions(pe, K_exact)
        return [K.convert_from(c, K_exact) for c in conds]


def _dup_schur_conditions(f: dup[Er], K: Domain[Er]) -> list[Er]:
    """
    Computes the Schur stability conditions, mapping the unit circle to the left
    half plane, transforming the problem into a Routh-Hurwitz stability problem.

    The transformation is done via ``z = (1 + s)/(1 - s)`` to the polynomial
    ``f``.

    """
    # Check if -1 is a root, since the transformation is not defined in this case
    if K.is_zero(dup_eval(f, -K.one, K)):
        return [-K.one]

    f_t = dup_transform(f, [K.one, K.one], [-K.one, K.one], K)
    return dup_routh_hurwitz(f_t, K)