Add files using upload-large-folder tool

lib/python3.12/site-packages/sympy/assumptions/__init__.py

@@ -0,0 +1,18 @@
+"""
+A module to implement logical predicates and assumption system.
+"""
+
+from .assume import (
+    AppliedPredicate, Predicate, AssumptionsContext, assuming,
+    global_assumptions
+)
+from .ask import Q, ask, register_handler, remove_handler
+from .refine import refine
+from .relation import BinaryRelation, AppliedBinaryRelation
+
+__all__ = [
+    'AppliedPredicate', 'Predicate', 'AssumptionsContext', 'assuming',
+    'global_assumptions', 'Q', 'ask', 'register_handler', 'remove_handler',
+    'refine',
+    'BinaryRelation', 'AppliedBinaryRelation'
+]

lib/python3.12/site-packages/sympy/assumptions/ask.py

@@ -0,0 +1,651 @@
+"""Module for querying SymPy objects about assumptions."""
+
+from sympy.assumptions.assume import (global_assumptions, Predicate,
+        AppliedPredicate)
+from sympy.assumptions.cnf import CNF, EncodedCNF, Literal
+from sympy.core import sympify
+from sympy.core.kind import BooleanKind
+from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le
+from sympy.logic.inference import satisfiable
+from sympy.utilities.decorator import memoize_property
+from sympy.utilities.exceptions import (sympy_deprecation_warning,
+                                        SymPyDeprecationWarning,
+                                        ignore_warnings)
+
+
+# Memoization is necessary for the properties of AssumptionKeys to
+# ensure that only one object of Predicate objects are created.
+# This is because assumption handlers are registered on those objects.
+
+
+class AssumptionKeys:
+    """
+    This class contains all the supported keys by ``ask``.
+    It should be accessed via the instance ``sympy.Q``.
+
+    """
+
+    # DO NOT add methods or properties other than predicate keys.
+    # SAT solver checks the properties of Q and use them to compute the
+    # fact system. Non-predicate attributes will break this.
+
+    @memoize_property
+    def hermitian(self):
+        from .handlers.sets import HermitianPredicate
+        return HermitianPredicate()
+
+    @memoize_property
+    def antihermitian(self):
+        from .handlers.sets import AntihermitianPredicate
+        return AntihermitianPredicate()
+
+    @memoize_property
+    def real(self):
+        from .handlers.sets import RealPredicate
+        return RealPredicate()
+
+    @memoize_property
+    def extended_real(self):
+        from .handlers.sets import ExtendedRealPredicate
+        return ExtendedRealPredicate()
+
+    @memoize_property
+    def imaginary(self):
+        from .handlers.sets import ImaginaryPredicate
+        return ImaginaryPredicate()
+
+    @memoize_property
+    def complex(self):
+        from .handlers.sets import ComplexPredicate
+        return ComplexPredicate()
+
+    @memoize_property
+    def algebraic(self):
+        from .handlers.sets import AlgebraicPredicate
+        return AlgebraicPredicate()
+
+    @memoize_property
+    def transcendental(self):
+        from .predicates.sets import TranscendentalPredicate
+        return TranscendentalPredicate()
+
+    @memoize_property
+    def integer(self):
+        from .handlers.sets import IntegerPredicate
+        return IntegerPredicate()
+
+    @memoize_property
+    def noninteger(self):
+        from .predicates.sets import NonIntegerPredicate
+        return NonIntegerPredicate()
+
+    @memoize_property
+    def rational(self):
+        from .handlers.sets import RationalPredicate
+        return RationalPredicate()
+
+    @memoize_property
+    def irrational(self):
+        from .handlers.sets import IrrationalPredicate
+        return IrrationalPredicate()
+
+    @memoize_property
+    def finite(self):
+        from .handlers.calculus import FinitePredicate
+        return FinitePredicate()
+
+    @memoize_property
+    def infinite(self):
+        from .handlers.calculus import InfinitePredicate
+        return InfinitePredicate()
+
+    @memoize_property
+    def positive_infinite(self):
+        from .handlers.calculus import PositiveInfinitePredicate
+        return PositiveInfinitePredicate()
+
+    @memoize_property
+    def negative_infinite(self):
+        from .handlers.calculus import NegativeInfinitePredicate
+        return NegativeInfinitePredicate()
+
+    @memoize_property
+    def positive(self):
+        from .handlers.order import PositivePredicate
+        return PositivePredicate()
+
+    @memoize_property
+    def negative(self):
+        from .handlers.order import NegativePredicate
+        return NegativePredicate()
+
+    @memoize_property
+    def zero(self):
+        from .handlers.order import ZeroPredicate
+        return ZeroPredicate()
+
+    @memoize_property
+    def extended_positive(self):
+        from .handlers.order import ExtendedPositivePredicate
+        return ExtendedPositivePredicate()
+
+    @memoize_property
+    def extended_negative(self):
+        from .handlers.order import ExtendedNegativePredicate
+        return ExtendedNegativePredicate()
+
+    @memoize_property
+    def nonzero(self):
+        from .handlers.order import NonZeroPredicate
+        return NonZeroPredicate()
+
+    @memoize_property
+    def nonpositive(self):
+        from .handlers.order import NonPositivePredicate
+        return NonPositivePredicate()
+
+    @memoize_property
+    def nonnegative(self):
+        from .handlers.order import NonNegativePredicate
+        return NonNegativePredicate()
+
+    @memoize_property
+    def extended_nonzero(self):
+        from .handlers.order import ExtendedNonZeroPredicate
+        return ExtendedNonZeroPredicate()
+
+    @memoize_property
+    def extended_nonpositive(self):
+        from .handlers.order import ExtendedNonPositivePredicate
+        return ExtendedNonPositivePredicate()
+
+    @memoize_property
+    def extended_nonnegative(self):
+        from .handlers.order import ExtendedNonNegativePredicate
+        return ExtendedNonNegativePredicate()
+
+    @memoize_property
+    def even(self):
+        from .handlers.ntheory import EvenPredicate
+        return EvenPredicate()
+
+    @memoize_property
+    def odd(self):
+        from .handlers.ntheory import OddPredicate
+        return OddPredicate()
+
+    @memoize_property
+    def prime(self):
+        from .handlers.ntheory import PrimePredicate
+        return PrimePredicate()
+
+    @memoize_property
+    def composite(self):
+        from .handlers.ntheory import CompositePredicate
+        return CompositePredicate()
+
+    @memoize_property
+    def commutative(self):
+        from .handlers.common import CommutativePredicate
+        return CommutativePredicate()
+
+    @memoize_property
+    def is_true(self):
+        from .handlers.common import IsTruePredicate
+        return IsTruePredicate()
+
+    @memoize_property
+    def symmetric(self):
+        from .handlers.matrices import SymmetricPredicate
+        return SymmetricPredicate()
+
+    @memoize_property
+    def invertible(self):
+        from .handlers.matrices import InvertiblePredicate
+        return InvertiblePredicate()
+
+    @memoize_property
+    def orthogonal(self):
+        from .handlers.matrices import OrthogonalPredicate
+        return OrthogonalPredicate()
+
+    @memoize_property
+    def unitary(self):
+        from .handlers.matrices import UnitaryPredicate
+        return UnitaryPredicate()
+
+    @memoize_property
+    def positive_definite(self):
+        from .handlers.matrices import PositiveDefinitePredicate
+        return PositiveDefinitePredicate()
+
+    @memoize_property
+    def upper_triangular(self):
+        from .handlers.matrices import UpperTriangularPredicate
+        return UpperTriangularPredicate()
+
+    @memoize_property
+    def lower_triangular(self):
+        from .handlers.matrices import LowerTriangularPredicate
+        return LowerTriangularPredicate()
+
+    @memoize_property
+    def diagonal(self):
+        from .handlers.matrices import DiagonalPredicate
+        return DiagonalPredicate()
+
+    @memoize_property
+    def fullrank(self):
+        from .handlers.matrices import FullRankPredicate
+        return FullRankPredicate()
+
+    @memoize_property
+    def square(self):
+        from .handlers.matrices import SquarePredicate
+        return SquarePredicate()
+
+    @memoize_property
+    def integer_elements(self):
+        from .handlers.matrices import IntegerElementsPredicate
+        return IntegerElementsPredicate()
+
+    @memoize_property
+    def real_elements(self):
+        from .handlers.matrices import RealElementsPredicate
+        return RealElementsPredicate()
+
+    @memoize_property
+    def complex_elements(self):
+        from .handlers.matrices import ComplexElementsPredicate
+        return ComplexElementsPredicate()
+
+    @memoize_property
+    def singular(self):
+        from .predicates.matrices import SingularPredicate
+        return SingularPredicate()
+
+    @memoize_property
+    def normal(self):
+        from .predicates.matrices import NormalPredicate
+        return NormalPredicate()
+
+    @memoize_property
+    def triangular(self):
+        from .predicates.matrices import TriangularPredicate
+        return TriangularPredicate()
+
+    @memoize_property
+    def unit_triangular(self):
+        from .predicates.matrices import UnitTriangularPredicate
+        return UnitTriangularPredicate()
+
+    @memoize_property
+    def eq(self):
+        from .relation.equality import EqualityPredicate
+        return EqualityPredicate()
+
+    @memoize_property
+    def ne(self):
+        from .relation.equality import UnequalityPredicate
+        return UnequalityPredicate()
+
+    @memoize_property
+    def gt(self):
+        from .relation.equality import StrictGreaterThanPredicate
+        return StrictGreaterThanPredicate()
+
+    @memoize_property
+    def ge(self):
+        from .relation.equality import GreaterThanPredicate
+        return GreaterThanPredicate()
+
+    @memoize_property
+    def lt(self):
+        from .relation.equality import StrictLessThanPredicate
+        return StrictLessThanPredicate()
+
+    @memoize_property
+    def le(self):
+        from .relation.equality import LessThanPredicate
+        return LessThanPredicate()
+
+
+Q = AssumptionKeys()
+
+def _extract_all_facts(assump, exprs):
+    """
+    Extract all relevant assumptions from *assump* with respect to given *exprs*.
+
+    Parameters
+    ==========
+
+    assump : sympy.assumptions.cnf.CNF
+
+    exprs : tuple of expressions
+
+    Returns
+    =======
+
+    sympy.assumptions.cnf.CNF
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import CNF
+    >>> from sympy.assumptions.ask import _extract_all_facts
+    >>> from sympy.abc import x, y
+    >>> assump = CNF.from_prop(Q.positive(x) & Q.integer(y))
+    >>> exprs = (x,)
+    >>> cnf = _extract_all_facts(assump, exprs)
+    >>> cnf.clauses
+    {frozenset({Literal(Q.positive, False)})}
+
+    """
+    facts = set()
+
+    for clause in assump.clauses:
+        args = []
+        for literal in clause:
+            if isinstance(literal.lit, AppliedPredicate) and len(literal.lit.arguments) == 1:
+                if literal.lit.arg in exprs:
+                    # Add literal if it has matching in it
+                    args.append(Literal(literal.lit.function, literal.is_Not))
+                else:
+                    # If any of the literals doesn't have matching expr don't add the whole clause.
+                    break
+            else:
+                # If any of the literals aren't unary predicate don't add the whole clause.
+                break
+
+        else:
+            if args:
+                facts.add(frozenset(args))
+    return CNF(facts)
+
+
+def ask(proposition, assumptions=True, context=global_assumptions):
+    """
+    Function to evaluate the proposition with assumptions.
+
+    Explanation
+    ===========
+
+    This function evaluates the proposition to ``True`` or ``False`` if
+    the truth value can be determined. If not, it returns ``None``.
+
+    It should be discerned from :func:`~.refine()` which, when applied to a
+    proposition, simplifies the argument to symbolic ``Boolean`` instead of
+    Python built-in ``True``, ``False`` or ``None``.
+
+    **Syntax**
+
+        * ask(proposition)
+            Evaluate the *proposition* in global assumption context.
+
+        * ask(proposition, assumptions)
+            Evaluate the *proposition* with respect to *assumptions* in
+            global assumption context.
+
+    Parameters
+    ==========
+
+    proposition : Boolean
+        Proposition which will be evaluated to boolean value. If this is
+        not ``AppliedPredicate``, it will be wrapped by ``Q.is_true``.
+
+    assumptions : Boolean, optional
+        Local assumptions to evaluate the *proposition*.
+
+    context : AssumptionsContext, optional
+        Default assumptions to evaluate the *proposition*. By default,
+        this is ``sympy.assumptions.global_assumptions`` variable.
+
+    Returns
+    =======
+
+    ``True``, ``False``, or ``None``
+
+    Raises
+    ======
+
+    TypeError : *proposition* or *assumptions* is not valid logical expression.
+
+    ValueError : assumptions are inconsistent.
+
+    Examples
+    ========
+
+    >>> from sympy import ask, Q, pi
+    >>> from sympy.abc import x, y
+    >>> ask(Q.rational(pi))
+    False
+    >>> ask(Q.even(x*y), Q.even(x) & Q.integer(y))
+    True
+    >>> ask(Q.prime(4*x), Q.integer(x))
+    False
+
+    If the truth value cannot be determined, ``None`` will be returned.
+
+    >>> print(ask(Q.odd(3*x))) # cannot determine unless we know x
+    None
+
+    ``ValueError`` is raised if assumptions are inconsistent.
+
+    >>> ask(Q.integer(x), Q.even(x) & Q.odd(x))
+    Traceback (most recent call last):
+      ...
+    ValueError: inconsistent assumptions Q.even(x) & Q.odd(x)
+
+    Notes
+    =====
+
+    Relations in assumptions are not implemented (yet), so the following
+    will not give a meaningful result.
+
+    >>> ask(Q.positive(x), x > 0)
+
+    It is however a work in progress.
+
+    See Also
+    ========
+
+    sympy.assumptions.refine.refine : Simplification using assumptions.
+        Proposition is not reduced to ``None`` if the truth value cannot
+        be determined.
+    """
+    from sympy.assumptions.satask import satask
+    from sympy.assumptions.lra_satask import lra_satask
+    from sympy.logic.algorithms.lra_theory import UnhandledInput
+
+    proposition = sympify(proposition)
+    assumptions = sympify(assumptions)
+
+    if isinstance(proposition, Predicate) or proposition.kind is not BooleanKind:
+        raise TypeError("proposition must be a valid logical expression")
+
+    if isinstance(assumptions, Predicate) or assumptions.kind is not BooleanKind:
+        raise TypeError("assumptions must be a valid logical expression")
+
+    binrelpreds = {Eq: Q.eq, Ne: Q.ne, Gt: Q.gt, Lt: Q.lt, Ge: Q.ge, Le: Q.le}
+    if isinstance(proposition, AppliedPredicate):
+        key, args = proposition.function, proposition.arguments
+    elif proposition.func in binrelpreds:
+        key, args = binrelpreds[type(proposition)], proposition.args
+    else:
+        key, args = Q.is_true, (proposition,)
+
+    # convert local and global assumptions to CNF
+    assump_cnf = CNF.from_prop(assumptions)
+    assump_cnf.extend(context)
+
+    # extract the relevant facts from assumptions with respect to args
+    local_facts = _extract_all_facts(assump_cnf, args)
+
+    # convert default facts and assumed facts to encoded CNF
+    known_facts_cnf = get_all_known_facts()
+    enc_cnf = EncodedCNF()
+    enc_cnf.from_cnf(CNF(known_facts_cnf))
+    enc_cnf.add_from_cnf(local_facts)
+
+    # check the satisfiability of given assumptions
+    if local_facts.clauses and satisfiable(enc_cnf) is False:
+        raise ValueError("inconsistent assumptions %s" % assumptions)
+
+    # quick computation for single fact
+    res = _ask_single_fact(key, local_facts)
+    if res is not None:
+        return res
+
+    # direct resolution method, no logic
+    res = key(*args)._eval_ask(assumptions)
+    if res is not None:
+        return bool(res)
+
+    # using satask (still costly)
+    res = satask(proposition, assumptions=assumptions, context=context)
+    if res is not None:
+        return res
+
+    try:
+        res = lra_satask(proposition, assumptions=assumptions, context=context)
+    except UnhandledInput:
+        return None
+
+    return res
+
+
+def _ask_single_fact(key, local_facts):
+    """
+    Compute the truth value of single predicate using assumptions.
+
+    Parameters
+    ==========
+
+    key : sympy.assumptions.assume.Predicate
+        Proposition predicate.
+
+    local_facts : sympy.assumptions.cnf.CNF
+        Local assumption in CNF form.
+
+    Returns
+    =======
+
+    ``True``, ``False`` or ``None``
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import CNF
+    >>> from sympy.assumptions.ask import _ask_single_fact
+
+    If prerequisite of proposition is rejected by the assumption,
+    return ``False``.
+
+    >>> key, assump = Q.zero, ~Q.zero
+    >>> local_facts = CNF.from_prop(assump)
+    >>> _ask_single_fact(key, local_facts)
+    False
+    >>> key, assump = Q.zero, ~Q.even
+    >>> local_facts = CNF.from_prop(assump)
+    >>> _ask_single_fact(key, local_facts)
+    False
+
+    If assumption implies the proposition, return ``True``.
+
+    >>> key, assump = Q.even, Q.zero
+    >>> local_facts = CNF.from_prop(assump)
+    >>> _ask_single_fact(key, local_facts)
+    True
+
+    If proposition rejects the assumption, return ``False``.
+
+    >>> key, assump = Q.even, Q.odd
+    >>> local_facts = CNF.from_prop(assump)
+    >>> _ask_single_fact(key, local_facts)
+    False
+    """
+    if local_facts.clauses:
+
+        known_facts_dict = get_known_facts_dict()
+
+        if len(local_facts.clauses) == 1:
+            cl, = local_facts.clauses
+            if len(cl) == 1:
+                f, = cl
+                prop_facts = known_facts_dict.get(key, None)
+                prop_req = prop_facts[0] if prop_facts is not None else set()
+                if f.is_Not and f.arg in prop_req:
+                    # the prerequisite of proposition is rejected
+                    return False
+
+        for clause in local_facts.clauses:
+            if len(clause) == 1:
+                f, = clause
+                prop_facts = known_facts_dict.get(f.arg, None) if not f.is_Not else None
+                if prop_facts is None:
+                    continue
+
+                prop_req, prop_rej = prop_facts
+                if key in prop_req:
+                    # assumption implies the proposition
+                    return True
+                elif key in prop_rej:
+                    # proposition rejects the assumption
+                    return False
+
+    return None
+
+
+def register_handler(key, handler):
+    """
+    Register a handler in the ask system. key must be a string and handler a
+    class inheriting from AskHandler.
+
+    .. deprecated:: 1.8.
+        Use multipledispatch handler instead. See :obj:`~.Predicate`.
+
+    """
+    sympy_deprecation_warning(
+        """
+        The AskHandler system is deprecated. The register_handler() function
+        should be replaced with the multipledispatch handler of Predicate.
+        """,
+        deprecated_since_version="1.8",
+        active_deprecations_target='deprecated-askhandler',
+    )
+    if isinstance(key, Predicate):
+        key = key.name.name
+    Qkey = getattr(Q, key, None)
+    if Qkey is not None:
+        Qkey.add_handler(handler)
+    else:
+        setattr(Q, key, Predicate(key, handlers=[handler]))
+
+
+def remove_handler(key, handler):
+    """
+    Removes a handler from the ask system.
+
+    .. deprecated:: 1.8.
+        Use multipledispatch handler instead. See :obj:`~.Predicate`.
+
+    """
+    sympy_deprecation_warning(
+        """
+        The AskHandler system is deprecated. The remove_handler() function
+        should be replaced with the multipledispatch handler of Predicate.
+        """,
+        deprecated_since_version="1.8",
+        active_deprecations_target='deprecated-askhandler',
+    )
+    if isinstance(key, Predicate):
+        key = key.name.name
+    # Don't show the same warning again recursively
+    with ignore_warnings(SymPyDeprecationWarning):
+        getattr(Q, key).remove_handler(handler)
+
+
+from sympy.assumptions.ask_generated import (get_all_known_facts,
+    get_known_facts_dict)

lib/python3.12/site-packages/sympy/assumptions/ask_generated.py

@@ -0,0 +1,352 @@
+"""
+Do NOT manually edit this file.
+Instead, run ./bin/ask_update.py.
+"""
+
+from sympy.assumptions.ask import Q
+from sympy.assumptions.cnf import Literal
+from sympy.core.cache import cacheit
+
+@cacheit
+def get_all_known_facts():
+    """
+    Known facts between unary predicates as CNF clauses.
+    """
+    return {
+        frozenset((Literal(Q.algebraic, False), Literal(Q.imaginary, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.negative, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.positive, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.rational, True))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.transcendental, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.algebraic, True), Literal(Q.finite, False))),
+        frozenset((Literal(Q.algebraic, True), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.antihermitian, False), Literal(Q.hermitian, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.antihermitian, False), Literal(Q.imaginary, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.finite, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.infinite, True))),
+        frozenset((Literal(Q.complex_elements, False), Literal(Q.real_elements, True))),
+        frozenset((Literal(Q.composite, False), Literal(Q.even, True), Literal(Q.positive, True), Literal(Q.prime, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.even, False), Literal(Q.odd, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.positive, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.prime, True))),
+        frozenset((Literal(Q.diagonal, False), Literal(Q.lower_triangular, True), Literal(Q.upper_triangular, True))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.lower_triangular, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.normal, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.symmetric, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.upper_triangular, False))),
+        frozenset((Literal(Q.even, False), Literal(Q.odd, False), Literal(Q.prime, True))),
+        frozenset((Literal(Q.even, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.even, True), Literal(Q.odd, True))),
+        frozenset((Literal(Q.even, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.finite, False), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.finite, True), Literal(Q.infinite, True))),
+        frozenset((Literal(Q.fullrank, False), Literal(Q.invertible, True))),
+        frozenset((Literal(Q.fullrank, True), Literal(Q.invertible, False), Literal(Q.square, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.negative, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.positive, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.negative, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.negative_infinite, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.integer_elements, True), Literal(Q.real_elements, False))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.positive_definite, True))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.singular, False))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.invertible, True), Literal(Q.singular, True))),
+        frozenset((Literal(Q.invertible, True), Literal(Q.square, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.negative, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.positive, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.rational, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.irrational, True), Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.zero, False))),
+        frozenset((Literal(Q.irrational, True), Literal(Q.rational, True))),
+        frozenset((Literal(Q.lower_triangular, False), Literal(Q.triangular, True), Literal(Q.upper_triangular, False))),
+        frozenset((Literal(Q.lower_triangular, True), Literal(Q.triangular, False))),
+        frozenset((Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.rational, True), Literal(Q.zero, False))),
+        frozenset((Literal(Q.negative, True), Literal(Q.negative_infinite, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.normal, False), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.normal, True), Literal(Q.square, False))),
+        frozenset((Literal(Q.odd, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.orthogonal, False), Literal(Q.real_elements, True), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.orthogonal, True), Literal(Q.positive_definite, False))),
+        frozenset((Literal(Q.orthogonal, True), Literal(Q.unitary, False))),
+        frozenset((Literal(Q.positive, False), Literal(Q.prime, True))),
+        frozenset((Literal(Q.positive, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.positive, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.positive_infinite, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.square, False), Literal(Q.symmetric, True))),
+        frozenset((Literal(Q.triangular, False), Literal(Q.unit_triangular, True))),
+        frozenset((Literal(Q.triangular, False), Literal(Q.upper_triangular, True)))
+    }
+
+@cacheit
+def get_all_known_matrix_facts():
+    """
+    Known facts between unary predicates for matrices as CNF clauses.
+    """
+    return {
+        frozenset((Literal(Q.complex_elements, False), Literal(Q.real_elements, True))),
+        frozenset((Literal(Q.diagonal, False), Literal(Q.lower_triangular, True), Literal(Q.upper_triangular, True))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.lower_triangular, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.normal, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.symmetric, False))),
+        frozenset((Literal(Q.diagonal, True), Literal(Q.upper_triangular, False))),
+        frozenset((Literal(Q.fullrank, False), Literal(Q.invertible, True))),
+        frozenset((Literal(Q.fullrank, True), Literal(Q.invertible, False), Literal(Q.square, True))),
+        frozenset((Literal(Q.integer_elements, True), Literal(Q.real_elements, False))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.positive_definite, True))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.singular, False))),
+        frozenset((Literal(Q.invertible, False), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.invertible, True), Literal(Q.singular, True))),
+        frozenset((Literal(Q.invertible, True), Literal(Q.square, False))),
+        frozenset((Literal(Q.lower_triangular, False), Literal(Q.triangular, True), Literal(Q.upper_triangular, False))),
+        frozenset((Literal(Q.lower_triangular, True), Literal(Q.triangular, False))),
+        frozenset((Literal(Q.normal, False), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.normal, True), Literal(Q.square, False))),
+        frozenset((Literal(Q.orthogonal, False), Literal(Q.real_elements, True), Literal(Q.unitary, True))),
+        frozenset((Literal(Q.orthogonal, True), Literal(Q.positive_definite, False))),
+        frozenset((Literal(Q.orthogonal, True), Literal(Q.unitary, False))),
+        frozenset((Literal(Q.square, False), Literal(Q.symmetric, True))),
+        frozenset((Literal(Q.triangular, False), Literal(Q.unit_triangular, True))),
+        frozenset((Literal(Q.triangular, False), Literal(Q.upper_triangular, True)))
+    }
+
+@cacheit
+def get_all_known_number_facts():
+    """
+    Known facts between unary predicates for numbers as CNF clauses.
+    """
+    return {
+        frozenset((Literal(Q.algebraic, False), Literal(Q.imaginary, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.negative, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.positive, True), Literal(Q.transcendental, False))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.rational, True))),
+        frozenset((Literal(Q.algebraic, False), Literal(Q.transcendental, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.algebraic, True), Literal(Q.finite, False))),
+        frozenset((Literal(Q.algebraic, True), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.antihermitian, False), Literal(Q.hermitian, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.antihermitian, False), Literal(Q.imaginary, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.finite, True))),
+        frozenset((Literal(Q.commutative, False), Literal(Q.infinite, True))),
+        frozenset((Literal(Q.composite, False), Literal(Q.even, True), Literal(Q.positive, True), Literal(Q.prime, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.even, False), Literal(Q.odd, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.positive, False))),
+        frozenset((Literal(Q.composite, True), Literal(Q.prime, True))),
+        frozenset((Literal(Q.even, False), Literal(Q.odd, False), Literal(Q.prime, True))),
+        frozenset((Literal(Q.even, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.even, True), Literal(Q.odd, True))),
+        frozenset((Literal(Q.even, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.finite, False), Literal(Q.transcendental, True))),
+        frozenset((Literal(Q.finite, True), Literal(Q.infinite, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.negative, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.positive, True))),
+        frozenset((Literal(Q.hermitian, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.negative, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.imaginary, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.negative_infinite, True))),
+        frozenset((Literal(Q.infinite, False), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.negative, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.positive, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.irrational, False), Literal(Q.rational, False), Literal(Q.zero, True))),
+        frozenset((Literal(Q.irrational, True), Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.zero, False))),
+        frozenset((Literal(Q.irrational, True), Literal(Q.rational, True))),
+        frozenset((Literal(Q.negative, False), Literal(Q.positive, False), Literal(Q.rational, True), Literal(Q.zero, False))),
+        frozenset((Literal(Q.negative, True), Literal(Q.negative_infinite, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.negative, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.positive, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.negative_infinite, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.odd, True), Literal(Q.rational, False))),
+        frozenset((Literal(Q.positive, False), Literal(Q.prime, True))),
+        frozenset((Literal(Q.positive, True), Literal(Q.positive_infinite, True))),
+        frozenset((Literal(Q.positive, True), Literal(Q.zero, True))),
+        frozenset((Literal(Q.positive_infinite, True), Literal(Q.zero, True)))
+    }
+
+@cacheit
+def get_known_facts_dict():
+    """
+    Logical relations between unary predicates as dictionary.
+
+    Each key is a predicate, and item is two groups of predicates.
+    First group contains the predicates which are implied by the key, and
+    second group contains the predicates which are rejected by the key.
+
+    """
+    return {
+        Q.algebraic: (set([Q.algebraic, Q.commutative, Q.complex, Q.finite]),
+        set([Q.infinite, Q.negative_infinite, Q.positive_infinite,
+        Q.transcendental])),
+        Q.antihermitian: (set([Q.antihermitian]), set([])),
+        Q.commutative: (set([Q.commutative]), set([])),
+        Q.complex: (set([Q.commutative, Q.complex, Q.finite]),
+        set([Q.infinite, Q.negative_infinite, Q.positive_infinite])),
+        Q.complex_elements: (set([Q.complex_elements]), set([])),
+        Q.composite: (set([Q.algebraic, Q.commutative, Q.complex, Q.composite,
+        Q.extended_nonnegative, Q.extended_nonzero,
+        Q.extended_positive, Q.extended_real, Q.finite, Q.hermitian,
+        Q.integer, Q.nonnegative, Q.nonzero, Q.positive, Q.rational,
+        Q.real]), set([Q.extended_negative, Q.extended_nonpositive,
+        Q.imaginary, Q.infinite, Q.irrational, Q.negative,
+        Q.negative_infinite, Q.nonpositive, Q.positive_infinite,
+        Q.prime, Q.transcendental, Q.zero])),
+        Q.diagonal: (set([Q.diagonal, Q.lower_triangular, Q.normal, Q.square,
+        Q.symmetric, Q.triangular, Q.upper_triangular]), set([])),
+        Q.even: (set([Q.algebraic, Q.commutative, Q.complex, Q.even,
+        Q.extended_real, Q.finite, Q.hermitian, Q.integer, Q.rational,
+        Q.real]), set([Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative_infinite, Q.odd, Q.positive_infinite,
+        Q.transcendental])),
+        Q.extended_negative: (set([Q.commutative, Q.extended_negative,
+        Q.extended_nonpositive, Q.extended_nonzero, Q.extended_real]),
+        set([Q.composite, Q.extended_nonnegative, Q.extended_positive,
+        Q.imaginary, Q.nonnegative, Q.positive, Q.positive_infinite,
+        Q.prime, Q.zero])),
+        Q.extended_nonnegative: (set([Q.commutative, Q.extended_nonnegative,
+        Q.extended_real]), set([Q.extended_negative, Q.imaginary,
+        Q.negative, Q.negative_infinite])),
+        Q.extended_nonpositive: (set([Q.commutative, Q.extended_nonpositive,
+        Q.extended_real]), set([Q.composite, Q.extended_positive,
+        Q.imaginary, Q.positive, Q.positive_infinite, Q.prime])),
+        Q.extended_nonzero: (set([Q.commutative, Q.extended_nonzero,
+        Q.extended_real]), set([Q.imaginary, Q.zero])),
+        Q.extended_positive: (set([Q.commutative, Q.extended_nonnegative,
+        Q.extended_nonzero, Q.extended_positive, Q.extended_real]),
+        set([Q.extended_negative, Q.extended_nonpositive, Q.imaginary,
+        Q.negative, Q.negative_infinite, Q.nonpositive, Q.zero])),
+        Q.extended_real: (set([Q.commutative, Q.extended_real]),
+        set([Q.imaginary])),
+        Q.finite: (set([Q.commutative, Q.finite]), set([Q.infinite,
+        Q.negative_infinite, Q.positive_infinite])),
+        Q.fullrank: (set([Q.fullrank]), set([])),
+        Q.hermitian: (set([Q.hermitian]), set([])),
+        Q.imaginary: (set([Q.antihermitian, Q.commutative, Q.complex,
+        Q.finite, Q.imaginary]), set([Q.composite, Q.even,
+        Q.extended_negative, Q.extended_nonnegative,
+        Q.extended_nonpositive, Q.extended_nonzero,
+        Q.extended_positive, Q.extended_real, Q.infinite, Q.integer,
+        Q.irrational, Q.negative, Q.negative_infinite, Q.nonnegative,
+        Q.nonpositive, Q.nonzero, Q.odd, Q.positive,
+        Q.positive_infinite, Q.prime, Q.rational, Q.real, Q.zero])),
+        Q.infinite: (set([Q.commutative, Q.infinite]), set([Q.algebraic,
+        Q.complex, Q.composite, Q.even, Q.finite, Q.imaginary,
+        Q.integer, Q.irrational, Q.negative, Q.nonnegative,
+        Q.nonpositive, Q.nonzero, Q.odd, Q.positive, Q.prime,
+        Q.rational, Q.real, Q.transcendental, Q.zero])),
+        Q.integer: (set([Q.algebraic, Q.commutative, Q.complex,
+        Q.extended_real, Q.finite, Q.hermitian, Q.integer, Q.rational,
+        Q.real]), set([Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative_infinite, Q.positive_infinite, Q.transcendental])),
+        Q.integer_elements: (set([Q.complex_elements, Q.integer_elements,
+        Q.real_elements]), set([])),
+        Q.invertible: (set([Q.fullrank, Q.invertible, Q.square]),
+        set([Q.singular])),
+        Q.irrational: (set([Q.commutative, Q.complex, Q.extended_nonzero,
+        Q.extended_real, Q.finite, Q.hermitian, Q.irrational,
+        Q.nonzero, Q.real]), set([Q.composite, Q.even, Q.imaginary,
+        Q.infinite, Q.integer, Q.negative_infinite, Q.odd,
+        Q.positive_infinite, Q.prime, Q.rational, Q.zero])),
+        Q.is_true: (set([Q.is_true]), set([])),
+        Q.lower_triangular: (set([Q.lower_triangular, Q.triangular]), set([])),
+        Q.negative: (set([Q.commutative, Q.complex, Q.extended_negative,
+        Q.extended_nonpositive, Q.extended_nonzero, Q.extended_real,
+        Q.finite, Q.hermitian, Q.negative, Q.nonpositive, Q.nonzero,
+        Q.real]), set([Q.composite, Q.extended_nonnegative,
+        Q.extended_positive, Q.imaginary, Q.infinite,
+        Q.negative_infinite, Q.nonnegative, Q.positive,
+        Q.positive_infinite, Q.prime, Q.zero])),
+        Q.negative_infinite: (set([Q.commutative, Q.extended_negative,
+        Q.extended_nonpositive, Q.extended_nonzero, Q.extended_real,
+        Q.infinite, Q.negative_infinite]), set([Q.algebraic,
+        Q.complex, Q.composite, Q.even, Q.extended_nonnegative,
+        Q.extended_positive, Q.finite, Q.imaginary, Q.integer,
+        Q.irrational, Q.negative, Q.nonnegative, Q.nonpositive,
+        Q.nonzero, Q.odd, Q.positive, Q.positive_infinite, Q.prime,
+        Q.rational, Q.real, Q.transcendental, Q.zero])),
+        Q.noninteger: (set([Q.noninteger]), set([])),
+        Q.nonnegative: (set([Q.commutative, Q.complex, Q.extended_nonnegative,
+        Q.extended_real, Q.finite, Q.hermitian, Q.nonnegative,
+        Q.real]), set([Q.extended_negative, Q.imaginary, Q.infinite,
+        Q.negative, Q.negative_infinite, Q.positive_infinite])),
+        Q.nonpositive: (set([Q.commutative, Q.complex, Q.extended_nonpositive,
+        Q.extended_real, Q.finite, Q.hermitian, Q.nonpositive,
+        Q.real]), set([Q.composite, Q.extended_positive, Q.imaginary,
+        Q.infinite, Q.negative_infinite, Q.positive,
+        Q.positive_infinite, Q.prime])),
+        Q.nonzero: (set([Q.commutative, Q.complex, Q.extended_nonzero,
+        Q.extended_real, Q.finite, Q.hermitian, Q.nonzero, Q.real]),
+        set([Q.imaginary, Q.infinite, Q.negative_infinite,
+        Q.positive_infinite, Q.zero])),
+        Q.normal: (set([Q.normal, Q.square]), set([])),
+        Q.odd: (set([Q.algebraic, Q.commutative, Q.complex,
+        Q.extended_nonzero, Q.extended_real, Q.finite, Q.hermitian,
+        Q.integer, Q.nonzero, Q.odd, Q.rational, Q.real]),
+        set([Q.even, Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative_infinite, Q.positive_infinite, Q.transcendental,
+        Q.zero])),
+        Q.orthogonal: (set([Q.fullrank, Q.invertible, Q.normal, Q.orthogonal,
+        Q.positive_definite, Q.square, Q.unitary]), set([Q.singular])),
+        Q.positive: (set([Q.commutative, Q.complex, Q.extended_nonnegative,
+        Q.extended_nonzero, Q.extended_positive, Q.extended_real,
+        Q.finite, Q.hermitian, Q.nonnegative, Q.nonzero, Q.positive,
+        Q.real]), set([Q.extended_negative, Q.extended_nonpositive,
+        Q.imaginary, Q.infinite, Q.negative, Q.negative_infinite,
+        Q.nonpositive, Q.positive_infinite, Q.zero])),
+        Q.positive_definite: (set([Q.fullrank, Q.invertible,
+        Q.positive_definite, Q.square]), set([Q.singular])),
+        Q.positive_infinite: (set([Q.commutative, Q.extended_nonnegative,
+        Q.extended_nonzero, Q.extended_positive, Q.extended_real,
+        Q.infinite, Q.positive_infinite]), set([Q.algebraic,
+        Q.complex, Q.composite, Q.even, Q.extended_negative,
+        Q.extended_nonpositive, Q.finite, Q.imaginary, Q.integer,
+        Q.irrational, Q.negative, Q.negative_infinite, Q.nonnegative,
+        Q.nonpositive, Q.nonzero, Q.odd, Q.positive, Q.prime,
+        Q.rational, Q.real, Q.transcendental, Q.zero])),
+        Q.prime: (set([Q.algebraic, Q.commutative, Q.complex,
+        Q.extended_nonnegative, Q.extended_nonzero,
+        Q.extended_positive, Q.extended_real, Q.finite, Q.hermitian,
+        Q.integer, Q.nonnegative, Q.nonzero, Q.positive, Q.prime,
+        Q.rational, Q.real]), set([Q.composite, Q.extended_negative,
+        Q.extended_nonpositive, Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative, Q.negative_infinite, Q.nonpositive,
+        Q.positive_infinite, Q.transcendental, Q.zero])),
+        Q.rational: (set([Q.algebraic, Q.commutative, Q.complex,
+        Q.extended_real, Q.finite, Q.hermitian, Q.rational, Q.real]),
+        set([Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative_infinite, Q.positive_infinite, Q.transcendental])),
+        Q.real: (set([Q.commutative, Q.complex, Q.extended_real, Q.finite,
+        Q.hermitian, Q.real]), set([Q.imaginary, Q.infinite,
+        Q.negative_infinite, Q.positive_infinite])),
+        Q.real_elements: (set([Q.complex_elements, Q.real_elements]), set([])),
+        Q.singular: (set([Q.singular]), set([Q.invertible, Q.orthogonal,
+        Q.positive_definite, Q.unitary])),
+        Q.square: (set([Q.square]), set([])),
+        Q.symmetric: (set([Q.square, Q.symmetric]), set([])),
+        Q.transcendental: (set([Q.commutative, Q.complex, Q.finite,
+        Q.transcendental]), set([Q.algebraic, Q.composite, Q.even,
+        Q.infinite, Q.integer, Q.negative_infinite, Q.odd,
+        Q.positive_infinite, Q.prime, Q.rational, Q.zero])),
+        Q.triangular: (set([Q.triangular]), set([])),
+        Q.unit_triangular: (set([Q.triangular, Q.unit_triangular]), set([])),
+        Q.unitary: (set([Q.fullrank, Q.invertible, Q.normal, Q.square,
+        Q.unitary]), set([Q.singular])),
+        Q.upper_triangular: (set([Q.triangular, Q.upper_triangular]), set([])),
+        Q.zero: (set([Q.algebraic, Q.commutative, Q.complex, Q.even,
+        Q.extended_nonnegative, Q.extended_nonpositive,
+        Q.extended_real, Q.finite, Q.hermitian, Q.integer,
+        Q.nonnegative, Q.nonpositive, Q.rational, Q.real, Q.zero]),
+        set([Q.composite, Q.extended_negative, Q.extended_nonzero,
+        Q.extended_positive, Q.imaginary, Q.infinite, Q.irrational,
+        Q.negative, Q.negative_infinite, Q.nonzero, Q.odd, Q.positive,
+        Q.positive_infinite, Q.prime, Q.transcendental])),
+    }

lib/python3.12/site-packages/sympy/assumptions/assume.py

@@ -0,0 +1,485 @@
+"""A module which implements predicates and assumption context."""
+
+from contextlib import contextmanager
+import inspect
+from sympy.core.symbol import Str
+from sympy.core.sympify import _sympify
+from sympy.logic.boolalg import Boolean, false, true
+from sympy.multipledispatch.dispatcher import Dispatcher, str_signature
+from sympy.utilities.exceptions import sympy_deprecation_warning
+from sympy.utilities.iterables import is_sequence
+from sympy.utilities.source import get_class
+
+
+class AssumptionsContext(set):
+    """
+    Set containing default assumptions which are applied to the ``ask()``
+    function.
+
+    Explanation
+    ===========
+
+    This is used to represent global assumptions, but you can also use this
+    class to create your own local assumptions contexts. It is basically a thin
+    wrapper to Python's set, so see its documentation for advanced usage.
+
+    Examples
+    ========
+
+    The default assumption context is ``global_assumptions``, which is initially empty:
+
+    >>> from sympy import ask, Q
+    >>> from sympy.assumptions import global_assumptions
+    >>> global_assumptions
+    AssumptionsContext()
+
+    You can add default assumptions:
+
+    >>> from sympy.abc import x
+    >>> global_assumptions.add(Q.real(x))
+    >>> global_assumptions
+    AssumptionsContext({Q.real(x)})
+    >>> ask(Q.real(x))
+    True
+
+    And remove them:
+
+    >>> global_assumptions.remove(Q.real(x))
+    >>> print(ask(Q.real(x)))
+    None
+
+    The ``clear()`` method removes every assumption:
+
+    >>> global_assumptions.add(Q.positive(x))
+    >>> global_assumptions
+    AssumptionsContext({Q.positive(x)})
+    >>> global_assumptions.clear()
+    >>> global_assumptions
+    AssumptionsContext()
+
+    See Also
+    ========
+
+    assuming
+
+    """
+
+    def add(self, *assumptions):
+        """Add assumptions."""
+        for a in assumptions:
+            super().add(a)
+
+    def _sympystr(self, printer):
+        if not self:
+            return "%s()" % self.__class__.__name__
+        return "{}({})".format(self.__class__.__name__, printer._print_set(self))
+
+global_assumptions = AssumptionsContext()
+
+
+class AppliedPredicate(Boolean):
+    """
+    The class of expressions resulting from applying ``Predicate`` to
+    the arguments. ``AppliedPredicate`` merely wraps its argument and
+    remain unevaluated. To evaluate it, use the ``ask()`` function.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, ask
+    >>> Q.integer(1)
+    Q.integer(1)
+
+    The ``function`` attribute returns the predicate, and the ``arguments``
+    attribute returns the tuple of arguments.
+
+    >>> type(Q.integer(1))
+    <class 'sympy.assumptions.assume.AppliedPredicate'>
+    >>> Q.integer(1).function
+    Q.integer
+    >>> Q.integer(1).arguments
+    (1,)
+
+    Applied predicates can be evaluated to a boolean value with ``ask``:
+
+    >>> ask(Q.integer(1))
+    True
+
+    """
+    __slots__ = ()
+
+    def __new__(cls, predicate, *args):
+        if not isinstance(predicate, Predicate):
+            raise TypeError("%s is not a Predicate." % predicate)
+        args = map(_sympify, args)
+        return super().__new__(cls, predicate, *args)
+
+    @property
+    def arg(self):
+        """
+        Return the expression used by this assumption.
+
+        Examples
+        ========
+
+        >>> from sympy import Q, Symbol
+        >>> x = Symbol('x')
+        >>> a = Q.integer(x + 1)
+        >>> a.arg
+        x + 1
+
+        """
+        # Will be deprecated
+        args = self._args
+        if len(args) == 2:
+            # backwards compatibility
+            return args[1]
+        raise TypeError("'arg' property is allowed only for unary predicates.")
+
+    @property
+    def function(self):
+        """
+        Return the predicate.
+        """
+        # Will be changed to self.args[0] after args overriding is removed
+        return self._args[0]
+
+    @property
+    def arguments(self):
+        """
+        Return the arguments which are applied to the predicate.
+        """
+        # Will be changed to self.args[1:] after args overriding is removed
+        return self._args[1:]
+
+    def _eval_ask(self, assumptions):
+        return self.function.eval(self.arguments, assumptions)
+
+    @property
+    def binary_symbols(self):
+        from .ask import Q
+        if self.function == Q.is_true:
+            i = self.arguments[0]
+            if i.is_Boolean or i.is_Symbol:
+                return i.binary_symbols
+        if self.function in (Q.eq, Q.ne):
+            if true in self.arguments or false in self.arguments:
+                if self.arguments[0].is_Symbol:
+                    return {self.arguments[0]}
+                elif self.arguments[1].is_Symbol:
+                    return {self.arguments[1]}
+        return set()
+
+
+class PredicateMeta(type):
+    def __new__(cls, clsname, bases, dct):
+        # If handler is not defined, assign empty dispatcher.
+        if "handler" not in dct:
+            name = f"Ask{clsname.capitalize()}Handler"
+            handler = Dispatcher(name, doc="Handler for key %s" % name)
+            dct["handler"] = handler
+
+        dct["_orig_doc"] = dct.get("__doc__", "")
+
+        return super().__new__(cls, clsname, bases, dct)
+
+    @property
+    def __doc__(cls):
+        handler = cls.handler
+        doc = cls._orig_doc
+        if cls is not Predicate and handler is not None:
+            doc += "Handler\n"
+            doc += "    =======\n\n"
+
+            # Append the handler's doc without breaking sphinx documentation.
+            docs = ["    Multiply dispatched method: %s" % handler.name]
+            if handler.doc:
+                for line in handler.doc.splitlines():
+                    if not line:
+                        continue
+                    docs.append("    %s" % line)
+            other = []
+            for sig in handler.ordering[::-1]:
+                func = handler.funcs[sig]
+                if func.__doc__:
+                    s = '    Inputs: <%s>' % str_signature(sig)
+                    lines = []
+                    for line in func.__doc__.splitlines():
+                        lines.append("    %s" % line)
+                    s += "\n".join(lines)
+                    docs.append(s)
+                else:
+                    other.append(str_signature(sig))
+            if other:
+                othersig = "    Other signatures:"
+                for line in other:
+                    othersig += "\n        * %s" % line
+                docs.append(othersig)
+
+            doc += '\n\n'.join(docs)
+
+        return doc
+
+
+class Predicate(Boolean, metaclass=PredicateMeta):
+    """
+    Base class for mathematical predicates. It also serves as a
+    constructor for undefined predicate objects.
+
+    Explanation
+    ===========
+
+    Predicate is a function that returns a boolean value [1].
+
+    Predicate function is object, and it is instance of predicate class.
+    When a predicate is applied to arguments, ``AppliedPredicate``
+    instance is returned. This merely wraps the argument and remain
+    unevaluated. To obtain the truth value of applied predicate, use the
+    function ``ask``.
+
+    Evaluation of predicate is done by multiple dispatching. You can
+    register new handler to the predicate to support new types.
+
+    Every predicate in SymPy can be accessed via the property of ``Q``.
+    For example, ``Q.even`` returns the predicate which checks if the
+    argument is even number.
+
+    To define a predicate which can be evaluated, you must subclass this
+    class, make an instance of it, and register it to ``Q``. After then,
+    dispatch the handler by argument types.
+
+    If you directly construct predicate using this class, you will get
+    ``UndefinedPredicate`` which cannot be dispatched. This is useful
+    when you are building boolean expressions which do not need to be
+    evaluated.
+
+    Examples
+    ========
+
+    Applying and evaluating to boolean value:
+
+    >>> from sympy import Q, ask
+    >>> ask(Q.prime(7))
+    True
+
+    You can define a new predicate by subclassing and dispatching. Here,
+    we define a predicate for sexy primes [2] as an example.
+
+    >>> from sympy import Predicate, Integer
+    >>> class SexyPrimePredicate(Predicate):
+    ...     name = "sexyprime"
+    >>> Q.sexyprime = SexyPrimePredicate()
+    >>> @Q.sexyprime.register(Integer, Integer)
+    ... def _(int1, int2, assumptions):
+    ...     args = sorted([int1, int2])
+    ...     if not all(ask(Q.prime(a), assumptions) for a in args):
+    ...         return False
+    ...     return args[1] - args[0] == 6
+    >>> ask(Q.sexyprime(5, 11))
+    True
+
+    Direct constructing returns ``UndefinedPredicate``, which can be
+    applied but cannot be dispatched.
+
+    >>> from sympy import Predicate, Integer
+    >>> Q.P = Predicate("P")
+    >>> type(Q.P)
+    <class 'sympy.assumptions.assume.UndefinedPredicate'>
+    >>> Q.P(1)
+    Q.P(1)
+    >>> Q.P.register(Integer)(lambda expr, assump: True)
+    Traceback (most recent call last):
+      ...
+    TypeError: <class 'sympy.assumptions.assume.UndefinedPredicate'> cannot be dispatched.
+
+    References
+    ==========
+
+    .. [1] https://en.wikipedia.org/wiki/Predicate_%28mathematical_logic%29
+    .. [2] https://en.wikipedia.org/wiki/Sexy_prime
+
+    """
+
+    is_Atom = True
+
+    def __new__(cls, *args, **kwargs):
+        if cls is Predicate:
+            return UndefinedPredicate(*args, **kwargs)
+        obj = super().__new__(cls, *args)
+        return obj
+
+    @property
+    def name(self):
+        # May be overridden
+        return type(self).__name__
+
+    @classmethod
+    def register(cls, *types, **kwargs):
+        """
+        Register the signature to the handler.
+        """
+        if cls.handler is None:
+            raise TypeError("%s cannot be dispatched." % type(cls))
+        return cls.handler.register(*types, **kwargs)
+
+    @classmethod
+    def register_many(cls, *types, **kwargs):
+        """
+        Register multiple signatures to same handler.
+        """
+        def _(func):
+            for t in types:
+                if not is_sequence(t):
+                    t = (t,)  # for convenience, allow passing `type` to mean `(type,)`
+                cls.register(*t, **kwargs)(func)
+        return _
+
+    def __call__(self, *args):
+        return AppliedPredicate(self, *args)
+
+    def eval(self, args, assumptions=True):
+        """
+        Evaluate ``self(*args)`` under the given assumptions.
+
+        This uses only direct resolution methods, not logical inference.
+        """
+        result = None
+        try:
+            result = self.handler(*args, assumptions=assumptions)
+        except NotImplementedError:
+            pass
+        return result
+
+    def _eval_refine(self, assumptions):
+        # When Predicate is no longer Boolean, delete this method
+        return self
+
+
+class UndefinedPredicate(Predicate):
+    """
+    Predicate without handler.
+
+    Explanation
+    ===========
+
+    This predicate is generated by using ``Predicate`` directly for
+    construction. It does not have a handler, and evaluating this with
+    arguments is done by SAT solver.
+
+    Examples
+    ========
+
+    >>> from sympy import Predicate, Q
+    >>> Q.P = Predicate('P')
+    >>> Q.P.func
+    <class 'sympy.assumptions.assume.UndefinedPredicate'>
+    >>> Q.P.name
+    Str('P')
+
+    """
+
+    handler = None
+
+    def __new__(cls, name, handlers=None):
+        # "handlers" parameter supports old design
+        if not isinstance(name, Str):
+            name = Str(name)
+        obj = super(Boolean, cls).__new__(cls, name)
+        obj.handlers = handlers or []
+        return obj
+
+    @property
+    def name(self):
+        return self.args[0]
+
+    def _hashable_content(self):
+        return (self.name,)
+
+    def __getnewargs__(self):
+        return (self.name,)
+
+    def __call__(self, expr):
+        return AppliedPredicate(self, expr)
+
+    def add_handler(self, handler):
+        sympy_deprecation_warning(
+            """
+            The AskHandler system is deprecated. Predicate.add_handler()
+            should be replaced with the multipledispatch handler of Predicate.
+            """,
+            deprecated_since_version="1.8",
+            active_deprecations_target='deprecated-askhandler',
+        )
+        self.handlers.append(handler)
+
+    def remove_handler(self, handler):
+        sympy_deprecation_warning(
+            """
+            The AskHandler system is deprecated. Predicate.remove_handler()
+            should be replaced with the multipledispatch handler of Predicate.
+            """,
+            deprecated_since_version="1.8",
+            active_deprecations_target='deprecated-askhandler',
+        )
+        self.handlers.remove(handler)
+
+    def eval(self, args, assumptions=True):
+        # Support for deprecated design
+        # When old design is removed, this will always return None
+        sympy_deprecation_warning(
+            """
+            The AskHandler system is deprecated. Evaluating UndefinedPredicate
+            objects should be replaced with the multipledispatch handler of
+            Predicate.
+            """,
+            deprecated_since_version="1.8",
+            active_deprecations_target='deprecated-askhandler',
+            stacklevel=5,
+        )
+        expr, = args
+        res, _res = None, None
+        mro = inspect.getmro(type(expr))
+        for handler in self.handlers:
+            cls = get_class(handler)
+            for subclass in mro:
+                eval_ = getattr(cls, subclass.__name__, None)
+                if eval_ is None:
+                    continue
+                res = eval_(expr, assumptions)
+                # Do not stop if value returned is None
+                # Try to check for higher classes
+                if res is None:
+                    continue
+                if _res is None:
+                    _res = res
+                else:
+                    # only check consistency if both resolutors have concluded
+                    if _res != res:
+                        raise ValueError('incompatible resolutors')
+                break
+        return res
+
+
+@contextmanager
+def assuming(*assumptions):
+    """
+    Context manager for assumptions.
+
+    Examples
+    ========
+
+    >>> from sympy import assuming, Q, ask
+    >>> from sympy.abc import x, y
+    >>> print(ask(Q.integer(x + y)))
+    None
+    >>> with assuming(Q.integer(x), Q.integer(y)):
+    ...     print(ask(Q.integer(x + y)))
+    True
+    """
+    old_global_assumptions = global_assumptions.copy()
+    global_assumptions.update(assumptions)
+    try:
+        yield
+    finally:
+        global_assumptions.clear()
+        global_assumptions.update(old_global_assumptions)

lib/python3.12/site-packages/sympy/assumptions/cnf.py

@@ -0,0 +1,445 @@
+"""
+The classes used here are for the internal use of assumptions system
+only and should not be used anywhere else as these do not possess the
+signatures common to SymPy objects. For general use of logic constructs
+please refer to sympy.logic classes And, Or, Not, etc.
+"""
+from itertools import combinations, product, zip_longest
+from sympy.assumptions.assume import AppliedPredicate, Predicate
+from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le
+from sympy.core.singleton import S
+from sympy.logic.boolalg import Or, And, Not, Xnor
+from sympy.logic.boolalg import (Equivalent, ITE, Implies, Nand, Nor, Xor)
+
+
+class Literal:
+    """
+    The smallest element of a CNF object.
+
+    Parameters
+    ==========
+
+    lit : Boolean expression
+
+    is_Not : bool
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import Literal
+    >>> from sympy.abc import x
+    >>> Literal(Q.even(x))
+    Literal(Q.even(x), False)
+    >>> Literal(~Q.even(x))
+    Literal(Q.even(x), True)
+    """
+
+    def __new__(cls, lit, is_Not=False):
+        if isinstance(lit, Not):
+            lit = lit.args[0]
+            is_Not = True
+        elif isinstance(lit, (AND, OR, Literal)):
+            return ~lit if is_Not else lit
+        obj = super().__new__(cls)
+        obj.lit = lit
+        obj.is_Not = is_Not
+        return obj
+
+    @property
+    def arg(self):
+        return self.lit
+
+    def rcall(self, expr):
+        if callable(self.lit):
+            lit = self.lit(expr)
+        else:
+            lit = self.lit.apply(expr)
+        return type(self)(lit, self.is_Not)
+
+    def __invert__(self):
+        is_Not = not self.is_Not
+        return Literal(self.lit, is_Not)
+
+    def __str__(self):
+        return '{}({}, {})'.format(type(self).__name__, self.lit, self.is_Not)
+
+    __repr__ = __str__
+
+    def __eq__(self, other):
+        return self.arg == other.arg and self.is_Not == other.is_Not
+
+    def __hash__(self):
+        h = hash((type(self).__name__, self.arg, self.is_Not))
+        return h
+
+
+class OR:
+    """
+    A low-level implementation for Or
+    """
+    def __init__(self, *args):
+        self._args = args
+
+    @property
+    def args(self):
+        return sorted(self._args, key=str)
+
+    def rcall(self, expr):
+        return type(self)(*[arg.rcall(expr)
+                            for arg in self._args
+                            ])
+
+    def __invert__(self):
+        return AND(*[~arg for arg in self._args])
+
+    def __hash__(self):
+        return hash((type(self).__name__,) + tuple(self.args))
+
+    def __eq__(self, other):
+        return self.args == other.args
+
+    def __str__(self):
+        s = '(' + ' | '.join([str(arg) for arg in self.args]) + ')'
+        return s
+
+    __repr__ = __str__
+
+
+class AND:
+    """
+    A low-level implementation for And
+    """
+    def __init__(self, *args):
+        self._args = args
+
+    def __invert__(self):
+        return OR(*[~arg for arg in self._args])
+
+    @property
+    def args(self):
+        return sorted(self._args, key=str)
+
+    def rcall(self, expr):
+        return type(self)(*[arg.rcall(expr)
+                            for arg in self._args
+                            ])
+
+    def __hash__(self):
+        return hash((type(self).__name__,) + tuple(self.args))
+
+    def __eq__(self, other):
+        return self.args == other.args
+
+    def __str__(self):
+        s = '('+' & '.join([str(arg) for arg in self.args])+')'
+        return s
+
+    __repr__ = __str__
+
+
+def to_NNF(expr, composite_map=None):
+    """
+    Generates the Negation Normal Form of any boolean expression in terms
+    of AND, OR, and Literal objects.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, Eq
+    >>> from sympy.assumptions.cnf import to_NNF
+    >>> from sympy.abc import x, y
+    >>> expr = Q.even(x) & ~Q.positive(x)
+    >>> to_NNF(expr)
+    (Literal(Q.even(x), False) & Literal(Q.positive(x), True))
+
+    Supported boolean objects are converted to corresponding predicates.
+
+    >>> to_NNF(Eq(x, y))
+    Literal(Q.eq(x, y), False)
+
+    If ``composite_map`` argument is given, ``to_NNF`` decomposes the
+    specified predicate into a combination of primitive predicates.
+
+    >>> cmap = {Q.nonpositive: Q.negative | Q.zero}
+    >>> to_NNF(Q.nonpositive, cmap)
+    (Literal(Q.negative, False) | Literal(Q.zero, False))
+    >>> to_NNF(Q.nonpositive(x), cmap)
+    (Literal(Q.negative(x), False) | Literal(Q.zero(x), False))
+    """
+    from sympy.assumptions.ask import Q
+
+    if composite_map is None:
+        composite_map = {}
+
+
+    binrelpreds = {Eq: Q.eq, Ne: Q.ne, Gt: Q.gt, Lt: Q.lt, Ge: Q.ge, Le: Q.le}
+    if type(expr) in binrelpreds:
+        pred = binrelpreds[type(expr)]
+        expr = pred(*expr.args)
+
+    if isinstance(expr, Not):
+        arg = expr.args[0]
+        tmp = to_NNF(arg, composite_map)  # Strategy: negate the NNF of expr
+        return ~tmp
+
+    if isinstance(expr, Or):
+        return OR(*[to_NNF(x, composite_map) for x in Or.make_args(expr)])
+
+    if isinstance(expr, And):
+        return AND(*[to_NNF(x, composite_map) for x in And.make_args(expr)])
+
+    if isinstance(expr, Nand):
+        tmp = AND(*[to_NNF(x, composite_map) for x in expr.args])
+        return ~tmp
+
+    if isinstance(expr, Nor):
+        tmp = OR(*[to_NNF(x, composite_map) for x in expr.args])
+        return ~tmp
+
+    if isinstance(expr, Xor):
+        cnfs = []
+        for i in range(0, len(expr.args) + 1, 2):
+            for neg in combinations(expr.args, i):
+                clause = [~to_NNF(s, composite_map) if s in neg else to_NNF(s, composite_map)
+                          for s in expr.args]
+                cnfs.append(OR(*clause))
+        return AND(*cnfs)
+
+    if isinstance(expr, Xnor):
+        cnfs = []
+        for i in range(0, len(expr.args) + 1, 2):
+            for neg in combinations(expr.args, i):
+                clause = [~to_NNF(s, composite_map) if s in neg else to_NNF(s, composite_map)
+                          for s in expr.args]
+                cnfs.append(OR(*clause))
+        return ~AND(*cnfs)
+
+    if isinstance(expr, Implies):
+        L, R = to_NNF(expr.args[0], composite_map), to_NNF(expr.args[1], composite_map)
+        return OR(~L, R)
+
+    if isinstance(expr, Equivalent):
+        cnfs = []
+        for a, b in zip_longest(expr.args, expr.args[1:], fillvalue=expr.args[0]):
+            a = to_NNF(a, composite_map)
+            b = to_NNF(b, composite_map)
+            cnfs.append(OR(~a, b))
+        return AND(*cnfs)
+
+    if isinstance(expr, ITE):
+        L = to_NNF(expr.args[0], composite_map)
+        M = to_NNF(expr.args[1], composite_map)
+        R = to_NNF(expr.args[2], composite_map)
+        return AND(OR(~L, M), OR(L, R))
+
+    if isinstance(expr, AppliedPredicate):
+        pred, args = expr.function, expr.arguments
+        newpred = composite_map.get(pred, None)
+        if newpred is not None:
+            return to_NNF(newpred.rcall(*args), composite_map)
+
+    if isinstance(expr, Predicate):
+        newpred = composite_map.get(expr, None)
+        if newpred is not None:
+            return to_NNF(newpred, composite_map)
+
+    return Literal(expr)
+
+
+def distribute_AND_over_OR(expr):
+    """
+    Distributes AND over OR in the NNF expression.
+    Returns the result( Conjunctive Normal Form of expression)
+    as a CNF object.
+    """
+    if not isinstance(expr, (AND, OR)):
+        tmp = set()
+        tmp.add(frozenset((expr,)))
+        return CNF(tmp)
+
+    if isinstance(expr, OR):
+        return CNF.all_or(*[distribute_AND_over_OR(arg)
+                            for arg in expr._args])
+
+    if isinstance(expr, AND):
+        return CNF.all_and(*[distribute_AND_over_OR(arg)
+                             for arg in expr._args])
+
+
+class CNF:
+    """
+    Class to represent CNF of a Boolean expression.
+    Consists of set of clauses, which themselves are stored as
+    frozenset of Literal objects.
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import CNF
+    >>> from sympy.abc import x
+    >>> cnf = CNF.from_prop(Q.real(x) & ~Q.zero(x))
+    >>> cnf.clauses
+    {frozenset({Literal(Q.zero(x), True)}),
+    frozenset({Literal(Q.negative(x), False),
+    Literal(Q.positive(x), False), Literal(Q.zero(x), False)})}
+    """
+    def __init__(self, clauses=None):
+        if not clauses:
+            clauses = set()
+        self.clauses = clauses
+
+    def add(self, prop):
+        clauses = CNF.to_CNF(prop).clauses
+        self.add_clauses(clauses)
+
+    def __str__(self):
+        s = ' & '.join(
+            ['(' + ' | '.join([str(lit) for lit in clause]) +')'
+            for clause in self.clauses]
+        )
+        return s
+
+    def extend(self, props):
+        for p in props:
+            self.add(p)
+        return self
+
+    def copy(self):
+        return CNF(set(self.clauses))
+
+    def add_clauses(self, clauses):
+        self.clauses |= clauses
+
+    @classmethod
+    def from_prop(cls, prop):
+        res = cls()
+        res.add(prop)
+        return res
+
+    def __iand__(self, other):
+        self.add_clauses(other.clauses)
+        return self
+
+    def all_predicates(self):
+        predicates = set()
+        for c in self.clauses:
+            predicates |= {arg.lit for arg in c}
+        return predicates
+
+    def _or(self, cnf):
+        clauses = set()
+        for a, b in product(self.clauses, cnf.clauses):
+            tmp = set(a)
+            tmp.update(b)
+            clauses.add(frozenset(tmp))
+        return CNF(clauses)
+
+    def _and(self, cnf):
+        clauses = self.clauses.union(cnf.clauses)
+        return CNF(clauses)
+
+    def _not(self):
+        clss = list(self.clauses)
+        ll = {frozenset((~x,)) for x in clss[-1]}
+        ll = CNF(ll)
+
+        for rest in clss[:-1]:
+            p = {frozenset((~x,)) for x in rest}
+            ll = ll._or(CNF(p))
+        return ll
+
+    def rcall(self, expr):
+        clause_list = []
+        for clause in self.clauses:
+            lits = [arg.rcall(expr) for arg in clause]
+            clause_list.append(OR(*lits))
+        expr = AND(*clause_list)
+        return distribute_AND_over_OR(expr)
+
+    @classmethod
+    def all_or(cls, *cnfs):
+        b = cnfs[0].copy()
+        for rest in cnfs[1:]:
+            b = b._or(rest)
+        return b
+
+    @classmethod
+    def all_and(cls, *cnfs):
+        b = cnfs[0].copy()
+        for rest in cnfs[1:]:
+            b = b._and(rest)
+        return b
+
+    @classmethod
+    def to_CNF(cls, expr):
+        from sympy.assumptions.facts import get_composite_predicates
+        expr = to_NNF(expr, get_composite_predicates())
+        expr = distribute_AND_over_OR(expr)
+        return expr
+
+    @classmethod
+    def CNF_to_cnf(cls, cnf):
+        """
+        Converts CNF object to SymPy's boolean expression
+        retaining the form of expression.
+        """
+        def remove_literal(arg):
+            return Not(arg.lit) if arg.is_Not else arg.lit
+
+        return And(*(Or(*(remove_literal(arg) for arg in clause)) for clause in cnf.clauses))
+
+
+class EncodedCNF:
+    """
+    Class for encoding the CNF expression.
+    """
+    def __init__(self, data=None, encoding=None):
+        if not data and not encoding:
+            data = []
+            encoding = {}
+        self.data = data
+        self.encoding = encoding
+        self._symbols = list(encoding.keys())
+
+    def from_cnf(self, cnf):
+        self._symbols = list(cnf.all_predicates())
+        n = len(self._symbols)
+        self.encoding = dict(zip(self._symbols, range(1, n + 1)))
+        self.data = [self.encode(clause) for clause in cnf.clauses]
+
+    @property
+    def symbols(self):
+        return self._symbols
+
+    @property
+    def variables(self):
+        return range(1, len(self._symbols) + 1)
+
+    def copy(self):
+        new_data = [set(clause) for clause in self.data]
+        return EncodedCNF(new_data, dict(self.encoding))
+
+    def add_prop(self, prop):
+        cnf = CNF.from_prop(prop)
+        self.add_from_cnf(cnf)
+
+    def add_from_cnf(self, cnf):
+        clauses = [self.encode(clause) for clause in cnf.clauses]
+        self.data += clauses
+
+    def encode_arg(self, arg):
+        literal = arg.lit
+        value = self.encoding.get(literal, None)
+        if value is None:
+            n = len(self._symbols)
+            self._symbols.append(literal)
+            value = self.encoding[literal] = n + 1
+        if arg.is_Not:
+            return -value
+        else:
+            return value
+
+    def encode(self, clause):
+        return {self.encode_arg(arg) if not arg.lit == S.false else 0 for arg in clause}

lib/python3.12/site-packages/sympy/assumptions/facts.py

@@ -0,0 +1,270 @@
+"""
+Known facts in assumptions module.
+
+This module defines the facts between unary predicates in ``get_known_facts()``,
+and supports functions to generate the contents in
+``sympy.assumptions.ask_generated`` file.
+"""
+
+from sympy.assumptions.ask import Q
+from sympy.assumptions.assume import AppliedPredicate
+from sympy.core.cache import cacheit
+from sympy.core.symbol import Symbol
+from sympy.logic.boolalg import (to_cnf, And, Not, Implies, Equivalent,
+    Exclusive,)
+from sympy.logic.inference import satisfiable
+
+
+@cacheit
+def get_composite_predicates():
+    # To reduce the complexity of sat solver, these predicates are
+    # transformed into the combination of primitive predicates.
+    return {
+        Q.real : Q.negative | Q.zero | Q.positive,
+        Q.integer : Q.even | Q.odd,
+        Q.nonpositive : Q.negative | Q.zero,
+        Q.nonzero : Q.negative | Q.positive,
+        Q.nonnegative : Q.zero | Q.positive,
+        Q.extended_real : Q.negative_infinite | Q.negative | Q.zero | Q.positive | Q.positive_infinite,
+        Q.extended_positive: Q.positive | Q.positive_infinite,
+        Q.extended_negative: Q.negative | Q.negative_infinite,
+        Q.extended_nonzero: Q.negative_infinite | Q.negative | Q.positive | Q.positive_infinite,
+        Q.extended_nonpositive: Q.negative_infinite | Q.negative | Q.zero,
+        Q.extended_nonnegative: Q.zero | Q.positive | Q.positive_infinite,
+        Q.complex : Q.algebraic | Q.transcendental
+    }
+
+
+@cacheit
+def get_known_facts(x=None):
+    """
+    Facts between unary predicates.
+
+    Parameters
+    ==========
+
+    x : Symbol, optional
+        Placeholder symbol for unary facts. Default is ``Symbol('x')``.
+
+    Returns
+    =======
+
+    fact : Known facts in conjugated normal form.
+
+    """
+    if x is None:
+        x = Symbol('x')
+
+    fact = And(
+        get_number_facts(x),
+        get_matrix_facts(x)
+    )
+    return fact
+
+
+@cacheit
+def get_number_facts(x = None):
+    """
+    Facts between unary number predicates.
+
+    Parameters
+    ==========
+
+    x : Symbol, optional
+        Placeholder symbol for unary facts. Default is ``Symbol('x')``.
+
+    Returns
+    =======
+
+    fact : Known facts in conjugated normal form.
+
+    """
+    if x is None:
+        x = Symbol('x')
+
+    fact = And(
+        # primitive predicates for extended real exclude each other.
+        Exclusive(Q.negative_infinite(x), Q.negative(x), Q.zero(x),
+            Q.positive(x), Q.positive_infinite(x)),
+
+        # build complex plane
+        Exclusive(Q.real(x), Q.imaginary(x)),
+        Implies(Q.real(x) | Q.imaginary(x), Q.complex(x)),
+
+        # other subsets of complex
+        Exclusive(Q.transcendental(x), Q.algebraic(x)),
+        Equivalent(Q.real(x), Q.rational(x) | Q.irrational(x)),
+        Exclusive(Q.irrational(x), Q.rational(x)),
+        Implies(Q.rational(x), Q.algebraic(x)),
+
+        # integers
+        Exclusive(Q.even(x), Q.odd(x)),
+        Implies(Q.integer(x), Q.rational(x)),
+        Implies(Q.zero(x), Q.even(x)),
+        Exclusive(Q.composite(x), Q.prime(x)),
+        Implies(Q.composite(x) | Q.prime(x), Q.integer(x) & Q.positive(x)),
+        Implies(Q.even(x) & Q.positive(x) & ~Q.prime(x), Q.composite(x)),
+
+        # hermitian and antihermitian
+        Implies(Q.real(x), Q.hermitian(x)),
+        Implies(Q.imaginary(x), Q.antihermitian(x)),
+        Implies(Q.zero(x), Q.hermitian(x) | Q.antihermitian(x)),
+
+        # define finity and infinity, and build extended real line
+        Exclusive(Q.infinite(x), Q.finite(x)),
+        Implies(Q.complex(x), Q.finite(x)),
+        Implies(Q.negative_infinite(x) | Q.positive_infinite(x), Q.infinite(x)),
+
+        # commutativity
+        Implies(Q.finite(x) | Q.infinite(x), Q.commutative(x)),
+    )
+    return fact
+
+
+@cacheit
+def get_matrix_facts(x = None):
+    """
+    Facts between unary matrix predicates.
+
+    Parameters
+    ==========
+
+    x : Symbol, optional
+        Placeholder symbol for unary facts. Default is ``Symbol('x')``.
+
+    Returns
+    =======
+
+    fact : Known facts in conjugated normal form.
+
+    """
+    if x is None:
+        x = Symbol('x')
+
+    fact = And(
+        # matrices
+        Implies(Q.orthogonal(x), Q.positive_definite(x)),
+        Implies(Q.orthogonal(x), Q.unitary(x)),
+        Implies(Q.unitary(x) & Q.real_elements(x), Q.orthogonal(x)),
+        Implies(Q.unitary(x), Q.normal(x)),
+        Implies(Q.unitary(x), Q.invertible(x)),
+        Implies(Q.normal(x), Q.square(x)),
+        Implies(Q.diagonal(x), Q.normal(x)),
+        Implies(Q.positive_definite(x), Q.invertible(x)),
+        Implies(Q.diagonal(x), Q.upper_triangular(x)),
+        Implies(Q.diagonal(x), Q.lower_triangular(x)),
+        Implies(Q.lower_triangular(x), Q.triangular(x)),
+        Implies(Q.upper_triangular(x), Q.triangular(x)),
+        Implies(Q.triangular(x), Q.upper_triangular(x) | Q.lower_triangular(x)),
+        Implies(Q.upper_triangular(x) & Q.lower_triangular(x), Q.diagonal(x)),
+        Implies(Q.diagonal(x), Q.symmetric(x)),
+        Implies(Q.unit_triangular(x), Q.triangular(x)),
+        Implies(Q.invertible(x), Q.fullrank(x)),
+        Implies(Q.invertible(x), Q.square(x)),
+        Implies(Q.symmetric(x), Q.square(x)),
+        Implies(Q.fullrank(x) & Q.square(x), Q.invertible(x)),
+        Equivalent(Q.invertible(x), ~Q.singular(x)),
+        Implies(Q.integer_elements(x), Q.real_elements(x)),
+        Implies(Q.real_elements(x), Q.complex_elements(x)),
+    )
+    return fact
+
+
+
+def generate_known_facts_dict(keys, fact):
+    """
+    Computes and returns a dictionary which contains the relations between
+    unary predicates.
+
+    Each key is a predicate, and item is two groups of predicates.
+    First group contains the predicates which are implied by the key, and
+    second group contains the predicates which are rejected by the key.
+
+    All predicates in *keys* and *fact* must be unary and have same placeholder
+    symbol.
+
+    Parameters
+    ==========
+
+    keys : list of AppliedPredicate instances.
+
+    fact : Fact between predicates in conjugated normal form.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, And, Implies
+    >>> from sympy.assumptions.facts import generate_known_facts_dict
+    >>> from sympy.abc import x
+    >>> keys = [Q.even(x), Q.odd(x), Q.zero(x)]
+    >>> fact = And(Implies(Q.even(x), ~Q.odd(x)),
+    ...     Implies(Q.zero(x), Q.even(x)))
+    >>> generate_known_facts_dict(keys, fact)
+    {Q.even: ({Q.even}, {Q.odd}),
+     Q.odd: ({Q.odd}, {Q.even, Q.zero}),
+     Q.zero: ({Q.even, Q.zero}, {Q.odd})}
+    """
+    fact_cnf = to_cnf(fact)
+    mapping = single_fact_lookup(keys, fact_cnf)
+
+    ret = {}
+    for key, value in mapping.items():
+        implied = set()
+        rejected = set()
+        for expr in value:
+            if isinstance(expr, AppliedPredicate):
+                implied.add(expr.function)
+            elif isinstance(expr, Not):
+                pred = expr.args[0]
+                rejected.add(pred.function)
+        ret[key.function] = (implied, rejected)
+    return ret
+
+
+@cacheit
+def get_known_facts_keys():
+    """
+    Return every unary predicates registered to ``Q``.
+
+    This function is used to generate the keys for
+    ``generate_known_facts_dict``.
+
+    """
+    # exclude polyadic predicates
+    exclude = {Q.eq, Q.ne, Q.gt, Q.lt, Q.ge, Q.le}
+
+    result = []
+    for attr in Q.__class__.__dict__:
+        if attr.startswith('__'):
+            continue
+        pred = getattr(Q, attr)
+        if pred in exclude:
+            continue
+        result.append(pred)
+    return result
+
+
+def single_fact_lookup(known_facts_keys, known_facts_cnf):
+    # Return the dictionary for quick lookup of single fact
+    mapping = {}
+    for key in known_facts_keys:
+        mapping[key] = {key}
+        for other_key in known_facts_keys:
+            if other_key != key:
+                if ask_full_inference(other_key, key, known_facts_cnf):
+                    mapping[key].add(other_key)
+                if ask_full_inference(~other_key, key, known_facts_cnf):
+                    mapping[key].add(~other_key)
+    return mapping
+
+
+def ask_full_inference(proposition, assumptions, known_facts_cnf):
+    """
+    Method for inferring properties about objects.
+
+    """
+    if not satisfiable(And(known_facts_cnf, assumptions, proposition)):
+        return False
+    if not satisfiable(And(known_facts_cnf, assumptions, Not(proposition))):
+        return True
+    return None

lib/python3.12/site-packages/sympy/assumptions/handlers/calculus.py

@@ -0,0 +1,258 @@
+"""
+This module contains query handlers responsible for calculus queries:
+infinitesimal, finite, etc.
+"""
+
+from sympy.assumptions import Q, ask
+from sympy.core import Add, Mul, Pow, Symbol
+from sympy.core.numbers import (NegativeInfinity, GoldenRatio,
+    Infinity, Exp1, ComplexInfinity, ImaginaryUnit, NaN, Number, Pi, E,
+    TribonacciConstant)
+from sympy.functions import cos, exp, log, sign, sin
+from sympy.logic.boolalg import conjuncts
+
+from ..predicates.calculus import (FinitePredicate, InfinitePredicate,
+    PositiveInfinitePredicate, NegativeInfinitePredicate)
+
+
+# FinitePredicate
+
+
+@FinitePredicate.register(Symbol)
+def _(expr, assumptions):
+    """
+    Handles Symbol.
+    """
+    if expr.is_finite is not None:
+        return expr.is_finite
+    if Q.finite(expr) in conjuncts(assumptions):
+        return True
+    return None
+
+@FinitePredicate.register(Add)
+def _(expr, assumptions):
+    """
+    Return True if expr is bounded, False if not and None if unknown.
+
+    Truth Table:
+
+    +-------+-----+-----------+-----------+
+    |       |     |           |           |
+    |       |  B  |     U     |     ?     |
+    |       |     |           |           |
+    +-------+-----+---+---+---+---+---+---+
+    |       |     |   |   |   |   |   |   |
+    |       |     |'+'|'-'|'x'|'+'|'-'|'x'|
+    |       |     |   |   |   |   |   |   |
+    +-------+-----+---+---+---+---+---+---+
+    |       |     |           |           |
+    |   B   |  B  |     U     |     ?     |
+    |       |     |           |           |
+    +---+---+-----+---+---+---+---+---+---+
+    |   |   |     |   |   |   |   |   |   |
+    |   |'+'|     | U | ? | ? | U | ? | ? |
+    |   |   |     |   |   |   |   |   |   |
+    |   +---+-----+---+---+---+---+---+---+
+    |   |   |     |   |   |   |   |   |   |
+    | U |'-'|     | ? | U | ? | ? | U | ? |
+    |   |   |     |   |   |   |   |   |   |
+    |   +---+-----+---+---+---+---+---+---+
+    |   |   |     |           |           |
+    |   |'x'|     |     ?     |     ?     |
+    |   |   |     |           |           |
+    +---+---+-----+---+---+---+---+---+---+
+    |       |     |           |           |
+    |   ?   |     |           |     ?     |
+    |       |     |           |           |
+    +-------+-----+-----------+---+---+---+
+
+        * 'B' = Bounded
+
+        * 'U' = Unbounded
+
+        * '?' = unknown boundedness
+
+        * '+' = positive sign
+
+        * '-' = negative sign
+
+        * 'x' = sign unknown
+
+        * All Bounded -> True
+
+        * 1 Unbounded and the rest Bounded -> False
+
+        * >1 Unbounded, all with same known sign -> False
+
+        * Any Unknown and unknown sign -> None
+
+        * Else -> None
+
+    When the signs are not the same you can have an undefined
+    result as in oo - oo, hence 'bounded' is also undefined.
+    """
+    sign = -1  # sign of unknown or infinite
+    result = True
+    for arg in expr.args:
+        _bounded = ask(Q.finite(arg), assumptions)
+        if _bounded:
+            continue
+        s = ask(Q.extended_positive(arg), assumptions)
+        # if there has been more than one sign or if the sign of this arg
+        # is None and Bounded is None or there was already
+        # an unknown sign, return None
+        if sign != -1 and s != sign or \
+                s is None and None in (_bounded, sign):
+            return None
+        else:
+            sign = s
+        # once False, do not change
+        if result is not False:
+            result = _bounded
+    return result
+
+@FinitePredicate.register(Mul)
+def _(expr, assumptions):
+    """
+    Return True if expr is bounded, False if not and None if unknown.
+
+    Truth Table:
+
+    +---+---+---+--------+
+    |   |   |   |        |
+    |   | B | U |   ?    |
+    |   |   |   |        |
+    +---+---+---+---+----+
+    |   |   |   |   |    |
+    |   |   |   | s | /s |
+    |   |   |   |   |    |
+    +---+---+---+---+----+
+    |   |   |   |        |
+    | B | B | U |   ?    |
+    |   |   |   |        |
+    +---+---+---+---+----+
+    |   |   |   |   |    |
+    | U |   | U | U | ?  |
+    |   |   |   |   |    |
+    +---+---+---+---+----+
+    |   |   |   |        |
+    | ? |   |   |   ?    |
+    |   |   |   |        |
+    +---+---+---+---+----+
+
+        * B = Bounded
+
+        * U = Unbounded
+
+        * ? = unknown boundedness
+
+        * s = signed (hence nonzero)
+
+        * /s = not signed
+    """
+    result = True
+    for arg in expr.args:
+        _bounded = ask(Q.finite(arg), assumptions)
+        if _bounded:
+            continue
+        elif _bounded is None:
+            if result is None:
+                return None
+            if ask(Q.extended_nonzero(arg), assumptions) is None:
+                return None
+            if result is not False:
+                result = None
+        else:
+            result = False
+    return result
+
+@FinitePredicate.register(Pow)
+def _(expr, assumptions):
+    """
+    * Unbounded ** NonZero -> Unbounded
+
+    * Bounded ** Bounded -> Bounded
+
+    * Abs()<=1 ** Positive -> Bounded
+
+    * Abs()>=1 ** Negative -> Bounded
+
+    * Otherwise unknown
+    """
+    if expr.base == E:
+        return ask(Q.finite(expr.exp), assumptions)
+
+    base_bounded = ask(Q.finite(expr.base), assumptions)
+    exp_bounded = ask(Q.finite(expr.exp), assumptions)
+    if base_bounded is None and exp_bounded is None:  # Common Case
+        return None
+    if base_bounded is False and ask(Q.extended_nonzero(expr.exp), assumptions):
+        return False
+    if base_bounded and exp_bounded:
+        return True
+    if (abs(expr.base) <= 1) == True and ask(Q.extended_positive(expr.exp), assumptions):
+        return True
+    if (abs(expr.base) >= 1) == True and ask(Q.extended_negative(expr.exp), assumptions):
+        return True
+    if (abs(expr.base) >= 1) == True and exp_bounded is False:
+        return False
+    return None
+
+@FinitePredicate.register(exp)
+def _(expr, assumptions):
+    return ask(Q.finite(expr.exp), assumptions)
+
+@FinitePredicate.register(log)
+def _(expr, assumptions):
+    # After complex -> finite fact is registered to new assumption system,
+    # querying Q.infinite may be removed.
+    if ask(Q.infinite(expr.args[0]), assumptions):
+        return False
+    return ask(~Q.zero(expr.args[0]), assumptions)
+
+@FinitePredicate.register_many(cos, sin, Number, Pi, Exp1, GoldenRatio,
+    TribonacciConstant, ImaginaryUnit, sign)
+def _(expr, assumptions):
+    return True
+
+@FinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
+def _(expr, assumptions):
+    return False
+
+@FinitePredicate.register(NaN)
+def _(expr, assumptions):
+    return None
+
+
+# InfinitePredicate
+
+
+@InfinitePredicate.register_many(ComplexInfinity, Infinity, NegativeInfinity)
+def _(expr, assumptions):
+    return True
+
+
+# PositiveInfinitePredicate
+
+
+@PositiveInfinitePredicate.register(Infinity)
+def _(expr, assumptions):
+    return True
+
+
+@PositiveInfinitePredicate.register_many(NegativeInfinity, ComplexInfinity)
+def _(expr, assumptions):
+    return False
+
+
+# NegativeInfinitePredicate
+
+
+@NegativeInfinitePredicate.register(NegativeInfinity)
+def _(expr, assumptions):
+    return True
+
+
+@NegativeInfinitePredicate.register_many(Infinity, ComplexInfinity)
+def _(expr, assumptions):
+    return False

lib/python3.12/site-packages/sympy/assumptions/handlers/matrices.py

@@ -0,0 +1,716 @@
+"""
+This module contains query handlers responsible for Matrices queries:
+Square, Symmetric, Invertible etc.
+"""
+
+from sympy.logic.boolalg import conjuncts
+from sympy.assumptions import Q, ask
+from sympy.assumptions.handlers import test_closed_group
+from sympy.matrices import MatrixBase
+from sympy.matrices.expressions import (BlockMatrix, BlockDiagMatrix, Determinant,
+    DiagMatrix, DiagonalMatrix, HadamardProduct, Identity, Inverse, MatAdd, MatMul,
+    MatPow, MatrixExpr, MatrixSlice, MatrixSymbol, OneMatrix, Trace, Transpose,
+    ZeroMatrix)
+from sympy.matrices.expressions.blockmatrix import reblock_2x2
+from sympy.matrices.expressions.factorizations import Factorization
+from sympy.matrices.expressions.fourier import DFT
+from sympy.core.logic import fuzzy_and
+from sympy.utilities.iterables import sift
+from sympy.core import Basic
+
+from ..predicates.matrices import (SquarePredicate, SymmetricPredicate,
+    InvertiblePredicate, OrthogonalPredicate, UnitaryPredicate,
+    FullRankPredicate, PositiveDefinitePredicate, UpperTriangularPredicate,
+    LowerTriangularPredicate, DiagonalPredicate, IntegerElementsPredicate,
+    RealElementsPredicate, ComplexElementsPredicate)
+
+
+def _Factorization(predicate, expr, assumptions):
+    if predicate in expr.predicates:
+        return True
+
+
+# SquarePredicate
+
+@SquarePredicate.register(MatrixExpr)
+def _(expr, assumptions):
+    return expr.shape[0] == expr.shape[1]
+
+
+# SymmetricPredicate
+
+@SymmetricPredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, mmul = expr.as_coeff_mmul()
+    if all(ask(Q.symmetric(arg), assumptions) for arg in mmul.args):
+        return True
+    # TODO: implement sathandlers system for the matrices.
+    # Now it duplicates the general fact: Implies(Q.diagonal, Q.symmetric).
+    if ask(Q.diagonal(expr), assumptions):
+        return True
+    if len(mmul.args) >= 2 and mmul.args[0] == mmul.args[-1].T:
+        if len(mmul.args) == 2:
+            return True
+        return ask(Q.symmetric(MatMul(*mmul.args[1:-1])), assumptions)
+
+@SymmetricPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.symmetric(base), assumptions)
+    return None
+
+@SymmetricPredicate.register(MatAdd)
+def _(expr, assumptions):
+    return all(ask(Q.symmetric(arg), assumptions) for arg in expr.args)
+
+@SymmetricPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    # TODO: implement sathandlers system for the matrices.
+    # Now it duplicates the general fact: Implies(Q.diagonal, Q.symmetric).
+    if ask(Q.diagonal(expr), assumptions):
+        return True
+    if Q.symmetric(expr) in conjuncts(assumptions):
+        return True
+
+@SymmetricPredicate.register_many(OneMatrix, ZeroMatrix)
+def _(expr, assumptions):
+    return ask(Q.square(expr), assumptions)
+
+@SymmetricPredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.symmetric(expr.arg), assumptions)
+
+@SymmetricPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    # TODO: implement sathandlers system for the matrices.
+    # Now it duplicates the general fact: Implies(Q.diagonal, Q.symmetric).
+    if ask(Q.diagonal(expr), assumptions):
+        return True
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.symmetric(expr.parent), assumptions)
+
+@SymmetricPredicate.register(Identity)
+def _(expr, assumptions):
+    return True
+
+
+# InvertiblePredicate
+
+@InvertiblePredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, mmul = expr.as_coeff_mmul()
+    if all(ask(Q.invertible(arg), assumptions) for arg in mmul.args):
+        return True
+    if any(ask(Q.invertible(arg), assumptions) is False
+            for arg in mmul.args):
+        return False
+
+@InvertiblePredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    if exp.is_negative == False:
+        return ask(Q.invertible(base), assumptions)
+    return None
+
+@InvertiblePredicate.register(MatAdd)
+def _(expr, assumptions):
+    return None
+
+@InvertiblePredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    if Q.invertible(expr) in conjuncts(assumptions):
+        return True
+
+@InvertiblePredicate.register_many(Identity, Inverse)
+def _(expr, assumptions):
+    return True
+
+@InvertiblePredicate.register(ZeroMatrix)
+def _(expr, assumptions):
+    return False
+
+@InvertiblePredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@InvertiblePredicate.register(Transpose)
+def _(expr, assumptions):
+    return ask(Q.invertible(expr.arg), assumptions)
+
+@InvertiblePredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.invertible(expr.parent), assumptions)
+
+@InvertiblePredicate.register(MatrixBase)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    return expr.rank() == expr.rows
+
+@InvertiblePredicate.register(MatrixExpr)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    return None
+
+@InvertiblePredicate.register(BlockMatrix)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    if expr.blockshape == (1, 1):
+        return ask(Q.invertible(expr.blocks[0, 0]), assumptions)
+    expr = reblock_2x2(expr)
+    if expr.blockshape == (2, 2):
+        [[A, B], [C, D]] = expr.blocks.tolist()
+        if ask(Q.invertible(A), assumptions) == True:
+            invertible = ask(Q.invertible(D - C * A.I * B), assumptions)
+            if invertible is not None:
+                return invertible
+        if ask(Q.invertible(B), assumptions) == True:
+            invertible = ask(Q.invertible(C - D * B.I * A), assumptions)
+            if invertible is not None:
+                return invertible
+        if ask(Q.invertible(C), assumptions) == True:
+            invertible = ask(Q.invertible(B - A * C.I * D), assumptions)
+            if invertible is not None:
+                return invertible
+        if ask(Q.invertible(D), assumptions) == True:
+            invertible = ask(Q.invertible(A - B * D.I * C), assumptions)
+            if invertible is not None:
+                return invertible
+    return None
+
+@InvertiblePredicate.register(BlockDiagMatrix)
+def _(expr, assumptions):
+    if expr.rowblocksizes != expr.colblocksizes:
+        return None
+    return fuzzy_and([ask(Q.invertible(a), assumptions) for a in expr.diag])
+
+
+# OrthogonalPredicate
+
+@OrthogonalPredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, mmul = expr.as_coeff_mmul()
+    if (all(ask(Q.orthogonal(arg), assumptions) for arg in mmul.args) and
+            factor == 1):
+        return True
+    if any(ask(Q.invertible(arg), assumptions) is False
+            for arg in mmul.args):
+        return False
+
+@OrthogonalPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if int_exp:
+        return ask(Q.orthogonal(base), assumptions)
+    return None
+
+@OrthogonalPredicate.register(MatAdd)
+def _(expr, assumptions):
+    if (len(expr.args) == 1 and
+            ask(Q.orthogonal(expr.args[0]), assumptions)):
+        return True
+
+@OrthogonalPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if (not expr.is_square or
+                    ask(Q.invertible(expr), assumptions) is False):
+        return False
+    if Q.orthogonal(expr) in conjuncts(assumptions):
+        return True
+
+@OrthogonalPredicate.register(Identity)
+def _(expr, assumptions):
+    return True
+
+@OrthogonalPredicate.register(ZeroMatrix)
+def _(expr, assumptions):
+    return False
+
+@OrthogonalPredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.orthogonal(expr.arg), assumptions)
+
+@OrthogonalPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.orthogonal(expr.parent), assumptions)
+
+@OrthogonalPredicate.register(Factorization)
+def _(expr, assumptions):
+    return _Factorization(Q.orthogonal, expr, assumptions)
+
+
+# UnitaryPredicate
+
+@UnitaryPredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, mmul = expr.as_coeff_mmul()
+    if (all(ask(Q.unitary(arg), assumptions) for arg in mmul.args) and
+            abs(factor) == 1):
+        return True
+    if any(ask(Q.invertible(arg), assumptions) is False
+            for arg in mmul.args):
+        return False
+
+@UnitaryPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if int_exp:
+        return ask(Q.unitary(base), assumptions)
+    return None
+
+@UnitaryPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if (not expr.is_square or
+                    ask(Q.invertible(expr), assumptions) is False):
+        return False
+    if Q.unitary(expr) in conjuncts(assumptions):
+        return True
+
+@UnitaryPredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.unitary(expr.arg), assumptions)
+
+@UnitaryPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.unitary(expr.parent), assumptions)
+
+@UnitaryPredicate.register_many(DFT, Identity)
+def _(expr, assumptions):
+    return True
+
+@UnitaryPredicate.register(ZeroMatrix)
+def _(expr, assumptions):
+    return False
+
+@UnitaryPredicate.register(Factorization)
+def _(expr, assumptions):
+    return _Factorization(Q.unitary, expr, assumptions)
+
+
+# FullRankPredicate
+
+@FullRankPredicate.register(MatMul)
+def _(expr, assumptions):
+    if all(ask(Q.fullrank(arg), assumptions) for arg in expr.args):
+        return True
+
+@FullRankPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if int_exp and ask(~Q.negative(exp), assumptions):
+        return ask(Q.fullrank(base), assumptions)
+    return None
+
+@FullRankPredicate.register(Identity)
+def _(expr, assumptions):
+    return True
+
+@FullRankPredicate.register(ZeroMatrix)
+def _(expr, assumptions):
+    return False
+
+@FullRankPredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@FullRankPredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.fullrank(expr.arg), assumptions)
+
+@FullRankPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if ask(Q.orthogonal(expr.parent), assumptions):
+        return True
+
+
+# PositiveDefinitePredicate
+
+@PositiveDefinitePredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, mmul = expr.as_coeff_mmul()
+    if (all(ask(Q.positive_definite(arg), assumptions)
+            for arg in mmul.args) and factor > 0):
+        return True
+    if (len(mmul.args) >= 2
+            and mmul.args[0] == mmul.args[-1].T
+            and ask(Q.fullrank(mmul.args[0]), assumptions)):
+        return ask(Q.positive_definite(
+            MatMul(*mmul.args[1:-1])), assumptions)
+
+@PositiveDefinitePredicate.register(MatPow)
+def _(expr, assumptions):
+    # a power of a positive definite matrix is positive definite
+    if ask(Q.positive_definite(expr.args[0]), assumptions):
+        return True
+
+@PositiveDefinitePredicate.register(MatAdd)
+def _(expr, assumptions):
+    if all(ask(Q.positive_definite(arg), assumptions)
+            for arg in expr.args):
+        return True
+
+@PositiveDefinitePredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if not expr.is_square:
+        return False
+    if Q.positive_definite(expr) in conjuncts(assumptions):
+        return True
+
+@PositiveDefinitePredicate.register(Identity)
+def _(expr, assumptions):
+    return True
+
+@PositiveDefinitePredicate.register(ZeroMatrix)
+def _(expr, assumptions):
+    return False
+
+@PositiveDefinitePredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@PositiveDefinitePredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.positive_definite(expr.arg), assumptions)
+
+@PositiveDefinitePredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.positive_definite(expr.parent), assumptions)
+
+
+# UpperTriangularPredicate
+
+@UpperTriangularPredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, matrices = expr.as_coeff_matrices()
+    if all(ask(Q.upper_triangular(m), assumptions) for m in matrices):
+        return True
+
+@UpperTriangularPredicate.register(MatAdd)
+def _(expr, assumptions):
+    if all(ask(Q.upper_triangular(arg), assumptions) for arg in expr.args):
+        return True
+
+@UpperTriangularPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.upper_triangular(base), assumptions)
+    return None
+
+@UpperTriangularPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if Q.upper_triangular(expr) in conjuncts(assumptions):
+        return True
+
+@UpperTriangularPredicate.register_many(Identity, ZeroMatrix)
+def _(expr, assumptions):
+    return True
+
+@UpperTriangularPredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@UpperTriangularPredicate.register(Transpose)
+def _(expr, assumptions):
+    return ask(Q.lower_triangular(expr.arg), assumptions)
+
+@UpperTriangularPredicate.register(Inverse)
+def _(expr, assumptions):
+    return ask(Q.upper_triangular(expr.arg), assumptions)
+
+@UpperTriangularPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.upper_triangular(expr.parent), assumptions)
+
+@UpperTriangularPredicate.register(Factorization)
+def _(expr, assumptions):
+    return _Factorization(Q.upper_triangular, expr, assumptions)
+
+# LowerTriangularPredicate
+
+@LowerTriangularPredicate.register(MatMul)
+def _(expr, assumptions):
+    factor, matrices = expr.as_coeff_matrices()
+    if all(ask(Q.lower_triangular(m), assumptions) for m in matrices):
+        return True
+
+@LowerTriangularPredicate.register(MatAdd)
+def _(expr, assumptions):
+    if all(ask(Q.lower_triangular(arg), assumptions) for arg in expr.args):
+        return True
+
+@LowerTriangularPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.lower_triangular(base), assumptions)
+    return None
+
+@LowerTriangularPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if Q.lower_triangular(expr) in conjuncts(assumptions):
+        return True
+
+@LowerTriangularPredicate.register_many(Identity, ZeroMatrix)
+def _(expr, assumptions):
+    return True
+
+@LowerTriangularPredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@LowerTriangularPredicate.register(Transpose)
+def _(expr, assumptions):
+    return ask(Q.upper_triangular(expr.arg), assumptions)
+
+@LowerTriangularPredicate.register(Inverse)
+def _(expr, assumptions):
+    return ask(Q.lower_triangular(expr.arg), assumptions)
+
+@LowerTriangularPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.lower_triangular(expr.parent), assumptions)
+
+@LowerTriangularPredicate.register(Factorization)
+def _(expr, assumptions):
+    return _Factorization(Q.lower_triangular, expr, assumptions)
+
+
+# DiagonalPredicate
+
+def _is_empty_or_1x1(expr):
+    return expr.shape in ((0, 0), (1, 1))
+
+@DiagonalPredicate.register(MatMul)
+def _(expr, assumptions):
+    if _is_empty_or_1x1(expr):
+        return True
+    factor, matrices = expr.as_coeff_matrices()
+    if all(ask(Q.diagonal(m), assumptions) for m in matrices):
+        return True
+
+@DiagonalPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.diagonal(base), assumptions)
+    return None
+
+@DiagonalPredicate.register(MatAdd)
+def _(expr, assumptions):
+    if all(ask(Q.diagonal(arg), assumptions) for arg in expr.args):
+        return True
+
+@DiagonalPredicate.register(MatrixSymbol)
+def _(expr, assumptions):
+    if _is_empty_or_1x1(expr):
+        return True
+    if Q.diagonal(expr) in conjuncts(assumptions):
+        return True
+
+@DiagonalPredicate.register(OneMatrix)
+def _(expr, assumptions):
+    return expr.shape[0] == 1 and expr.shape[1] == 1
+
+@DiagonalPredicate.register_many(Inverse, Transpose)
+def _(expr, assumptions):
+    return ask(Q.diagonal(expr.arg), assumptions)
+
+@DiagonalPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    if _is_empty_or_1x1(expr):
+        return True
+    if not expr.on_diag:
+        return None
+    else:
+        return ask(Q.diagonal(expr.parent), assumptions)
+
+@DiagonalPredicate.register_many(DiagonalMatrix, DiagMatrix, Identity, ZeroMatrix)
+def _(expr, assumptions):
+    return True
+
+@DiagonalPredicate.register(Factorization)
+def _(expr, assumptions):
+    return _Factorization(Q.diagonal, expr, assumptions)
+
+
+# IntegerElementsPredicate
+
+def BM_elements(predicate, expr, assumptions):
+    """ Block Matrix elements. """
+    return all(ask(predicate(b), assumptions) for b in expr.blocks)
+
+def MS_elements(predicate, expr, assumptions):
+    """ Matrix Slice elements. """
+    return ask(predicate(expr.parent), assumptions)
+
+def MatMul_elements(matrix_predicate, scalar_predicate, expr, assumptions):
+    d = sift(expr.args, lambda x: isinstance(x, MatrixExpr))
+    factors, matrices = d[False], d[True]
+    return fuzzy_and([
+        test_closed_group(Basic(*factors), assumptions, scalar_predicate),
+        test_closed_group(Basic(*matrices), assumptions, matrix_predicate)])
+
+
+@IntegerElementsPredicate.register_many(Determinant, HadamardProduct, MatAdd,
+    Trace, Transpose)
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.integer_elements)
+
+@IntegerElementsPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    if exp.is_negative == False:
+        return ask(Q.integer_elements(base), assumptions)
+    return None
+
+@IntegerElementsPredicate.register_many(Identity, OneMatrix, ZeroMatrix)
+def _(expr, assumptions):
+    return True
+
+@IntegerElementsPredicate.register(MatMul)
+def _(expr, assumptions):
+    return MatMul_elements(Q.integer_elements, Q.integer, expr, assumptions)
+
+@IntegerElementsPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    return MS_elements(Q.integer_elements, expr, assumptions)
+
+@IntegerElementsPredicate.register(BlockMatrix)
+def _(expr, assumptions):
+    return BM_elements(Q.integer_elements, expr, assumptions)
+
+
+# RealElementsPredicate
+
+@RealElementsPredicate.register_many(Determinant, Factorization, HadamardProduct,
+    MatAdd, Trace, Transpose)
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.real_elements)
+
+@RealElementsPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.real_elements(base), assumptions)
+    return None
+
+@RealElementsPredicate.register(MatMul)
+def _(expr, assumptions):
+    return MatMul_elements(Q.real_elements, Q.real, expr, assumptions)
+
+@RealElementsPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    return MS_elements(Q.real_elements, expr, assumptions)
+
+@RealElementsPredicate.register(BlockMatrix)
+def _(expr, assumptions):
+    return BM_elements(Q.real_elements, expr, assumptions)
+
+
+# ComplexElementsPredicate
+
+@ComplexElementsPredicate.register_many(Determinant, Factorization, HadamardProduct,
+    Inverse, MatAdd, Trace, Transpose)
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.complex_elements)
+
+@ComplexElementsPredicate.register(MatPow)
+def _(expr, assumptions):
+    # only for integer powers
+    base, exp = expr.args
+    int_exp = ask(Q.integer(exp), assumptions)
+    if not int_exp:
+        return None
+    non_negative = ask(~Q.negative(exp), assumptions)
+    if (non_negative or non_negative == False
+                        and ask(Q.invertible(base), assumptions)):
+        return ask(Q.complex_elements(base), assumptions)
+    return None
+
+@ComplexElementsPredicate.register(MatMul)
+def _(expr, assumptions):
+    return MatMul_elements(Q.complex_elements, Q.complex, expr, assumptions)
+
+@ComplexElementsPredicate.register(MatrixSlice)
+def _(expr, assumptions):
+    return MS_elements(Q.complex_elements, expr, assumptions)
+
+@ComplexElementsPredicate.register(BlockMatrix)
+def _(expr, assumptions):
+    return BM_elements(Q.complex_elements, expr, assumptions)
+
+@ComplexElementsPredicate.register(DFT)
+def _(expr, assumptions):
+    return True

lib/python3.12/site-packages/sympy/assumptions/handlers/ntheory.py

@@ -0,0 +1,269 @@
+"""
+Handlers for keys related to number theory: prime, even, odd, etc.
+"""
+
+from sympy.assumptions import Q, ask
+from sympy.core import Add, Basic, Expr, Float, Mul, Pow, S
+from sympy.core.numbers import (ImaginaryUnit, Infinity, Integer, NaN,
+    NegativeInfinity, NumberSymbol, Rational, int_valued)
+from sympy.functions import Abs, im, re
+from sympy.ntheory import isprime
+
+from sympy.multipledispatch import MDNotImplementedError
+
+from ..predicates.ntheory import (PrimePredicate, CompositePredicate,
+    EvenPredicate, OddPredicate)
+
+
+# PrimePredicate
+
+def _PrimePredicate_number(expr, assumptions):
+    # helper method
+    exact = not expr.atoms(Float)
+    try:
+        i = int(expr.round())
+        if (expr - i).equals(0) is False:
+            raise TypeError
+    except TypeError:
+        return False
+    if exact:
+        return isprime(i)
+    # when not exact, we won't give a True or False
+    # since the number represents an approximate value
+
+@PrimePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_prime
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@PrimePredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _PrimePredicate_number(expr, assumptions)
+
+@PrimePredicate.register(Mul)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _PrimePredicate_number(expr, assumptions)
+    for arg in expr.args:
+        if not ask(Q.integer(arg), assumptions):
+            return None
+    for arg in expr.args:
+        if arg.is_number and arg.is_composite:
+            return False
+
+@PrimePredicate.register(Pow)
+def _(expr, assumptions):
+    """
+    Integer**Integer     -> !Prime
+    """
+    if expr.is_number:
+        return _PrimePredicate_number(expr, assumptions)
+    if ask(Q.integer(expr.exp), assumptions) and \
+            ask(Q.integer(expr.base), assumptions):
+        return False
+
+@PrimePredicate.register(Integer)
+def _(expr, assumptions):
+    return isprime(expr)
+
+@PrimePredicate.register_many(Rational, Infinity, NegativeInfinity, ImaginaryUnit)
+def _(expr, assumptions):
+    return False
+
+@PrimePredicate.register(Float)
+def _(expr, assumptions):
+    return _PrimePredicate_number(expr, assumptions)
+
+@PrimePredicate.register(NumberSymbol)
+def _(expr, assumptions):
+    return _PrimePredicate_number(expr, assumptions)
+
+@PrimePredicate.register(NaN)
+def _(expr, assumptions):
+    return None
+
+
+# CompositePredicate
+
+@CompositePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_composite
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@CompositePredicate.register(Basic)
+def _(expr, assumptions):
+    _positive = ask(Q.positive(expr), assumptions)
+    if _positive:
+        _integer = ask(Q.integer(expr), assumptions)
+        if _integer:
+            _prime = ask(Q.prime(expr), assumptions)
+            if _prime is None:
+                return
+            # Positive integer which is not prime is not
+            # necessarily composite
+            if expr.equals(1):
+                return False
+            return not _prime
+        else:
+            return _integer
+    else:
+        return _positive
+
+
+# EvenPredicate
+
+def _EvenPredicate_number(expr, assumptions):
+    # helper method
+    if isinstance(expr, (float, Float)):
+        if int_valued(expr):
+            return None
+        return False
+    try:
+        i = int(expr.round())
+    except TypeError:
+        return False
+    if not (expr - i).equals(0):
+        return False
+    return i % 2 == 0
+
+@EvenPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_even
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@EvenPredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _EvenPredicate_number(expr, assumptions)
+
+@EvenPredicate.register(Mul)
+def _(expr, assumptions):
+    """
+    Even * Integer    -> Even
+    Even * Odd        -> Even
+    Integer * Odd     -> ?
+    Odd * Odd         -> Odd
+    Even * Even       -> Even
+    Integer * Integer -> Even if Integer + Integer = Odd
+    otherwise         -> ?
+    """
+    if expr.is_number:
+        return _EvenPredicate_number(expr, assumptions)
+    even, odd, irrational, acc = False, 0, False, 1
+    for arg in expr.args:
+        # check for all integers and at least one even
+        if ask(Q.integer(arg), assumptions):
+            if ask(Q.even(arg), assumptions):
+                even = True
+            elif ask(Q.odd(arg), assumptions):
+                odd += 1
+            elif not even and acc != 1:
+                if ask(Q.odd(acc + arg), assumptions):
+                    even = True
+        elif ask(Q.irrational(arg), assumptions):
+            # one irrational makes the result False
+            # two makes it undefined
+            if irrational:
+                break
+            irrational = True
+        else:
+            break
+        acc = arg
+    else:
+        if irrational:
+            return False
+        if even:
+            return True
+        if odd == len(expr.args):
+            return False
+
+@EvenPredicate.register(Add)
+def _(expr, assumptions):
+    """
+    Even + Odd  -> Odd
+    Even + Even -> Even
+    Odd  + Odd  -> Even
+
+    """
+    if expr.is_number:
+        return _EvenPredicate_number(expr, assumptions)
+    _result = True
+    for arg in expr.args:
+        if ask(Q.even(arg), assumptions):
+            pass
+        elif ask(Q.odd(arg), assumptions):
+            _result = not _result
+        else:
+            break
+    else:
+        return _result
+
+@EvenPredicate.register(Pow)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _EvenPredicate_number(expr, assumptions)
+    if ask(Q.integer(expr.exp), assumptions):
+        if ask(Q.positive(expr.exp), assumptions):
+            return ask(Q.even(expr.base), assumptions)
+        elif ask(~Q.negative(expr.exp) & Q.odd(expr.base), assumptions):
+            return False
+        elif expr.base is S.NegativeOne:
+            return False
+
+@EvenPredicate.register(Integer)
+def _(expr, assumptions):
+    return not bool(expr.p & 1)
+
+@EvenPredicate.register_many(Rational, Infinity, NegativeInfinity, ImaginaryUnit)
+def _(expr, assumptions):
+    return False
+
+@EvenPredicate.register(NumberSymbol)
+def _(expr, assumptions):
+    return _EvenPredicate_number(expr, assumptions)
+
+@EvenPredicate.register(Abs)
+def _(expr, assumptions):
+    if ask(Q.real(expr.args[0]), assumptions):
+        return ask(Q.even(expr.args[0]), assumptions)
+
+@EvenPredicate.register(re)
+def _(expr, assumptions):
+    if ask(Q.real(expr.args[0]), assumptions):
+        return ask(Q.even(expr.args[0]), assumptions)
+
+@EvenPredicate.register(im)
+def _(expr, assumptions):
+    if ask(Q.real(expr.args[0]), assumptions):
+        return True
+
+@EvenPredicate.register(NaN)
+def _(expr, assumptions):
+    return None
+
+
+# OddPredicate
+
+@OddPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_odd
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@OddPredicate.register(Basic)
+def _(expr, assumptions):
+    _integer = ask(Q.integer(expr), assumptions)
+    if _integer:
+        _even = ask(Q.even(expr), assumptions)
+        if _even is None:
+            return None
+        return not _even
+    return _integer

lib/python3.12/site-packages/sympy/assumptions/handlers/order.py

@@ -0,0 +1,436 @@
+"""
+Handlers related to order relations: positive, negative, etc.
+"""
+
+from sympy.assumptions import Q, ask
+from sympy.core import Add, Basic, Expr, Mul, Pow
+from sympy.core.logic import fuzzy_not, fuzzy_and, fuzzy_or
+from sympy.core.numbers import E, ImaginaryUnit, NaN, I, pi
+from sympy.functions import Abs, acos, acot, asin, atan, exp, factorial, log
+from sympy.matrices import Determinant, Trace
+from sympy.matrices.expressions.matexpr import MatrixElement
+
+from sympy.multipledispatch import MDNotImplementedError
+
+from ..predicates.order import (NegativePredicate, NonNegativePredicate,
+    NonZeroPredicate, ZeroPredicate, NonPositivePredicate, PositivePredicate,
+    ExtendedNegativePredicate, ExtendedNonNegativePredicate,
+    ExtendedNonPositivePredicate, ExtendedNonZeroPredicate,
+    ExtendedPositivePredicate,)
+
+
+# NegativePredicate
+
+def _NegativePredicate_number(expr, assumptions):
+    r, i = expr.as_real_imag()
+    # If the imaginary part can symbolically be shown to be zero then
+    # we just evaluate the real part; otherwise we evaluate the imaginary
+    # part to see if it actually evaluates to zero and if it does then
+    # we make the comparison between the real part and zero.
+    if not i:
+        r = r.evalf(2)
+        if r._prec != 1:
+            return r < 0
+    else:
+        i = i.evalf(2)
+        if i._prec != 1:
+            if i != 0:
+                return False
+            r = r.evalf(2)
+            if r._prec != 1:
+                return r < 0
+
+@NegativePredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _NegativePredicate_number(expr, assumptions)
+
+@NegativePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_negative
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@NegativePredicate.register(Add)
+def _(expr, assumptions):
+    """
+    Positive + Positive -> Positive,
+    Negative + Negative -> Negative
+    """
+    if expr.is_number:
+        return _NegativePredicate_number(expr, assumptions)
+
+    r = ask(Q.real(expr), assumptions)
+    if r is not True:
+        return r
+
+    nonpos = 0
+    for arg in expr.args:
+        if ask(Q.negative(arg), assumptions) is not True:
+            if ask(Q.positive(arg), assumptions) is False:
+                nonpos += 1
+            else:
+                break
+    else:
+        if nonpos < len(expr.args):
+            return True
+
+@NegativePredicate.register(Mul)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _NegativePredicate_number(expr, assumptions)
+    result = None
+    for arg in expr.args:
+        if result is None:
+            result = False
+        if ask(Q.negative(arg), assumptions):
+            result = not result
+        elif ask(Q.positive(arg), assumptions):
+            pass
+        else:
+            return
+    return result
+
+@NegativePredicate.register(Pow)
+def _(expr, assumptions):
+    """
+    Real ** Even -> NonNegative
+    Real ** Odd  -> same_as_base
+    NonNegative ** Positive -> NonNegative
+    """
+    if expr.base == E:
+        # Exponential is always positive:
+        if ask(Q.real(expr.exp), assumptions):
+            return False
+        return
+
+    if expr.is_number:
+        return _NegativePredicate_number(expr, assumptions)
+    if ask(Q.real(expr.base), assumptions):
+        if ask(Q.positive(expr.base), assumptions):
+            if ask(Q.real(expr.exp), assumptions):
+                return False
+        if ask(Q.even(expr.exp), assumptions):
+            return False
+        if ask(Q.odd(expr.exp), assumptions):
+            return ask(Q.negative(expr.base), assumptions)
+
+@NegativePredicate.register_many(Abs, ImaginaryUnit)
+def _(expr, assumptions):
+    return False
+
+@NegativePredicate.register(exp)
+def _(expr, assumptions):
+    if ask(Q.real(expr.exp), assumptions):
+        return False
+    raise MDNotImplementedError
+
+
+# NonNegativePredicate
+
+@NonNegativePredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        notnegative = fuzzy_not(_NegativePredicate_number(expr, assumptions))
+        if notnegative:
+            return ask(Q.real(expr), assumptions)
+        else:
+            return notnegative
+
+@NonNegativePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_nonnegative
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+
+# NonZeroPredicate
+
+@NonZeroPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_nonzero
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@NonZeroPredicate.register(Basic)
+def _(expr, assumptions):
+    if ask(Q.real(expr)) is False:
+        return False
+    if expr.is_number:
+        # if there are no symbols just evalf
+        i = expr.evalf(2)
+        def nonz(i):
+            if i._prec != 1:
+                return i != 0
+        return fuzzy_or(nonz(i) for i in i.as_real_imag())
+
+@NonZeroPredicate.register(Add)
+def _(expr, assumptions):
+    if all(ask(Q.positive(x), assumptions) for x in expr.args) \
+            or all(ask(Q.negative(x), assumptions) for x in expr.args):
+        return True
+
+@NonZeroPredicate.register(Mul)
+def _(expr, assumptions):
+    for arg in expr.args:
+        result = ask(Q.nonzero(arg), assumptions)
+        if result:
+            continue
+        return result
+    return True
+
+@NonZeroPredicate.register(Pow)
+def _(expr, assumptions):
+    return ask(Q.nonzero(expr.base), assumptions)
+
+@NonZeroPredicate.register(Abs)
+def _(expr, assumptions):
+    return ask(Q.nonzero(expr.args[0]), assumptions)
+
+@NonZeroPredicate.register(NaN)
+def _(expr, assumptions):
+    return None
+
+
+# ZeroPredicate
+
+@ZeroPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_zero
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@ZeroPredicate.register(Basic)
+def _(expr, assumptions):
+    return fuzzy_and([fuzzy_not(ask(Q.nonzero(expr), assumptions)),
+        ask(Q.real(expr), assumptions)])
+
+@ZeroPredicate.register(Mul)
+def _(expr, assumptions):
+    # TODO: This should be deducible from the nonzero handler
+    return fuzzy_or(ask(Q.zero(arg), assumptions) for arg in expr.args)
+
+
+# NonPositivePredicate
+
+@NonPositivePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_nonpositive
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@NonPositivePredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        notpositive = fuzzy_not(_PositivePredicate_number(expr, assumptions))
+        if notpositive:
+            return ask(Q.real(expr), assumptions)
+        else:
+            return notpositive
+
+
+# PositivePredicate
+
+def _PositivePredicate_number(expr, assumptions):
+    r, i = expr.as_real_imag()
+    # If the imaginary part can symbolically be shown to be zero then
+    # we just evaluate the real part; otherwise we evaluate the imaginary
+    # part to see if it actually evaluates to zero and if it does then
+    # we make the comparison between the real part and zero.
+    if not i:
+        r = r.evalf(2)
+        if r._prec != 1:
+            return r > 0
+    else:
+        i = i.evalf(2)
+        if i._prec != 1:
+            if i != 0:
+                return False
+            r = r.evalf(2)
+            if r._prec != 1:
+                return r > 0
+
+@PositivePredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_positive
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@PositivePredicate.register(Basic)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _PositivePredicate_number(expr, assumptions)
+
+@PositivePredicate.register(Mul)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _PositivePredicate_number(expr, assumptions)
+    result = True
+    for arg in expr.args:
+        if ask(Q.positive(arg), assumptions):
+            continue
+        elif ask(Q.negative(arg), assumptions):
+            result = result ^ True
+        else:
+            return
+    return result
+
+@PositivePredicate.register(Add)
+def _(expr, assumptions):
+    if expr.is_number:
+        return _PositivePredicate_number(expr, assumptions)
+
+    r = ask(Q.real(expr), assumptions)
+    if r is not True:
+        return r
+
+    nonneg = 0
+    for arg in expr.args:
+        if ask(Q.positive(arg), assumptions) is not True:
+            if ask(Q.negative(arg), assumptions) is False:
+                nonneg += 1
+            else:
+                break
+    else:
+        if nonneg < len(expr.args):
+            return True
+
+@PositivePredicate.register(Pow)
+def _(expr, assumptions):
+    if expr.base == E:
+        if ask(Q.real(expr.exp), assumptions):
+            return True
+        if ask(Q.imaginary(expr.exp), assumptions):
+            return ask(Q.even(expr.exp/(I*pi)), assumptions)
+        return
+
+    if expr.is_number:
+        return _PositivePredicate_number(expr, assumptions)
+    if ask(Q.positive(expr.base), assumptions):
+        if ask(Q.real(expr.exp), assumptions):
+            return True
+    if ask(Q.negative(expr.base), assumptions):
+        if ask(Q.even(expr.exp), assumptions):
+            return True
+        if ask(Q.odd(expr.exp), assumptions):
+            return False
+
+@PositivePredicate.register(exp)
+def _(expr, assumptions):
+    if ask(Q.real(expr.exp), assumptions):
+        return True
+    if ask(Q.imaginary(expr.exp), assumptions):
+        return ask(Q.even(expr.exp/(I*pi)), assumptions)
+
+@PositivePredicate.register(log)
+def _(expr, assumptions):
+    r = ask(Q.real(expr.args[0]), assumptions)
+    if r is not True:
+        return r
+    if ask(Q.positive(expr.args[0] - 1), assumptions):
+        return True
+    if ask(Q.negative(expr.args[0] - 1), assumptions):
+        return False
+
+@PositivePredicate.register(factorial)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.integer(x) & Q.positive(x), assumptions):
+            return True
+
+@PositivePredicate.register(ImaginaryUnit)
+def _(expr, assumptions):
+    return False
+
+@PositivePredicate.register(Abs)
+def _(expr, assumptions):
+    return ask(Q.nonzero(expr), assumptions)
+
+@PositivePredicate.register(Trace)
+def _(expr, assumptions):
+    if ask(Q.positive_definite(expr.arg), assumptions):
+        return True
+
+@PositivePredicate.register(Determinant)
+def _(expr, assumptions):
+    if ask(Q.positive_definite(expr.arg), assumptions):
+        return True
+
+@PositivePredicate.register(MatrixElement)
+def _(expr, assumptions):
+    if (expr.i == expr.j
+            and ask(Q.positive_definite(expr.parent), assumptions)):
+        return True
+
+@PositivePredicate.register(atan)
+def _(expr, assumptions):
+    return ask(Q.positive(expr.args[0]), assumptions)
+
+@PositivePredicate.register(asin)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.positive(x) & Q.nonpositive(x - 1), assumptions):
+        return True
+    if ask(Q.negative(x) & Q.nonnegative(x + 1), assumptions):
+        return False
+
+@PositivePredicate.register(acos)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.nonpositive(x - 1) & Q.nonnegative(x + 1), assumptions):
+        return True
+
+@PositivePredicate.register(acot)
+def _(expr, assumptions):
+    return ask(Q.real(expr.args[0]), assumptions)
+
+@PositivePredicate.register(NaN)
+def _(expr, assumptions):
+    return None
+
+
+# ExtendedNegativePredicate
+
+@ExtendedNegativePredicate.register(object)
+def _(expr, assumptions):
+    return ask(Q.negative(expr) | Q.negative_infinite(expr), assumptions)
+
+
+# ExtendedPositivePredicate
+
+@ExtendedPositivePredicate.register(object)
+def _(expr, assumptions):
+    return ask(Q.positive(expr) | Q.positive_infinite(expr), assumptions)
+
+
+# ExtendedNonZeroPredicate
+
+@ExtendedNonZeroPredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.negative_infinite(expr) | Q.negative(expr) | Q.positive(expr) | Q.positive_infinite(expr),
+        assumptions)
+
+
+# ExtendedNonPositivePredicate
+
+@ExtendedNonPositivePredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.negative_infinite(expr) | Q.negative(expr) | Q.zero(expr),
+        assumptions)
+
+
+# ExtendedNonNegativePredicate
+
+@ExtendedNonNegativePredicate.register(object)
+def _(expr, assumptions):
+    return ask(
+        Q.zero(expr) | Q.positive(expr) | Q.positive_infinite(expr),
+        assumptions)

lib/python3.12/site-packages/sympy/assumptions/handlers/sets.py

@@ -0,0 +1,772 @@
+"""
+Handlers for predicates related to set membership: integer, rational, etc.
+"""
+
+from sympy.assumptions import Q, ask
+from sympy.core import Add, Basic, Expr, Mul, Pow, S
+from sympy.core.numbers import (AlgebraicNumber, ComplexInfinity, Exp1, Float,
+    GoldenRatio, ImaginaryUnit, Infinity, Integer, NaN, NegativeInfinity,
+    Number, NumberSymbol, Pi, pi, Rational, TribonacciConstant, E)
+from sympy.core.logic import fuzzy_bool
+from sympy.functions import (Abs, acos, acot, asin, atan, cos, cot, exp, im,
+    log, re, sin, tan)
+from sympy.core.numbers import I
+from sympy.core.relational import Eq
+from sympy.functions.elementary.complexes import conjugate
+from sympy.matrices import Determinant, MatrixBase, Trace
+from sympy.matrices.expressions.matexpr import MatrixElement
+
+from sympy.multipledispatch import MDNotImplementedError
+
+from .common import test_closed_group
+from ..predicates.sets import (IntegerPredicate, RationalPredicate,
+    IrrationalPredicate, RealPredicate, ExtendedRealPredicate,
+    HermitianPredicate, ComplexPredicate, ImaginaryPredicate,
+    AntihermitianPredicate, AlgebraicPredicate)
+
+
+# IntegerPredicate
+
+def _IntegerPredicate_number(expr, assumptions):
+    # helper function
+        try:
+            i = int(expr.round())
+            if not (expr - i).equals(0):
+                raise TypeError
+            return True
+        except TypeError:
+            return False
+
+@IntegerPredicate.register_many(int, Integer) # type:ignore
+def _(expr, assumptions):
+    return True
+
+@IntegerPredicate.register_many(Exp1, GoldenRatio, ImaginaryUnit, Infinity,
+        NegativeInfinity, Pi, Rational, TribonacciConstant)
+def _(expr, assumptions):
+    return False
+
+@IntegerPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_integer
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@IntegerPredicate.register_many(Add, Pow)
+def _(expr, assumptions):
+    """
+    * Integer + Integer       -> Integer
+    * Integer + !Integer      -> !Integer
+    * !Integer + !Integer -> ?
+    """
+    if expr.is_number:
+        return _IntegerPredicate_number(expr, assumptions)
+    return test_closed_group(expr, assumptions, Q.integer)
+
+@IntegerPredicate.register(Mul)
+def _(expr, assumptions):
+    """
+    * Integer*Integer      -> Integer
+    * Integer*Irrational   -> !Integer
+    * Odd/Even             -> !Integer
+    * Integer*Rational     -> ?
+    """
+    if expr.is_number:
+        return _IntegerPredicate_number(expr, assumptions)
+    _output = True
+    for arg in expr.args:
+        if not ask(Q.integer(arg), assumptions):
+            if arg.is_Rational:
+                if arg.q == 2:
+                    return ask(Q.even(2*expr), assumptions)
+                if ~(arg.q & 1):
+                    return None
+            elif ask(Q.irrational(arg), assumptions):
+                if _output:
+                    _output = False
+                else:
+                    return
+            else:
+                return
+
+    return _output
+
+@IntegerPredicate.register(Abs)
+def _(expr, assumptions):
+    return ask(Q.integer(expr.args[0]), assumptions)
+
+@IntegerPredicate.register_many(Determinant, MatrixElement, Trace)
+def _(expr, assumptions):
+    return ask(Q.integer_elements(expr.args[0]), assumptions)
+
+
+# RationalPredicate
+
+@RationalPredicate.register(Rational)
+def _(expr, assumptions):
+    return True
+
+@RationalPredicate.register(Float)
+def _(expr, assumptions):
+    return None
+
+@RationalPredicate.register_many(Exp1, GoldenRatio, ImaginaryUnit, Infinity,
+    NegativeInfinity, Pi, TribonacciConstant)
+def _(expr, assumptions):
+    return False
+
+@RationalPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_rational
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@RationalPredicate.register_many(Add, Mul)
+def _(expr, assumptions):
+    """
+    * Rational + Rational     -> Rational
+    * Rational + !Rational    -> !Rational
+    * !Rational + !Rational   -> ?
+    """
+    if expr.is_number:
+        if expr.as_real_imag()[1]:
+            return False
+    return test_closed_group(expr, assumptions, Q.rational)
+
+@RationalPredicate.register(Pow)
+def _(expr, assumptions):
+    """
+    * Rational ** Integer      -> Rational
+    * Irrational ** Rational   -> Irrational
+    * Rational ** Irrational   -> ?
+    """
+    if expr.base == E:
+        x = expr.exp
+        if ask(Q.rational(x), assumptions):
+            return ask(~Q.nonzero(x), assumptions)
+        return
+
+    if ask(Q.integer(expr.exp), assumptions):
+        return ask(Q.rational(expr.base), assumptions)
+    elif ask(Q.rational(expr.exp), assumptions):
+        if ask(Q.prime(expr.base), assumptions):
+            return False
+
+@RationalPredicate.register_many(asin, atan, cos, sin, tan)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.rational(x), assumptions):
+        return ask(~Q.nonzero(x), assumptions)
+
+@RationalPredicate.register(exp)
+def _(expr, assumptions):
+    x = expr.exp
+    if ask(Q.rational(x), assumptions):
+        return ask(~Q.nonzero(x), assumptions)
+
+@RationalPredicate.register_many(acot, cot)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.rational(x), assumptions):
+        return False
+
+@RationalPredicate.register_many(acos, log)
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.rational(x), assumptions):
+        return ask(~Q.nonzero(x - 1), assumptions)
+
+
+# IrrationalPredicate
+
+@IrrationalPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_irrational
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@IrrationalPredicate.register(Basic)
+def _(expr, assumptions):
+    _real = ask(Q.real(expr), assumptions)
+    if _real:
+        _rational = ask(Q.rational(expr), assumptions)
+        if _rational is None:
+            return None
+        return not _rational
+    else:
+        return _real
+
+
+# RealPredicate
+
+def _RealPredicate_number(expr, assumptions):
+    # let as_real_imag() work first since the expression may
+    # be simpler to evaluate
+    i = expr.as_real_imag()[1].evalf(2)
+    if i._prec != 1:
+        return not i
+    # allow None to be returned if we couldn't show for sure
+    # that i was 0
+
+@RealPredicate.register_many(Abs, Exp1, Float, GoldenRatio, im, Pi, Rational,
+    re, TribonacciConstant)
+def _(expr, assumptions):
+    return True
+
+@RealPredicate.register_many(ImaginaryUnit, Infinity, NegativeInfinity)
+def _(expr, assumptions):
+    return False
+
+@RealPredicate.register(Expr)
+def _(expr, assumptions):
+    ret = expr.is_real
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@RealPredicate.register(Add)
+def _(expr, assumptions):
+    """
+    * Real + Real              -> Real
+    * Real + (Complex & !Real) -> !Real
+    """
+    if expr.is_number:
+        return _RealPredicate_number(expr, assumptions)
+    return test_closed_group(expr, assumptions, Q.real)
+
+@RealPredicate.register(Mul)
+def _(expr, assumptions):
+    """
+    * Real*Real               -> Real
+    * Real*Imaginary          -> !Real
+    * Imaginary*Imaginary     -> Real
+    """
+    if expr.is_number:
+        return _RealPredicate_number(expr, assumptions)
+    result = True
+    for arg in expr.args:
+        if ask(Q.real(arg), assumptions):
+            pass
+        elif ask(Q.imaginary(arg), assumptions):
+            result = result ^ True
+        else:
+            break
+    else:
+        return result
+
+@RealPredicate.register(Pow)
+def _(expr, assumptions):
+    """
+    * Real**Integer              -> Real
+    * Positive**Real             -> Real
+    * Real**(Integer/Even)       -> Real if base is nonnegative
+    * Real**(Integer/Odd)        -> Real
+    * Imaginary**(Integer/Even)  -> Real
+    * Imaginary**(Integer/Odd)   -> not Real
+    * Imaginary**Real            -> ? since Real could be 0 (giving real)
+                                    or 1 (giving imaginary)
+    * b**Imaginary               -> Real if log(b) is imaginary and b != 0
+                                    and exponent != integer multiple of
+                                    I*pi/log(b)
+    * Real**Real                 -> ? e.g. sqrt(-1) is imaginary and
+                                    sqrt(2) is not
+    """
+    if expr.is_number:
+        return _RealPredicate_number(expr, assumptions)
+
+    if expr.base == E:
+        return ask(
+            Q.integer(expr.exp/I/pi) | Q.real(expr.exp), assumptions
+        )
+
+    if expr.base.func == exp or (expr.base.is_Pow and expr.base.base == E):
+        if ask(Q.imaginary(expr.base.exp), assumptions):
+            if ask(Q.imaginary(expr.exp), assumptions):
+                return True
+        # If the i = (exp's arg)/(I*pi) is an integer or half-integer
+        # multiple of I*pi then 2*i will be an integer. In addition,
+        # exp(i*I*pi) = (-1)**i so the overall realness of the expr
+        # can be determined by replacing exp(i*I*pi) with (-1)**i.
+        i = expr.base.exp/I/pi
+        if ask(Q.integer(2*i), assumptions):
+            return ask(Q.real((S.NegativeOne**i)**expr.exp), assumptions)
+        return
+
+    if ask(Q.imaginary(expr.base), assumptions):
+        if ask(Q.integer(expr.exp), assumptions):
+            odd = ask(Q.odd(expr.exp), assumptions)
+            if odd is not None:
+                return not odd
+            return
+
+    if ask(Q.imaginary(expr.exp), assumptions):
+        imlog = ask(Q.imaginary(log(expr.base)), assumptions)
+        if imlog is not None:
+            # I**i -> real, log(I) is imag;
+            # (2*I)**i -> complex, log(2*I) is not imag
+            return imlog
+
+    if ask(Q.real(expr.base), assumptions):
+        if ask(Q.real(expr.exp), assumptions):
+            if expr.exp.is_Rational and \
+                    ask(Q.even(expr.exp.q), assumptions):
+                return ask(Q.positive(expr.base), assumptions)
+            elif ask(Q.integer(expr.exp), assumptions):
+                return True
+            elif ask(Q.positive(expr.base), assumptions):
+                return True
+            elif ask(Q.negative(expr.base), assumptions):
+                return False
+
+@RealPredicate.register_many(cos, sin)
+def _(expr, assumptions):
+    if ask(Q.real(expr.args[0]), assumptions):
+            return True
+
+@RealPredicate.register(exp)
+def _(expr, assumptions):
+    return ask(
+        Q.integer(expr.exp/I/pi) | Q.real(expr.exp), assumptions
+    )
+
+@RealPredicate.register(log)
+def _(expr, assumptions):
+    return ask(Q.positive(expr.args[0]), assumptions)
+
+@RealPredicate.register_many(Determinant, MatrixElement, Trace)
+def _(expr, assumptions):
+    return ask(Q.real_elements(expr.args[0]), assumptions)
+
+
+# ExtendedRealPredicate
+
+@ExtendedRealPredicate.register(object)
+def _(expr, assumptions):
+    return ask(Q.negative_infinite(expr)
+               | Q.negative(expr)
+               | Q.zero(expr)
+               | Q.positive(expr)
+               | Q.positive_infinite(expr),
+            assumptions)
+
+@ExtendedRealPredicate.register_many(Infinity, NegativeInfinity)
+def _(expr, assumptions):
+    return True
+
+@ExtendedRealPredicate.register_many(Add, Mul, Pow) # type:ignore
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.extended_real)
+
+
+# HermitianPredicate
+
+@HermitianPredicate.register(object) # type:ignore
+def _(expr, assumptions):
+    if isinstance(expr, MatrixBase):
+        return None
+    return ask(Q.real(expr), assumptions)
+
+@HermitianPredicate.register(Add) # type:ignore
+def _(expr, assumptions):
+    """
+    * Hermitian + Hermitian  -> Hermitian
+    * Hermitian + !Hermitian -> !Hermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    return test_closed_group(expr, assumptions, Q.hermitian)
+
+@HermitianPredicate.register(Mul) # type:ignore
+def _(expr, assumptions):
+    """
+    As long as there is at most only one noncommutative term:
+
+    * Hermitian*Hermitian         -> Hermitian
+    * Hermitian*Antihermitian     -> !Hermitian
+    * Antihermitian*Antihermitian -> Hermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    nccount = 0
+    result = True
+    for arg in expr.args:
+        if ask(Q.antihermitian(arg), assumptions):
+            result = result ^ True
+        elif not ask(Q.hermitian(arg), assumptions):
+            break
+        if ask(~Q.commutative(arg), assumptions):
+            nccount += 1
+            if nccount > 1:
+                break
+    else:
+        return result
+
+@HermitianPredicate.register(Pow) # type:ignore
+def _(expr, assumptions):
+    """
+    * Hermitian**Integer -> Hermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    if expr.base == E:
+        if ask(Q.hermitian(expr.exp), assumptions):
+            return True
+        raise MDNotImplementedError
+    if ask(Q.hermitian(expr.base), assumptions):
+        if ask(Q.integer(expr.exp), assumptions):
+            return True
+    raise MDNotImplementedError
+
+@HermitianPredicate.register_many(cos, sin) # type:ignore
+def _(expr, assumptions):
+    if ask(Q.hermitian(expr.args[0]), assumptions):
+        return True
+    raise MDNotImplementedError
+
+@HermitianPredicate.register(exp) # type:ignore
+def _(expr, assumptions):
+    if ask(Q.hermitian(expr.exp), assumptions):
+        return True
+    raise MDNotImplementedError
+
+@HermitianPredicate.register(MatrixBase) # type:ignore
+def _(mat, assumptions):
+    rows, cols = mat.shape
+    ret_val = True
+    for i in range(rows):
+        for j in range(i, cols):
+            cond = fuzzy_bool(Eq(mat[i, j], conjugate(mat[j, i])))
+            if cond is None:
+                ret_val = None
+            if cond == False:
+                return False
+    if ret_val is None:
+        raise MDNotImplementedError
+    return ret_val
+
+
+# ComplexPredicate
+
+@ComplexPredicate.register_many(Abs, cos, exp, im, ImaginaryUnit, log, Number, # type:ignore
+    NumberSymbol, re, sin)
+def _(expr, assumptions):
+    return True
+
+@ComplexPredicate.register_many(Infinity, NegativeInfinity) # type:ignore
+def _(expr, assumptions):
+    return False
+
+@ComplexPredicate.register(Expr) # type:ignore
+def _(expr, assumptions):
+    ret = expr.is_complex
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@ComplexPredicate.register_many(Add, Mul) # type:ignore
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.complex)
+
+@ComplexPredicate.register(Pow) # type:ignore
+def _(expr, assumptions):
+    if expr.base == E:
+        return True
+    return test_closed_group(expr, assumptions, Q.complex)
+
+@ComplexPredicate.register_many(Determinant, MatrixElement, Trace) # type:ignore
+def _(expr, assumptions):
+    return ask(Q.complex_elements(expr.args[0]), assumptions)
+
+@ComplexPredicate.register(NaN) # type:ignore
+def _(expr, assumptions):
+    return None
+
+
+# ImaginaryPredicate
+
+def _Imaginary_number(expr, assumptions):
+    # let as_real_imag() work first since the expression may
+    # be simpler to evaluate
+    r = expr.as_real_imag()[0].evalf(2)
+    if r._prec != 1:
+        return not r
+    # allow None to be returned if we couldn't show for sure
+    # that r was 0
+
+@ImaginaryPredicate.register(ImaginaryUnit) # type:ignore
+def _(expr, assumptions):
+    return True
+
+@ImaginaryPredicate.register(Expr) # type:ignore
+def _(expr, assumptions):
+    ret = expr.is_imaginary
+    if ret is None:
+        raise MDNotImplementedError
+    return ret
+
+@ImaginaryPredicate.register(Add) # type:ignore
+def _(expr, assumptions):
+    """
+    * Imaginary + Imaginary -> Imaginary
+    * Imaginary + Complex   -> ?
+    * Imaginary + Real      -> !Imaginary
+    """
+    if expr.is_number:
+        return _Imaginary_number(expr, assumptions)
+
+    reals = 0
+    for arg in expr.args:
+        if ask(Q.imaginary(arg), assumptions):
+            pass
+        elif ask(Q.real(arg), assumptions):
+            reals += 1
+        else:
+            break
+    else:
+        if reals == 0:
+            return True
+        if reals in (1, len(expr.args)):
+            # two reals could sum 0 thus giving an imaginary
+            return False
+
+@ImaginaryPredicate.register(Mul) # type:ignore
+def _(expr, assumptions):
+    """
+    * Real*Imaginary      -> Imaginary
+    * Imaginary*Imaginary -> Real
+    """
+    if expr.is_number:
+        return _Imaginary_number(expr, assumptions)
+    result = False
+    reals = 0
+    for arg in expr.args:
+        if ask(Q.imaginary(arg), assumptions):
+            result = result ^ True
+        elif not ask(Q.real(arg), assumptions):
+            break
+    else:
+        if reals == len(expr.args):
+            return False
+        return result
+
+@ImaginaryPredicate.register(Pow) # type:ignore
+def _(expr, assumptions):
+    """
+    * Imaginary**Odd        -> Imaginary
+    * Imaginary**Even       -> Real
+    * b**Imaginary          -> !Imaginary if exponent is an integer
+                               multiple of I*pi/log(b)
+    * Imaginary**Real       -> ?
+    * Positive**Real        -> Real
+    * Negative**Integer     -> Real
+    * Negative**(Integer/2) -> Imaginary
+    * Negative**Real        -> not Imaginary if exponent is not Rational
+    """
+    if expr.is_number:
+        return _Imaginary_number(expr, assumptions)
+
+    if expr.base == E:
+        a = expr.exp/I/pi
+        return ask(Q.integer(2*a) & ~Q.integer(a), assumptions)
+
+    if expr.base.func == exp or (expr.base.is_Pow and expr.base.base == E):
+        if ask(Q.imaginary(expr.base.exp), assumptions):
+            if ask(Q.imaginary(expr.exp), assumptions):
+                return False
+            i = expr.base.exp/I/pi
+            if ask(Q.integer(2*i), assumptions):
+                return ask(Q.imaginary((S.NegativeOne**i)**expr.exp), assumptions)
+
+    if ask(Q.imaginary(expr.base), assumptions):
+        if ask(Q.integer(expr.exp), assumptions):
+            odd = ask(Q.odd(expr.exp), assumptions)
+            if odd is not None:
+                return odd
+            return
+
+    if ask(Q.imaginary(expr.exp), assumptions):
+        imlog = ask(Q.imaginary(log(expr.base)), assumptions)
+        if imlog is not None:
+            # I**i -> real; (2*I)**i -> complex ==> not imaginary
+            return False
+
+    if ask(Q.real(expr.base) & Q.real(expr.exp), assumptions):
+        if ask(Q.positive(expr.base), assumptions):
+            return False
+        else:
+            rat = ask(Q.rational(expr.exp), assumptions)
+            if not rat:
+                return rat
+            if ask(Q.integer(expr.exp), assumptions):
+                return False
+            else:
+                half = ask(Q.integer(2*expr.exp), assumptions)
+                if half:
+                    return ask(Q.negative(expr.base), assumptions)
+                return half
+
+@ImaginaryPredicate.register(log) # type:ignore
+def _(expr, assumptions):
+    if ask(Q.real(expr.args[0]), assumptions):
+        if ask(Q.positive(expr.args[0]), assumptions):
+            return False
+        return
+    # XXX it should be enough to do
+    # return ask(Q.nonpositive(expr.args[0]), assumptions)
+    # but ask(Q.nonpositive(exp(x)), Q.imaginary(x)) -> None;
+    # it should return True since exp(x) will be either 0 or complex
+    if expr.args[0].func == exp or (expr.args[0].is_Pow and expr.args[0].base == E):
+        if expr.args[0].exp in [I, -I]:
+            return True
+    im = ask(Q.imaginary(expr.args[0]), assumptions)
+    if im is False:
+        return False
+
+@ImaginaryPredicate.register(exp) # type:ignore
+def _(expr, assumptions):
+    a = expr.exp/I/pi
+    return ask(Q.integer(2*a) & ~Q.integer(a), assumptions)
+
+@ImaginaryPredicate.register_many(Number, NumberSymbol) # type:ignore
+def _(expr, assumptions):
+    return not (expr.as_real_imag()[1] == 0)
+
+@ImaginaryPredicate.register(NaN) # type:ignore
+def _(expr, assumptions):
+    return None
+
+
+# AntihermitianPredicate
+
+@AntihermitianPredicate.register(object) # type:ignore
+def _(expr, assumptions):
+    if isinstance(expr, MatrixBase):
+        return None
+    if ask(Q.zero(expr), assumptions):
+        return True
+    return ask(Q.imaginary(expr), assumptions)
+
+@AntihermitianPredicate.register(Add) # type:ignore
+def _(expr, assumptions):
+    """
+    * Antihermitian + Antihermitian  -> Antihermitian
+    * Antihermitian + !Antihermitian -> !Antihermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    return test_closed_group(expr, assumptions, Q.antihermitian)
+
+@AntihermitianPredicate.register(Mul) # type:ignore
+def _(expr, assumptions):
+    """
+    As long as there is at most only one noncommutative term:
+
+    * Hermitian*Hermitian         -> !Antihermitian
+    * Hermitian*Antihermitian     -> Antihermitian
+    * Antihermitian*Antihermitian -> !Antihermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    nccount = 0
+    result = False
+    for arg in expr.args:
+        if ask(Q.antihermitian(arg), assumptions):
+            result = result ^ True
+        elif not ask(Q.hermitian(arg), assumptions):
+            break
+        if ask(~Q.commutative(arg), assumptions):
+            nccount += 1
+            if nccount > 1:
+                break
+    else:
+        return result
+
+@AntihermitianPredicate.register(Pow) # type:ignore
+def _(expr, assumptions):
+    """
+    * Hermitian**Integer  -> !Antihermitian
+    * Antihermitian**Even -> !Antihermitian
+    * Antihermitian**Odd  -> Antihermitian
+    """
+    if expr.is_number:
+        raise MDNotImplementedError
+    if ask(Q.hermitian(expr.base), assumptions):
+        if ask(Q.integer(expr.exp), assumptions):
+            return False
+    elif ask(Q.antihermitian(expr.base), assumptions):
+        if ask(Q.even(expr.exp), assumptions):
+            return False
+        elif ask(Q.odd(expr.exp), assumptions):
+            return True
+    raise MDNotImplementedError
+
+@AntihermitianPredicate.register(MatrixBase) # type:ignore
+def _(mat, assumptions):
+    rows, cols = mat.shape
+    ret_val = True
+    for i in range(rows):
+        for j in range(i, cols):
+            cond = fuzzy_bool(Eq(mat[i, j], -conjugate(mat[j, i])))
+            if cond is None:
+                ret_val = None
+            if cond == False:
+                return False
+    if ret_val is None:
+        raise MDNotImplementedError
+    return ret_val
+
+
+# AlgebraicPredicate
+
+@AlgebraicPredicate.register_many(AlgebraicNumber, Float, GoldenRatio, # type:ignore
+    ImaginaryUnit, TribonacciConstant)
+def _(expr, assumptions):
+    return True
+
+@AlgebraicPredicate.register_many(ComplexInfinity, Exp1, Infinity, # type:ignore
+    NegativeInfinity, Pi)
+def _(expr, assumptions):
+    return False
+
+@AlgebraicPredicate.register_many(Add, Mul) # type:ignore
+def _(expr, assumptions):
+    return test_closed_group(expr, assumptions, Q.algebraic)
+
+@AlgebraicPredicate.register(Pow) # type:ignore
+def _(expr, assumptions):
+    if expr.base == E:
+        if ask(Q.algebraic(expr.exp), assumptions):
+            return ask(~Q.nonzero(expr.exp), assumptions)
+        return
+    return expr.exp.is_Rational and ask(Q.algebraic(expr.base), assumptions)
+
+@AlgebraicPredicate.register(Rational) # type:ignore
+def _(expr, assumptions):
+    return expr.q != 0
+
+@AlgebraicPredicate.register_many(asin, atan, cos, sin, tan) # type:ignore
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.algebraic(x), assumptions):
+        return ask(~Q.nonzero(x), assumptions)
+
+@AlgebraicPredicate.register(exp) # type:ignore
+def _(expr, assumptions):
+    x = expr.exp
+    if ask(Q.algebraic(x), assumptions):
+        return ask(~Q.nonzero(x), assumptions)
+
+@AlgebraicPredicate.register_many(acot, cot) # type:ignore
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.algebraic(x), assumptions):
+        return False
+
+@AlgebraicPredicate.register_many(acos, log) # type:ignore
+def _(expr, assumptions):
+    x = expr.args[0]
+    if ask(Q.algebraic(x), assumptions):
+        return ask(~Q.nonzero(x - 1), assumptions)

lib/python3.12/site-packages/sympy/assumptions/lra_satask.py

@@ -0,0 +1,286 @@
+from sympy.assumptions.assume import global_assumptions
+from sympy.assumptions.cnf import CNF, EncodedCNF
+from sympy.assumptions.ask import Q
+from sympy.logic.inference import satisfiable
+from sympy.logic.algorithms.lra_theory import UnhandledInput, ALLOWED_PRED
+from sympy.matrices.kind import MatrixKind
+from sympy.core.kind import NumberKind
+from sympy.assumptions.assume import AppliedPredicate
+from sympy.core.mul import Mul
+from sympy.core.singleton import S
+
+
+def lra_satask(proposition, assumptions=True, context=global_assumptions):
+    """
+    Function to evaluate the proposition with assumptions using SAT algorithm
+    in conjunction with an Linear Real Arithmetic theory solver.
+
+    Used to handle inequalities. Should eventually be depreciated and combined
+    into satask, but infinity handling and other things need to be implemented
+    before that can happen.
+    """
+    props = CNF.from_prop(proposition)
+    _props = CNF.from_prop(~proposition)
+
+    cnf = CNF.from_prop(assumptions)
+    assumptions = EncodedCNF()
+    assumptions.from_cnf(cnf)
+
+    context_cnf = CNF()
+    if context:
+        context_cnf = context_cnf.extend(context)
+
+    assumptions.add_from_cnf(context_cnf)
+
+    return check_satisfiability(props, _props, assumptions)
+
+# Some predicates such as Q.prime can't be handled by lra_satask.
+# For example, (x > 0) & (x < 1) & Q.prime(x) is unsat but lra_satask would think it was sat.
+# WHITE_LIST is a list of predicates that can always be handled.
+WHITE_LIST = ALLOWED_PRED | {Q.positive, Q.negative, Q.zero, Q.nonzero, Q.nonpositive, Q.nonnegative,
+                                            Q.extended_positive, Q.extended_negative, Q.extended_nonpositive,
+                                            Q.extended_negative, Q.extended_nonzero, Q.negative_infinite,
+                                            Q.positive_infinite}
+
+
+def check_satisfiability(prop, _prop, factbase):
+    sat_true = factbase.copy()
+    sat_false = factbase.copy()
+    sat_true.add_from_cnf(prop)
+    sat_false.add_from_cnf(_prop)
+
+    all_pred, all_exprs = get_all_pred_and_expr_from_enc_cnf(sat_true)
+
+    for pred in all_pred:
+        if pred.function not in WHITE_LIST and pred.function != Q.ne:
+            raise UnhandledInput(f"LRASolver: {pred} is an unhandled predicate")
+    for expr in all_exprs:
+        if expr.kind == MatrixKind(NumberKind):
+            raise UnhandledInput(f"LRASolver: {expr} is of MatrixKind")
+        if expr == S.NaN:
+            raise UnhandledInput("LRASolver: nan")
+
+    # convert old assumptions into predicates and add them to sat_true and sat_false
+    # also check for unhandled predicates
+    for assm in extract_pred_from_old_assum(all_exprs):
+        n = len(sat_true.encoding)
+        if assm not in sat_true.encoding:
+            sat_true.encoding[assm] = n+1
+        sat_true.data.append([sat_true.encoding[assm]])
+
+        n = len(sat_false.encoding)
+        if assm not in sat_false.encoding:
+            sat_false.encoding[assm] = n+1
+        sat_false.data.append([sat_false.encoding[assm]])
+
+
+    sat_true = _preprocess(sat_true)
+    sat_false = _preprocess(sat_false)
+
+    can_be_true = satisfiable(sat_true, use_lra_theory=True) is not False
+    can_be_false = satisfiable(sat_false, use_lra_theory=True) is not False
+
+    if can_be_true and can_be_false:
+        return None
+
+    if can_be_true and not can_be_false:
+        return True
+
+    if not can_be_true and can_be_false:
+        return False
+
+    if not can_be_true and not can_be_false:
+        raise ValueError("Inconsistent assumptions")
+
+
+def _preprocess(enc_cnf):
+    """
+    Returns an encoded cnf with only Q.eq, Q.gt, Q.lt,
+    Q.ge, and Q.le predicate.
+
+    Converts every unequality into a disjunction of strict
+    inequalities. For example, x != 3 would become
+    x < 3 OR x > 3.
+
+    Also converts all negated Q.ne predicates into
+    equalities.
+    """
+
+    # loops through each literal in each clause
+    # to construct a new, preprocessed encodedCNF
+
+    enc_cnf = enc_cnf.copy()
+    cur_enc = 1
+    rev_encoding = {value: key for key, value in enc_cnf.encoding.items()}
+
+    new_encoding = {}
+    new_data = []
+    for clause in enc_cnf.data:
+        new_clause = []
+        for lit in clause:
+            if lit == 0:
+                new_clause.append(lit)
+                new_encoding[lit] = False
+                continue
+            prop = rev_encoding[abs(lit)]
+            negated = lit < 0
+            sign = (lit > 0) - (lit < 0)
+
+            prop = _pred_to_binrel(prop)
+
+            if not isinstance(prop, AppliedPredicate):
+                if prop not in new_encoding:
+                    new_encoding[prop] = cur_enc
+                    cur_enc += 1
+                lit = new_encoding[prop]
+                new_clause.append(sign*lit)
+                continue
+
+
+            if negated and prop.function == Q.eq:
+                negated = False
+                prop = Q.ne(*prop.arguments)
+
+            if prop.function == Q.ne:
+                arg1, arg2 = prop.arguments
+                if negated:
+                    new_prop = Q.eq(arg1, arg2)
+                    if new_prop not in new_encoding:
+                        new_encoding[new_prop] = cur_enc
+                        cur_enc += 1
+
+                    new_enc = new_encoding[new_prop]
+                    new_clause.append(new_enc)
+                    continue
+                else:
+                    new_props = (Q.gt(arg1, arg2), Q.lt(arg1, arg2))
+                    for new_prop in new_props:
+                        if new_prop not in new_encoding:
+                            new_encoding[new_prop] = cur_enc
+                            cur_enc += 1
+
+                        new_enc = new_encoding[new_prop]
+                        new_clause.append(new_enc)
+                    continue
+
+            if prop.function == Q.eq and negated:
+                assert False
+
+            if prop not in new_encoding:
+                new_encoding[prop] = cur_enc
+                cur_enc += 1
+            new_clause.append(new_encoding[prop]*sign)
+        new_data.append(new_clause)
+
+    assert len(new_encoding) >= cur_enc - 1
+
+    enc_cnf = EncodedCNF(new_data, new_encoding)
+    return enc_cnf
+
+
+def _pred_to_binrel(pred):
+    if not isinstance(pred, AppliedPredicate):
+        return pred
+
+    if pred.function in pred_to_pos_neg_zero:
+        f = pred_to_pos_neg_zero[pred.function]
+        if f is False:
+            return False
+        pred = f(pred.arguments[0])
+
+    if pred.function == Q.positive:
+        pred = Q.gt(pred.arguments[0], 0)
+    elif pred.function == Q.negative:
+        pred = Q.lt(pred.arguments[0], 0)
+    elif pred.function == Q.zero:
+        pred = Q.eq(pred.arguments[0], 0)
+    elif pred.function == Q.nonpositive:
+        pred = Q.le(pred.arguments[0], 0)
+    elif pred.function == Q.nonnegative:
+        pred = Q.ge(pred.arguments[0], 0)
+    elif pred.function == Q.nonzero:
+        pred = Q.ne(pred.arguments[0], 0)
+
+    return pred
+
+pred_to_pos_neg_zero = {
+    Q.extended_positive: Q.positive,
+    Q.extended_negative: Q.negative,
+    Q.extended_nonpositive: Q.nonpositive,
+    Q.extended_negative: Q.negative,
+    Q.extended_nonzero: Q.nonzero,
+    Q.negative_infinite: False,
+    Q.positive_infinite: False
+}
+
+def get_all_pred_and_expr_from_enc_cnf(enc_cnf):
+    all_exprs = set()
+    all_pred = set()
+    for pred in enc_cnf.encoding.keys():
+        if isinstance(pred, AppliedPredicate):
+            all_pred.add(pred)
+            all_exprs.update(pred.arguments)
+
+    return all_pred, all_exprs
+
+def extract_pred_from_old_assum(all_exprs):
+    """
+    Returns a list of relevant new assumption predicate
+    based on any old assumptions.
+
+    Raises an UnhandledInput exception if any of the assumptions are
+    unhandled.
+
+    Ignored predicate:
+    - commutative
+    - complex
+    - algebraic
+    - transcendental
+    - extended_real
+    - real
+    - all matrix predicate
+    - rational
+    - irrational
+
+    Example
+    =======
+    >>> from sympy.assumptions.lra_satask import extract_pred_from_old_assum
+    >>> from sympy import symbols
+    >>> x, y = symbols("x y", positive=True)
+    >>> extract_pred_from_old_assum([x, y, 2])
+    [Q.positive(x), Q.positive(y)]
+    """
+    ret = []
+    for expr in all_exprs:
+        if not hasattr(expr, "free_symbols"):
+            continue
+        if len(expr.free_symbols) == 0:
+            continue
+
+        if expr.is_real is not True:
+            raise UnhandledInput(f"LRASolver: {expr} must be real")
+        # test for I times imaginary variable; such expressions are considered real
+        if isinstance(expr, Mul) and any(arg.is_real is not True for arg in expr.args):
+            raise UnhandledInput(f"LRASolver: {expr} must be real")
+
+        if expr.is_integer == True and expr.is_zero != True:
+            raise UnhandledInput(f"LRASolver: {expr} is an integer")
+        if expr.is_integer == False:
+            raise UnhandledInput(f"LRASolver: {expr} can't be an integer")
+        if expr.is_rational == False:
+            raise UnhandledInput(f"LRASolver: {expr} is irational")
+
+        if expr.is_zero:
+            ret.append(Q.zero(expr))
+        elif expr.is_positive:
+            ret.append(Q.positive(expr))
+        elif expr.is_negative:
+            ret.append(Q.negative(expr))
+        elif expr.is_nonzero:
+            ret.append(Q.nonzero(expr))
+        elif expr.is_nonpositive:
+            ret.append(Q.nonpositive(expr))
+        elif expr.is_nonnegative:
+            ret.append(Q.nonnegative(expr))
+
+    return ret

lib/python3.12/site-packages/sympy/assumptions/refine.py

@@ -0,0 +1,405 @@
+from __future__ import annotations
+from typing import Callable
+
+from sympy.core import S, Add, Expr, Basic, Mul, Pow, Rational
+from sympy.core.logic import fuzzy_not
+from sympy.logic.boolalg import Boolean
+
+from sympy.assumptions import ask, Q  # type: ignore
+
+
+def refine(expr, assumptions=True):
+    """
+    Simplify an expression using assumptions.
+
+    Explanation
+    ===========
+
+    Unlike :func:`~.simplify()` which performs structural simplification
+    without any assumption, this function transforms the expression into
+    the form which is only valid under certain assumptions. Note that
+    ``simplify()`` is generally not done in refining process.
+
+    Refining boolean expression involves reducing it to ``S.true`` or
+    ``S.false``. Unlike :func:`~.ask()`, the expression will not be reduced
+    if the truth value cannot be determined.
+
+    Examples
+    ========
+
+    >>> from sympy import refine, sqrt, Q
+    >>> from sympy.abc import x
+    >>> refine(sqrt(x**2), Q.real(x))
+    Abs(x)
+    >>> refine(sqrt(x**2), Q.positive(x))
+    x
+
+    >>> refine(Q.real(x), Q.positive(x))
+    True
+    >>> refine(Q.positive(x), Q.real(x))
+    Q.positive(x)
+
+    See Also
+    ========
+
+    sympy.simplify.simplify.simplify : Structural simplification without assumptions.
+    sympy.assumptions.ask.ask : Query for boolean expressions using assumptions.
+    """
+    if not isinstance(expr, Basic):
+        return expr
+
+    if not expr.is_Atom:
+        args = [refine(arg, assumptions) for arg in expr.args]
+        # TODO: this will probably not work with Integral or Polynomial
+        expr = expr.func(*args)
+    if hasattr(expr, '_eval_refine'):
+        ref_expr = expr._eval_refine(assumptions)
+        if ref_expr is not None:
+            return ref_expr
+    name = expr.__class__.__name__
+    handler = handlers_dict.get(name, None)
+    if handler is None:
+        return expr
+    new_expr = handler(expr, assumptions)
+    if (new_expr is None) or (expr == new_expr):
+        return expr
+    if not isinstance(new_expr, Expr):
+        return new_expr
+    return refine(new_expr, assumptions)
+
+
+def refine_abs(expr, assumptions):
+    """
+    Handler for the absolute value.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, Abs
+    >>> from sympy.assumptions.refine import refine_abs
+    >>> from sympy.abc import x
+    >>> refine_abs(Abs(x), Q.real(x))
+    >>> refine_abs(Abs(x), Q.positive(x))
+    x
+    >>> refine_abs(Abs(x), Q.negative(x))
+    -x
+
+    """
+    from sympy.functions.elementary.complexes import Abs
+    arg = expr.args[0]
+    if ask(Q.real(arg), assumptions) and \
+            fuzzy_not(ask(Q.negative(arg), assumptions)):
+        # if it's nonnegative
+        return arg
+    if ask(Q.negative(arg), assumptions):
+        return -arg
+    # arg is Mul
+    if isinstance(arg, Mul):
+        r = [refine(abs(a), assumptions) for a in arg.args]
+        non_abs = []
+        in_abs = []
+        for i in r:
+            if isinstance(i, Abs):
+                in_abs.append(i.args[0])
+            else:
+                non_abs.append(i)
+        return Mul(*non_abs) * Abs(Mul(*in_abs))
+
+
+def refine_Pow(expr, assumptions):
+    """
+    Handler for instances of Pow.
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.refine import refine_Pow
+    >>> from sympy.abc import x,y,z
+    >>> refine_Pow((-1)**x, Q.real(x))
+    >>> refine_Pow((-1)**x, Q.even(x))
+    1
+    >>> refine_Pow((-1)**x, Q.odd(x))
+    -1
+
+    For powers of -1, even parts of the exponent can be simplified:
+
+    >>> refine_Pow((-1)**(x+y), Q.even(x))
+    (-1)**y
+    >>> refine_Pow((-1)**(x+y+z), Q.odd(x) & Q.odd(z))
+    (-1)**y
+    >>> refine_Pow((-1)**(x+y+2), Q.odd(x))
+    (-1)**(y + 1)
+    >>> refine_Pow((-1)**(x+3), True)
+    (-1)**(x + 1)
+
+    """
+    from sympy.functions.elementary.complexes import Abs
+    from sympy.functions import sign
+    if isinstance(expr.base, Abs):
+        if ask(Q.real(expr.base.args[0]), assumptions) and \
+                ask(Q.even(expr.exp), assumptions):
+            return expr.base.args[0] ** expr.exp
+    if ask(Q.real(expr.base), assumptions):
+        if expr.base.is_number:
+            if ask(Q.even(expr.exp), assumptions):
+                return abs(expr.base) ** expr.exp
+            if ask(Q.odd(expr.exp), assumptions):
+                return sign(expr.base) * abs(expr.base) ** expr.exp
+        if isinstance(expr.exp, Rational):
+            if isinstance(expr.base, Pow):
+                return abs(expr.base.base) ** (expr.base.exp * expr.exp)
+
+        if expr.base is S.NegativeOne:
+            if expr.exp.is_Add:
+
+                old = expr
+
+                # For powers of (-1) we can remove
+                #  - even terms
+                #  - pairs of odd terms
+                #  - a single odd term + 1
+                #  - A numerical constant N can be replaced with mod(N,2)
+
+                coeff, terms = expr.exp.as_coeff_add()
+                terms = set(terms)
+                even_terms = set()
+                odd_terms = set()
+                initial_number_of_terms = len(terms)
+
+                for t in terms:
+                    if ask(Q.even(t), assumptions):
+                        even_terms.add(t)
+                    elif ask(Q.odd(t), assumptions):
+                        odd_terms.add(t)
+
+                terms -= even_terms
+                if len(odd_terms) % 2:
+                    terms -= odd_terms
+                    new_coeff = (coeff + S.One) % 2
+                else:
+                    terms -= odd_terms
+                    new_coeff = coeff % 2
+
+                if new_coeff != coeff or len(terms) < initial_number_of_terms:
+                    terms.add(new_coeff)
+                    expr = expr.base**(Add(*terms))
+
+                # Handle (-1)**((-1)**n/2 + m/2)
+                e2 = 2*expr.exp
+                if ask(Q.even(e2), assumptions):
+                    if e2.could_extract_minus_sign():
+                        e2 *= expr.base
+                if e2.is_Add:
+                    i, p = e2.as_two_terms()
+                    if p.is_Pow and p.base is S.NegativeOne:
+                        if ask(Q.integer(p.exp), assumptions):
+                            i = (i + 1)/2
+                            if ask(Q.even(i), assumptions):
+                                return expr.base**p.exp
+                            elif ask(Q.odd(i), assumptions):
+                                return expr.base**(p.exp + 1)
+                            else:
+                                return expr.base**(p.exp + i)
+
+                if old != expr:
+                    return expr
+
+
+def refine_atan2(expr, assumptions):
+    """
+    Handler for the atan2 function.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, atan2
+    >>> from sympy.assumptions.refine import refine_atan2
+    >>> from sympy.abc import x, y
+    >>> refine_atan2(atan2(y,x), Q.real(y) & Q.positive(x))
+    atan(y/x)
+    >>> refine_atan2(atan2(y,x), Q.negative(y) & Q.negative(x))
+    atan(y/x) - pi
+    >>> refine_atan2(atan2(y,x), Q.positive(y) & Q.negative(x))
+    atan(y/x) + pi
+    >>> refine_atan2(atan2(y,x), Q.zero(y) & Q.negative(x))
+    pi
+    >>> refine_atan2(atan2(y,x), Q.positive(y) & Q.zero(x))
+    pi/2
+    >>> refine_atan2(atan2(y,x), Q.negative(y) & Q.zero(x))
+    -pi/2
+    >>> refine_atan2(atan2(y,x), Q.zero(y) & Q.zero(x))
+    nan
+    """
+    from sympy.functions.elementary.trigonometric import atan
+    y, x = expr.args
+    if ask(Q.real(y) & Q.positive(x), assumptions):
+        return atan(y / x)
+    elif ask(Q.negative(y) & Q.negative(x), assumptions):
+        return atan(y / x) - S.Pi
+    elif ask(Q.positive(y) & Q.negative(x), assumptions):
+        return atan(y / x) + S.Pi
+    elif ask(Q.zero(y) & Q.negative(x), assumptions):
+        return S.Pi
+    elif ask(Q.positive(y) & Q.zero(x), assumptions):
+        return S.Pi/2
+    elif ask(Q.negative(y) & Q.zero(x), assumptions):
+        return -S.Pi/2
+    elif ask(Q.zero(y) & Q.zero(x), assumptions):
+        return S.NaN
+    else:
+        return expr
+
+
+def refine_re(expr, assumptions):
+    """
+    Handler for real part.
+
+    Examples
+    ========
+
+    >>> from sympy.assumptions.refine import refine_re
+    >>> from sympy import Q, re
+    >>> from sympy.abc import x
+    >>> refine_re(re(x), Q.real(x))
+    x
+    >>> refine_re(re(x), Q.imaginary(x))
+    0
+    """
+    arg = expr.args[0]
+    if ask(Q.real(arg), assumptions):
+        return arg
+    if ask(Q.imaginary(arg), assumptions):
+        return S.Zero
+    return _refine_reim(expr, assumptions)
+
+
+def refine_im(expr, assumptions):
+    """
+    Handler for imaginary part.
+
+    Explanation
+    ===========
+
+    >>> from sympy.assumptions.refine import refine_im
+    >>> from sympy import Q, im
+    >>> from sympy.abc import x
+    >>> refine_im(im(x), Q.real(x))
+    0
+    >>> refine_im(im(x), Q.imaginary(x))
+    -I*x
+    """
+    arg = expr.args[0]
+    if ask(Q.real(arg), assumptions):
+        return S.Zero
+    if ask(Q.imaginary(arg), assumptions):
+        return - S.ImaginaryUnit * arg
+    return _refine_reim(expr, assumptions)
+
+def refine_arg(expr, assumptions):
+    """
+    Handler for complex argument
+
+    Explanation
+    ===========
+
+    >>> from sympy.assumptions.refine import refine_arg
+    >>> from sympy import Q, arg
+    >>> from sympy.abc import x
+    >>> refine_arg(arg(x), Q.positive(x))
+    0
+    >>> refine_arg(arg(x), Q.negative(x))
+    pi
+    """
+    rg = expr.args[0]
+    if ask(Q.positive(rg), assumptions):
+        return S.Zero
+    if ask(Q.negative(rg), assumptions):
+        return S.Pi
+    return None
+
+
+def _refine_reim(expr, assumptions):
+    # Helper function for refine_re & refine_im
+    expanded = expr.expand(complex = True)
+    if expanded != expr:
+        refined = refine(expanded, assumptions)
+        if refined != expanded:
+            return refined
+    # Best to leave the expression as is
+    return None
+
+
+def refine_sign(expr, assumptions):
+    """
+    Handler for sign.
+
+    Examples
+    ========
+
+    >>> from sympy.assumptions.refine import refine_sign
+    >>> from sympy import Symbol, Q, sign, im
+    >>> x = Symbol('x', real = True)
+    >>> expr = sign(x)
+    >>> refine_sign(expr, Q.positive(x) & Q.nonzero(x))
+    1
+    >>> refine_sign(expr, Q.negative(x) & Q.nonzero(x))
+    -1
+    >>> refine_sign(expr, Q.zero(x))
+    0
+    >>> y = Symbol('y', imaginary = True)
+    >>> expr = sign(y)
+    >>> refine_sign(expr, Q.positive(im(y)))
+    I
+    >>> refine_sign(expr, Q.negative(im(y)))
+    -I
+    """
+    arg = expr.args[0]
+    if ask(Q.zero(arg), assumptions):
+        return S.Zero
+    if ask(Q.real(arg)):
+        if ask(Q.positive(arg), assumptions):
+            return S.One
+        if ask(Q.negative(arg), assumptions):
+            return S.NegativeOne
+    if ask(Q.imaginary(arg)):
+        arg_re, arg_im = arg.as_real_imag()
+        if ask(Q.positive(arg_im), assumptions):
+            return S.ImaginaryUnit
+        if ask(Q.negative(arg_im), assumptions):
+            return -S.ImaginaryUnit
+    return expr
+
+
+def refine_matrixelement(expr, assumptions):
+    """
+    Handler for symmetric part.
+
+    Examples
+    ========
+
+    >>> from sympy.assumptions.refine import refine_matrixelement
+    >>> from sympy import MatrixSymbol, Q
+    >>> X = MatrixSymbol('X', 3, 3)
+    >>> refine_matrixelement(X[0, 1], Q.symmetric(X))
+    X[0, 1]
+    >>> refine_matrixelement(X[1, 0], Q.symmetric(X))
+    X[0, 1]
+    """
+    from sympy.matrices.expressions.matexpr import MatrixElement
+    matrix, i, j = expr.args
+    if ask(Q.symmetric(matrix), assumptions):
+        if (i - j).could_extract_minus_sign():
+            return expr
+        return MatrixElement(matrix, j, i)
+
+handlers_dict: dict[str, Callable[[Expr, Boolean], Expr]] = {
+    'Abs': refine_abs,
+    'Pow': refine_Pow,
+    'atan2': refine_atan2,
+    're': refine_re,
+    'im': refine_im,
+    'arg': refine_arg,
+    'sign': refine_sign,
+    'MatrixElement': refine_matrixelement
+}

lib/python3.12/site-packages/sympy/assumptions/satask.py

@@ -0,0 +1,369 @@
+"""
+Module to evaluate the proposition with assumptions using SAT algorithm.
+"""
+
+from sympy.core.singleton import S
+from sympy.core.symbol import Symbol
+from sympy.core.kind import NumberKind, UndefinedKind
+from sympy.assumptions.ask_generated import get_all_known_matrix_facts, get_all_known_number_facts
+from sympy.assumptions.assume import global_assumptions, AppliedPredicate
+from sympy.assumptions.sathandlers import class_fact_registry
+from sympy.core import oo
+from sympy.logic.inference import satisfiable
+from sympy.assumptions.cnf import CNF, EncodedCNF
+from sympy.matrices.kind import MatrixKind
+
+
+def satask(proposition, assumptions=True, context=global_assumptions,
+        use_known_facts=True, iterations=oo):
+    """
+    Function to evaluate the proposition with assumptions using SAT algorithm.
+
+    This function extracts every fact relevant to the expressions composing
+    proposition and assumptions. For example, if a predicate containing
+    ``Abs(x)`` is proposed, then ``Q.zero(Abs(x)) | Q.positive(Abs(x))``
+    will be found and passed to SAT solver because ``Q.nonnegative`` is
+    registered as a fact for ``Abs``.
+
+    Proposition is evaluated to ``True`` or ``False`` if the truth value can be
+    determined. If not, ``None`` is returned.
+
+    Parameters
+    ==========
+
+    proposition : Any boolean expression.
+        Proposition which will be evaluated to boolean value.
+
+    assumptions : Any boolean expression, optional.
+        Local assumptions to evaluate the *proposition*.
+
+    context : AssumptionsContext, optional.
+        Default assumptions to evaluate the *proposition*. By default,
+        this is ``sympy.assumptions.global_assumptions`` variable.
+
+    use_known_facts : bool, optional.
+        If ``True``, facts from ``sympy.assumptions.ask_generated``
+        module are passed to SAT solver as well.
+
+    iterations : int, optional.
+        Number of times that relevant facts are recursively extracted.
+        Default is infinite times until no new fact is found.
+
+    Returns
+    =======
+
+    ``True``, ``False``, or ``None``
+
+    Examples
+    ========
+
+    >>> from sympy import Abs, Q
+    >>> from sympy.assumptions.satask import satask
+    >>> from sympy.abc import x
+    >>> satask(Q.zero(Abs(x)), Q.zero(x))
+    True
+
+    """
+    props = CNF.from_prop(proposition)
+    _props = CNF.from_prop(~proposition)
+
+    assumptions = CNF.from_prop(assumptions)
+
+    context_cnf = CNF()
+    if context:
+        context_cnf = context_cnf.extend(context)
+
+    sat = get_all_relevant_facts(props, assumptions, context_cnf,
+        use_known_facts=use_known_facts, iterations=iterations)
+    sat.add_from_cnf(assumptions)
+    if context:
+        sat.add_from_cnf(context_cnf)
+
+    return check_satisfiability(props, _props, sat)
+
+
+def check_satisfiability(prop, _prop, factbase):
+    sat_true = factbase.copy()
+    sat_false = factbase.copy()
+    sat_true.add_from_cnf(prop)
+    sat_false.add_from_cnf(_prop)
+    can_be_true = satisfiable(sat_true)
+    can_be_false = satisfiable(sat_false)
+
+    if can_be_true and can_be_false:
+        return None
+
+    if can_be_true and not can_be_false:
+        return True
+
+    if not can_be_true and can_be_false:
+        return False
+
+    if not can_be_true and not can_be_false:
+        # TODO: Run additional checks to see which combination of the
+        # assumptions, global_assumptions, and relevant_facts are
+        # inconsistent.
+        raise ValueError("Inconsistent assumptions")
+
+
+def extract_predargs(proposition, assumptions=None, context=None):
+    """
+    Extract every expression in the argument of predicates from *proposition*,
+    *assumptions* and *context*.
+
+    Parameters
+    ==========
+
+    proposition : sympy.assumptions.cnf.CNF
+
+    assumptions : sympy.assumptions.cnf.CNF, optional.
+
+    context : sympy.assumptions.cnf.CNF, optional.
+        CNF generated from assumptions context.
+
+    Examples
+    ========
+
+    >>> from sympy import Q, Abs
+    >>> from sympy.assumptions.cnf import CNF
+    >>> from sympy.assumptions.satask import extract_predargs
+    >>> from sympy.abc import x, y
+    >>> props = CNF.from_prop(Q.zero(Abs(x*y)))
+    >>> assump = CNF.from_prop(Q.zero(x) & Q.zero(y))
+    >>> extract_predargs(props, assump)
+    {x, y, Abs(x*y)}
+
+    """
+    req_keys = find_symbols(proposition)
+    keys = proposition.all_predicates()
+    # XXX: We need this since True/False are not Basic
+    lkeys = set()
+    if assumptions:
+        lkeys |= assumptions.all_predicates()
+    if context:
+        lkeys |= context.all_predicates()
+
+    lkeys = lkeys - {S.true, S.false}
+    tmp_keys = None
+    while tmp_keys != set():
+        tmp = set()
+        for l in lkeys:
+            syms = find_symbols(l)
+            if (syms & req_keys) != set():
+                tmp |= syms
+        tmp_keys = tmp - req_keys
+        req_keys |= tmp_keys
+    keys |= {l for l in lkeys if find_symbols(l) & req_keys != set()}
+
+    exprs = set()
+    for key in keys:
+        if isinstance(key, AppliedPredicate):
+            exprs |= set(key.arguments)
+        else:
+            exprs.add(key)
+    return exprs
+
+def find_symbols(pred):
+    """
+    Find every :obj:`~.Symbol` in *pred*.
+
+    Parameters
+    ==========
+
+    pred : sympy.assumptions.cnf.CNF, or any Expr.
+
+    """
+    if isinstance(pred, CNF):
+        symbols = set()
+        for a in pred.all_predicates():
+            symbols |= find_symbols(a)
+        return symbols
+    return pred.atoms(Symbol)
+
+
+def get_relevant_clsfacts(exprs, relevant_facts=None):
+    """
+    Extract relevant facts from the items in *exprs*. Facts are defined in
+    ``assumptions.sathandlers`` module.
+
+    This function is recursively called by ``get_all_relevant_facts()``.
+
+    Parameters
+    ==========
+
+    exprs : set
+        Expressions whose relevant facts are searched.
+
+    relevant_facts : sympy.assumptions.cnf.CNF, optional.
+        Pre-discovered relevant facts.
+
+    Returns
+    =======
+
+    exprs : set
+        Candidates for next relevant fact searching.
+
+    relevant_facts : sympy.assumptions.cnf.CNF
+        Updated relevant facts.
+
+    Examples
+    ========
+
+    Here, we will see how facts relevant to ``Abs(x*y)`` are recursively
+    extracted. On the first run, set containing the expression is passed
+    without pre-discovered relevant facts. The result is a set containing
+    candidates for next run, and ``CNF()`` instance containing facts
+    which are relevant to ``Abs`` and its argument.
+
+    >>> from sympy import Abs
+    >>> from sympy.assumptions.satask import get_relevant_clsfacts
+    >>> from sympy.abc import x, y
+    >>> exprs = {Abs(x*y)}
+    >>> exprs, facts = get_relevant_clsfacts(exprs)
+    >>> exprs
+    {x*y}
+    >>> facts.clauses #doctest: +SKIP
+    {frozenset({Literal(Q.odd(Abs(x*y)), False), Literal(Q.odd(x*y), True)}),
+    frozenset({Literal(Q.zero(Abs(x*y)), False), Literal(Q.zero(x*y), True)}),
+    frozenset({Literal(Q.even(Abs(x*y)), False), Literal(Q.even(x*y), True)}),
+    frozenset({Literal(Q.zero(Abs(x*y)), True), Literal(Q.zero(x*y), False)}),
+    frozenset({Literal(Q.even(Abs(x*y)), False),
+                Literal(Q.odd(Abs(x*y)), False),
+                Literal(Q.odd(x*y), True)}),
+    frozenset({Literal(Q.even(Abs(x*y)), False),
+                Literal(Q.even(x*y), True),
+                Literal(Q.odd(Abs(x*y)), False)}),
+    frozenset({Literal(Q.positive(Abs(x*y)), False),
+                Literal(Q.zero(Abs(x*y)), False)})}
+
+    We pass the first run's results to the second run, and get the expressions
+    for next run and updated facts.
+
+    >>> exprs, facts = get_relevant_clsfacts(exprs, relevant_facts=facts)
+    >>> exprs
+    {x, y}
+
+    On final run, no more candidate is returned thus we know that all
+    relevant facts are successfully retrieved.
+
+    >>> exprs, facts = get_relevant_clsfacts(exprs, relevant_facts=facts)
+    >>> exprs
+    set()
+
+    """
+    if not relevant_facts:
+        relevant_facts = CNF()
+
+    newexprs = set()
+    for expr in exprs:
+        for fact in class_fact_registry(expr):
+            newfact = CNF.to_CNF(fact)
+            relevant_facts = relevant_facts._and(newfact)
+            for key in newfact.all_predicates():
+                if isinstance(key, AppliedPredicate):
+                    newexprs |= set(key.arguments)
+
+    return newexprs - exprs, relevant_facts
+
+
+def get_all_relevant_facts(proposition, assumptions, context,
+        use_known_facts=True, iterations=oo):
+    """
+    Extract all relevant facts from *proposition* and *assumptions*.
+
+    This function extracts the facts by recursively calling
+    ``get_relevant_clsfacts()``. Extracted facts are converted to
+    ``EncodedCNF`` and returned.
+
+    Parameters
+    ==========
+
+    proposition : sympy.assumptions.cnf.CNF
+        CNF generated from proposition expression.
+
+    assumptions : sympy.assumptions.cnf.CNF
+        CNF generated from assumption expression.
+
+    context : sympy.assumptions.cnf.CNF
+        CNF generated from assumptions context.
+
+    use_known_facts : bool, optional.
+        If ``True``, facts from ``sympy.assumptions.ask_generated``
+        module are encoded as well.
+
+    iterations : int, optional.
+        Number of times that relevant facts are recursively extracted.
+        Default is infinite times until no new fact is found.
+
+    Returns
+    =======
+
+    sympy.assumptions.cnf.EncodedCNF
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.cnf import CNF
+    >>> from sympy.assumptions.satask import get_all_relevant_facts
+    >>> from sympy.abc import x, y
+    >>> props = CNF.from_prop(Q.nonzero(x*y))
+    >>> assump = CNF.from_prop(Q.nonzero(x))
+    >>> context = CNF.from_prop(Q.nonzero(y))
+    >>> get_all_relevant_facts(props, assump, context) #doctest: +SKIP
+    <sympy.assumptions.cnf.EncodedCNF at 0x7f09faa6ccd0>
+
+    """
+    # The relevant facts might introduce new keys, e.g., Q.zero(x*y) will
+    # introduce the keys Q.zero(x) and Q.zero(y), so we need to run it until
+    # we stop getting new things. Hopefully this strategy won't lead to an
+    # infinite loop in the future.
+    i = 0
+    relevant_facts = CNF()
+    all_exprs = set()
+    while True:
+        if i == 0:
+            exprs = extract_predargs(proposition, assumptions, context)
+        all_exprs |= exprs
+        exprs, relevant_facts = get_relevant_clsfacts(exprs, relevant_facts)
+        i += 1
+        if i >= iterations:
+            break
+        if not exprs:
+            break
+
+    if use_known_facts:
+        known_facts_CNF = CNF()
+
+        if any(expr.kind == MatrixKind(NumberKind) for expr in all_exprs):
+            known_facts_CNF.add_clauses(get_all_known_matrix_facts())
+        # check for undefinedKind since kind system isn't fully implemented
+        if any(((expr.kind == NumberKind) or (expr.kind == UndefinedKind)) for expr in all_exprs):
+            known_facts_CNF.add_clauses(get_all_known_number_facts())
+
+        kf_encoded = EncodedCNF()
+        kf_encoded.from_cnf(known_facts_CNF)
+
+        def translate_literal(lit, delta):
+            if lit > 0:
+                return lit + delta
+            else:
+                return lit - delta
+
+        def translate_data(data, delta):
+            return [{translate_literal(i, delta) for i in clause} for clause in data]
+        data = []
+        symbols = []
+        n_lit = len(kf_encoded.symbols)
+        for i, expr in enumerate(all_exprs):
+            symbols += [pred(expr) for pred in kf_encoded.symbols]
+            data += translate_data(kf_encoded.data, i * n_lit)
+
+        encoding = dict(list(zip(symbols, range(1, len(symbols)+1))))
+        ctx = EncodedCNF(data, encoding)
+    else:
+        ctx = EncodedCNF()
+
+    ctx.add_from_cnf(relevant_facts)
+
+    return ctx

lib/python3.12/site-packages/sympy/assumptions/sathandlers.py

@@ -0,0 +1,322 @@
+from collections import defaultdict
+
+from sympy.assumptions.ask import Q
+from sympy.core import (Add, Mul, Pow, Number, NumberSymbol, Symbol)
+from sympy.core.numbers import ImaginaryUnit
+from sympy.functions.elementary.complexes import Abs
+from sympy.logic.boolalg import (Equivalent, And, Or, Implies)
+from sympy.matrices.expressions import MatMul
+
+# APIs here may be subject to change
+
+
+### Helper functions ###
+
+def allargs(symbol, fact, expr):
+    """
+    Apply all arguments of the expression to the fact structure.
+
+    Parameters
+    ==========
+
+    symbol : Symbol
+        A placeholder symbol.
+
+    fact : Boolean
+        Resulting ``Boolean`` expression.
+
+    expr : Expr
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.sathandlers import allargs
+    >>> from sympy.abc import x, y
+    >>> allargs(x, Q.negative(x) | Q.positive(x), x*y)
+    (Q.negative(x) | Q.positive(x)) & (Q.negative(y) | Q.positive(y))
+
+    """
+    return And(*[fact.subs(symbol, arg) for arg in expr.args])
+
+
+def anyarg(symbol, fact, expr):
+    """
+    Apply any argument of the expression to the fact structure.
+
+    Parameters
+    ==========
+
+    symbol : Symbol
+        A placeholder symbol.
+
+    fact : Boolean
+        Resulting ``Boolean`` expression.
+
+    expr : Expr
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.sathandlers import anyarg
+    >>> from sympy.abc import x, y
+    >>> anyarg(x, Q.negative(x) & Q.positive(x), x*y)
+    (Q.negative(x) & Q.positive(x)) | (Q.negative(y) & Q.positive(y))
+
+    """
+    return Or(*[fact.subs(symbol, arg) for arg in expr.args])
+
+
+def exactlyonearg(symbol, fact, expr):
+    """
+    Apply exactly one argument of the expression to the fact structure.
+
+    Parameters
+    ==========
+
+    symbol : Symbol
+        A placeholder symbol.
+
+    fact : Boolean
+        Resulting ``Boolean`` expression.
+
+    expr : Expr
+
+    Examples
+    ========
+
+    >>> from sympy import Q
+    >>> from sympy.assumptions.sathandlers import exactlyonearg
+    >>> from sympy.abc import x, y
+    >>> exactlyonearg(x, Q.positive(x), x*y)
+    (Q.positive(x) & ~Q.positive(y)) | (Q.positive(y) & ~Q.positive(x))
+
+    """
+    pred_args = [fact.subs(symbol, arg) for arg in expr.args]
+    res = Or(*[And(pred_args[i], *[~lit for lit in pred_args[:i] +
+        pred_args[i+1:]]) for i in range(len(pred_args))])
+    return res
+
+
+### Fact registry ###
+
+class ClassFactRegistry:
+    """
+    Register handlers against classes.
+
+    Explanation
+    ===========
+
+    ``register`` method registers the handler function for a class. Here,
+    handler function should return a single fact. ``multiregister`` method
+    registers the handler function for multiple classes. Here, handler function
+    should return a container of multiple facts.
+
+    ``registry(expr)`` returns a set of facts for *expr*.
+
+    Examples
+    ========
+
+    Here, we register the facts for ``Abs``.
+
+    >>> from sympy import Abs, Equivalent, Q
+    >>> from sympy.assumptions.sathandlers import ClassFactRegistry
+    >>> reg = ClassFactRegistry()
+    >>> @reg.register(Abs)
+    ... def f1(expr):
+    ...     return Q.nonnegative(expr)
+    >>> @reg.register(Abs)
+    ... def f2(expr):
+    ...     arg = expr.args[0]
+    ...     return Equivalent(~Q.zero(arg), ~Q.zero(expr))
+
+    Calling the registry with expression returns the defined facts for the
+    expression.
+
+    >>> from sympy.abc import x
+    >>> reg(Abs(x))
+    {Q.nonnegative(Abs(x)), Equivalent(~Q.zero(x), ~Q.zero(Abs(x)))}
+
+    Multiple facts can be registered at once by ``multiregister`` method.
+
+    >>> reg2 = ClassFactRegistry()
+    >>> @reg2.multiregister(Abs)
+    ... def _(expr):
+    ...     arg = expr.args[0]
+    ...     return [Q.even(arg) >> Q.even(expr), Q.odd(arg) >> Q.odd(expr)]
+    >>> reg2(Abs(x))
+    {Implies(Q.even(x), Q.even(Abs(x))), Implies(Q.odd(x), Q.odd(Abs(x)))}
+
+    """
+    def __init__(self):
+        self.singlefacts = defaultdict(frozenset)
+        self.multifacts = defaultdict(frozenset)
+
+    def register(self, cls):
+        def _(func):
+            self.singlefacts[cls] |= {func}
+            return func
+        return _
+
+    def multiregister(self, *classes):
+        def _(func):
+            for cls in classes:
+                self.multifacts[cls] |= {func}
+            return func
+        return _
+
+    def __getitem__(self, key):
+        ret1 = self.singlefacts[key]
+        for k in self.singlefacts:
+            if issubclass(key, k):
+                ret1 |= self.singlefacts[k]
+
+        ret2 = self.multifacts[key]
+        for k in self.multifacts:
+            if issubclass(key, k):
+                ret2 |= self.multifacts[k]
+
+        return ret1, ret2
+
+    def __call__(self, expr):
+        ret = set()
+
+        handlers1, handlers2 = self[type(expr)]
+
+        ret.update(h(expr) for h in handlers1)
+        for h in handlers2:
+            ret.update(h(expr))
+        return ret
+
+class_fact_registry = ClassFactRegistry()
+
+
+
+### Class fact registration ###
+
+x = Symbol('x')
+
+## Abs ##
+
+@class_fact_registry.multiregister(Abs)
+def _(expr):
+    arg = expr.args[0]
+    return [Q.nonnegative(expr),
+            Equivalent(~Q.zero(arg), ~Q.zero(expr)),
+            Q.even(arg) >> Q.even(expr),
+            Q.odd(arg) >> Q.odd(expr),
+            Q.integer(arg) >> Q.integer(expr),
+            ]
+
+
+### Add ##
+
+@class_fact_registry.multiregister(Add)
+def _(expr):
+    return [allargs(x, Q.positive(x), expr) >> Q.positive(expr),
+            allargs(x, Q.negative(x), expr) >> Q.negative(expr),
+            allargs(x, Q.real(x), expr) >> Q.real(expr),
+            allargs(x, Q.rational(x), expr) >> Q.rational(expr),
+            allargs(x, Q.integer(x), expr) >> Q.integer(expr),
+            exactlyonearg(x, ~Q.integer(x), expr) >> ~Q.integer(expr),
+            ]
+
+@class_fact_registry.register(Add)
+def _(expr):
+    allargs_real = allargs(x, Q.real(x), expr)
+    onearg_irrational = exactlyonearg(x, Q.irrational(x), expr)
+    return Implies(allargs_real, Implies(onearg_irrational, Q.irrational(expr)))
+
+
+### Mul ###
+
+@class_fact_registry.multiregister(Mul)
+def _(expr):
+    return [Equivalent(Q.zero(expr), anyarg(x, Q.zero(x), expr)),
+            allargs(x, Q.positive(x), expr) >> Q.positive(expr),
+            allargs(x, Q.real(x), expr) >> Q.real(expr),
+            allargs(x, Q.rational(x), expr) >> Q.rational(expr),
+            allargs(x, Q.integer(x), expr) >> Q.integer(expr),
+            exactlyonearg(x, ~Q.rational(x), expr) >> ~Q.integer(expr),
+            allargs(x, Q.commutative(x), expr) >> Q.commutative(expr),
+            ]
+
+@class_fact_registry.register(Mul)
+def _(expr):
+    # Implicitly assumes Mul has more than one arg
+    # Would be allargs(x, Q.prime(x) | Q.composite(x)) except 1 is composite
+    # More advanced prime assumptions will require inequalities, as 1 provides
+    # a corner case.
+    allargs_prime = allargs(x, Q.prime(x), expr)
+    return Implies(allargs_prime, ~Q.prime(expr))
+
+@class_fact_registry.register(Mul)
+def _(expr):
+    # General Case: Odd number of imaginary args implies mul is imaginary(To be implemented)
+    allargs_imag_or_real = allargs(x, Q.imaginary(x) | Q.real(x), expr)
+    onearg_imaginary = exactlyonearg(x, Q.imaginary(x), expr)
+    return Implies(allargs_imag_or_real, Implies(onearg_imaginary, Q.imaginary(expr)))
+
+@class_fact_registry.register(Mul)
+def _(expr):
+    allargs_real = allargs(x, Q.real(x), expr)
+    onearg_irrational = exactlyonearg(x, Q.irrational(x), expr)
+    return Implies(allargs_real, Implies(onearg_irrational, Q.irrational(expr)))
+
+@class_fact_registry.register(Mul)
+def _(expr):
+    # Including the integer qualification means we don't need to add any facts
+    # for odd, since the assumptions already know that every integer is
+    # exactly one of even or odd.
+    allargs_integer = allargs(x, Q.integer(x), expr)
+    anyarg_even = anyarg(x, Q.even(x), expr)
+    return Implies(allargs_integer, Equivalent(anyarg_even, Q.even(expr)))
+
+
+### MatMul ###
+
+@class_fact_registry.register(MatMul)
+def _(expr):
+    allargs_square = allargs(x, Q.square(x), expr)
+    allargs_invertible = allargs(x, Q.invertible(x), expr)
+    return Implies(allargs_square, Equivalent(Q.invertible(expr), allargs_invertible))
+
+
+### Pow ###
+
+@class_fact_registry.multiregister(Pow)
+def _(expr):
+    base, exp = expr.base, expr.exp
+    return [
+        (Q.real(base) & Q.even(exp) & Q.nonnegative(exp)) >> Q.nonnegative(expr),
+        (Q.nonnegative(base) & Q.odd(exp) & Q.nonnegative(exp)) >> Q.nonnegative(expr),
+        (Q.nonpositive(base) & Q.odd(exp) & Q.nonnegative(exp)) >> Q.nonpositive(expr),
+        Equivalent(Q.zero(expr), Q.zero(base) & Q.positive(exp))
+    ]
+
+
+### Numbers ###
+
+_old_assump_getters = {
+    Q.positive: lambda o: o.is_positive,
+    Q.zero: lambda o: o.is_zero,
+    Q.negative: lambda o: o.is_negative,
+    Q.rational: lambda o: o.is_rational,
+    Q.irrational: lambda o: o.is_irrational,
+    Q.even: lambda o: o.is_even,
+    Q.odd: lambda o: o.is_odd,
+    Q.imaginary: lambda o: o.is_imaginary,
+    Q.prime: lambda o: o.is_prime,
+    Q.composite: lambda o: o.is_composite,
+}
+
+@class_fact_registry.multiregister(Number, NumberSymbol, ImaginaryUnit)
+def _(expr):
+    ret = []
+    for p, getter in _old_assump_getters.items():
+        pred = p(expr)
+        prop = getter(expr)
+        if prop is not None:
+            ret.append(Equivalent(pred, prop))
+    return ret

lib/python3.12/site-packages/sympy/assumptions/tests/test_assumptions_2.py

@@ -0,0 +1,35 @@
+"""
+rename this to test_assumptions.py when the old assumptions system is deleted
+"""
+from sympy.abc import x, y
+from sympy.assumptions.assume import global_assumptions
+from sympy.assumptions.ask import Q
+from sympy.printing import pretty
+
+
+def test_equal():
+    """Test for equality"""
+    assert Q.positive(x) == Q.positive(x)
+    assert Q.positive(x) != ~Q.positive(x)
+    assert ~Q.positive(x) == ~Q.positive(x)
+
+
+def test_pretty():
+    assert pretty(Q.positive(x)) == "Q.positive(x)"
+    assert pretty(
+        {Q.positive, Q.integer}) == "{Q.integer, Q.positive}"
+
+
+def test_global():
+    """Test for global assumptions"""
+    global_assumptions.add(x > 0)
+    assert (x > 0) in global_assumptions
+    global_assumptions.remove(x > 0)
+    assert not (x > 0) in global_assumptions
+    # same with multiple of assumptions
+    global_assumptions.add(x > 0, y > 0)
+    assert (x > 0) in global_assumptions
+    assert (y > 0) in global_assumptions
+    global_assumptions.clear()
+    assert not (x > 0) in global_assumptions
+    assert not (y > 0) in global_assumptions

lib/python3.12/site-packages/sympy/assumptions/tests/test_context.py

@@ -0,0 +1,39 @@
+from sympy.assumptions import ask, Q
+from sympy.assumptions.assume import assuming, global_assumptions
+from sympy.abc import x, y
+
+def test_assuming():
+    with assuming(Q.integer(x)):
+        assert ask(Q.integer(x))
+    assert not ask(Q.integer(x))
+
+def test_assuming_nested():
+    assert not ask(Q.integer(x))
+    assert not ask(Q.integer(y))
+    with assuming(Q.integer(x)):
+        assert ask(Q.integer(x))
+        assert not ask(Q.integer(y))
+        with assuming(Q.integer(y)):
+            assert ask(Q.integer(x))
+            assert ask(Q.integer(y))
+        assert ask(Q.integer(x))
+        assert not ask(Q.integer(y))
+    assert not ask(Q.integer(x))
+    assert not ask(Q.integer(y))
+
+def test_finally():
+    try:
+        with assuming(Q.integer(x)):
+            1/0
+    except ZeroDivisionError:
+        pass
+    assert not ask(Q.integer(x))
+
+def test_remove_safe():
+    global_assumptions.add(Q.integer(x))
+    with assuming():
+        assert ask(Q.integer(x))
+        global_assumptions.remove(Q.integer(x))
+        assert not ask(Q.integer(x))
+    assert ask(Q.integer(x))
+    global_assumptions.clear() # for the benefit of other tests

lib/python3.12/site-packages/sympy/assumptions/tests/test_matrices.py

@@ -0,0 +1,283 @@
+from sympy.assumptions.ask import (Q, ask)
+from sympy.core.symbol import Symbol
+from sympy.matrices.expressions.diagonal import (DiagMatrix, DiagonalMatrix)
+from sympy.matrices.dense import Matrix
+from sympy.matrices.expressions import (MatrixSymbol, Identity, ZeroMatrix,
+        OneMatrix, Trace, MatrixSlice, Determinant, BlockMatrix, BlockDiagMatrix)
+from sympy.matrices.expressions.factorizations import LofLU
+from sympy.testing.pytest import XFAIL
+
+X = MatrixSymbol('X', 2, 2)
+Y = MatrixSymbol('Y', 2, 3)
+Z = MatrixSymbol('Z', 2, 2)
+A1x1 = MatrixSymbol('A1x1', 1, 1)
+B1x1 = MatrixSymbol('B1x1', 1, 1)
+C0x0 = MatrixSymbol('C0x0', 0, 0)
+V1 = MatrixSymbol('V1', 2, 1)
+V2 = MatrixSymbol('V2', 2, 1)
+
+def test_square():
+    assert ask(Q.square(X))
+    assert not ask(Q.square(Y))
+    assert ask(Q.square(Y*Y.T))
+
+def test_invertible():
+    assert ask(Q.invertible(X), Q.invertible(X))
+    assert ask(Q.invertible(Y)) is False
+    assert ask(Q.invertible(X*Y), Q.invertible(X)) is False
+    assert ask(Q.invertible(X*Z), Q.invertible(X)) is None
+    assert ask(Q.invertible(X*Z), Q.invertible(X) & Q.invertible(Z)) is True
+    assert ask(Q.invertible(X.T)) is None
+    assert ask(Q.invertible(X.T), Q.invertible(X)) is True
+    assert ask(Q.invertible(X.I)) is True
+    assert ask(Q.invertible(Identity(3))) is True
+    assert ask(Q.invertible(ZeroMatrix(3, 3))) is False
+    assert ask(Q.invertible(OneMatrix(1, 1))) is True
+    assert ask(Q.invertible(OneMatrix(3, 3))) is False
+    assert ask(Q.invertible(X), Q.fullrank(X) & Q.square(X))
+
+def test_singular():
+    assert ask(Q.singular(X)) is None
+    assert ask(Q.singular(X), Q.invertible(X)) is False
+    assert ask(Q.singular(X), ~Q.invertible(X)) is True
+
+@XFAIL
+def test_invertible_fullrank():
+    assert ask(Q.invertible(X), Q.fullrank(X)) is True
+
+
+def test_invertible_BlockMatrix():
+    assert ask(Q.invertible(BlockMatrix([Identity(3)]))) == True
+    assert ask(Q.invertible(BlockMatrix([ZeroMatrix(3, 3)]))) == False
+
+    X = Matrix([[1, 2, 3], [3, 5, 4]])
+    Y = Matrix([[4, 2, 7], [2, 3, 5]])
+    # non-invertible A block
+    assert ask(Q.invertible(BlockMatrix([
+        [Matrix.ones(3, 3), Y.T],
+        [X, Matrix.eye(2)],
+    ]))) == True
+    # non-invertible B block
+    assert ask(Q.invertible(BlockMatrix([
+        [Y.T, Matrix.ones(3, 3)],
+        [Matrix.eye(2), X],
+    ]))) == True
+    # non-invertible C block
+    assert ask(Q.invertible(BlockMatrix([
+        [X, Matrix.eye(2)],
+        [Matrix.ones(3, 3), Y.T],
+    ]))) == True
+    # non-invertible D block
+    assert ask(Q.invertible(BlockMatrix([
+        [Matrix.eye(2), X],
+        [Y.T, Matrix.ones(3, 3)],
+    ]))) == True
+
+
+def test_invertible_BlockDiagMatrix():
+    assert ask(Q.invertible(BlockDiagMatrix(Identity(3), Identity(5)))) == True
+    assert ask(Q.invertible(BlockDiagMatrix(ZeroMatrix(3, 3), Identity(5)))) == False
+    assert ask(Q.invertible(BlockDiagMatrix(Identity(3), OneMatrix(5, 5)))) == False
+
+
+def test_symmetric():
+    assert ask(Q.symmetric(X), Q.symmetric(X))
+    assert ask(Q.symmetric(X*Z), Q.symmetric(X)) is None
+    assert ask(Q.symmetric(X*Z), Q.symmetric(X) & Q.symmetric(Z)) is True
+    assert ask(Q.symmetric(X + Z), Q.symmetric(X) & Q.symmetric(Z)) is True
+    assert ask(Q.symmetric(Y)) is False
+    assert ask(Q.symmetric(Y*Y.T)) is True
+    assert ask(Q.symmetric(Y.T*X*Y)) is None
+    assert ask(Q.symmetric(Y.T*X*Y), Q.symmetric(X)) is True
+    assert ask(Q.symmetric(X**10), Q.symmetric(X)) is True
+    assert ask(Q.symmetric(A1x1)) is True
+    assert ask(Q.symmetric(A1x1 + B1x1)) is True
+    assert ask(Q.symmetric(A1x1 * B1x1)) is True
+    assert ask(Q.symmetric(V1.T*V1)) is True
+    assert ask(Q.symmetric(V1.T*(V1 + V2))) is True
+    assert ask(Q.symmetric(V1.T*(V1 + V2) + A1x1)) is True
+    assert ask(Q.symmetric(MatrixSlice(Y, (0, 1), (1, 2)))) is True
+    assert ask(Q.symmetric(Identity(3))) is True
+    assert ask(Q.symmetric(ZeroMatrix(3, 3))) is True
+    assert ask(Q.symmetric(OneMatrix(3, 3))) is True
+
+def _test_orthogonal_unitary(predicate):
+    assert ask(predicate(X), predicate(X))
+    assert ask(predicate(X.T), predicate(X)) is True
+    assert ask(predicate(X.I), predicate(X)) is True
+    assert ask(predicate(X**2), predicate(X))
+    assert ask(predicate(Y)) is False
+    assert ask(predicate(X)) is None
+    assert ask(predicate(X), ~Q.invertible(X)) is False
+    assert ask(predicate(X*Z*X), predicate(X) & predicate(Z)) is True
+    assert ask(predicate(Identity(3))) is True
+    assert ask(predicate(ZeroMatrix(3, 3))) is False
+    assert ask(Q.invertible(X), predicate(X))
+    assert not ask(predicate(X + Z), predicate(X) & predicate(Z))
+
+def test_orthogonal():
+    _test_orthogonal_unitary(Q.orthogonal)
+
+def test_unitary():
+    _test_orthogonal_unitary(Q.unitary)
+    assert ask(Q.unitary(X), Q.orthogonal(X))
+
+def test_fullrank():
+    assert ask(Q.fullrank(X), Q.fullrank(X))
+    assert ask(Q.fullrank(X**2), Q.fullrank(X))
+    assert ask(Q.fullrank(X.T), Q.fullrank(X)) is True
+    assert ask(Q.fullrank(X)) is None
+    assert ask(Q.fullrank(Y)) is None
+    assert ask(Q.fullrank(X*Z), Q.fullrank(X) & Q.fullrank(Z)) is True
+    assert ask(Q.fullrank(Identity(3))) is True
+    assert ask(Q.fullrank(ZeroMatrix(3, 3))) is False
+    assert ask(Q.fullrank(OneMatrix(1, 1))) is True
+    assert ask(Q.fullrank(OneMatrix(3, 3))) is False
+    assert ask(Q.invertible(X), ~Q.fullrank(X)) == False
+
+
+def test_positive_definite():
+    assert ask(Q.positive_definite(X), Q.positive_definite(X))
+    assert ask(Q.positive_definite(X.T), Q.positive_definite(X)) is True
+    assert ask(Q.positive_definite(X.I), Q.positive_definite(X)) is True
+    assert ask(Q.positive_definite(Y)) is False
+    assert ask(Q.positive_definite(X)) is None
+    assert ask(Q.positive_definite(X**3), Q.positive_definite(X))
+    assert ask(Q.positive_definite(X*Z*X),
+            Q.positive_definite(X) & Q.positive_definite(Z)) is True
+    assert ask(Q.positive_definite(X), Q.orthogonal(X))
+    assert ask(Q.positive_definite(Y.T*X*Y),
+            Q.positive_definite(X) & Q.fullrank(Y)) is True
+    assert not ask(Q.positive_definite(Y.T*X*Y), Q.positive_definite(X))
+    assert ask(Q.positive_definite(Identity(3))) is True
+    assert ask(Q.positive_definite(ZeroMatrix(3, 3))) is False
+    assert ask(Q.positive_definite(OneMatrix(1, 1))) is True
+    assert ask(Q.positive_definite(OneMatrix(3, 3))) is False
+    assert ask(Q.positive_definite(X + Z), Q.positive_definite(X) &
+            Q.positive_definite(Z)) is True
+    assert not ask(Q.positive_definite(-X), Q.positive_definite(X))
+    assert ask(Q.positive(X[1, 1]), Q.positive_definite(X))
+
+def test_triangular():
+    assert ask(Q.upper_triangular(X + Z.T + Identity(2)), Q.upper_triangular(X) &
+            Q.lower_triangular(Z)) is True
+    assert ask(Q.upper_triangular(X*Z.T), Q.upper_triangular(X) &
+            Q.lower_triangular(Z)) is True
+    assert ask(Q.lower_triangular(Identity(3))) is True
+    assert ask(Q.lower_triangular(ZeroMatrix(3, 3))) is True
+    assert ask(Q.upper_triangular(ZeroMatrix(3, 3))) is True
+    assert ask(Q.lower_triangular(OneMatrix(1, 1))) is True
+    assert ask(Q.upper_triangular(OneMatrix(1, 1))) is True
+    assert ask(Q.lower_triangular(OneMatrix(3, 3))) is False
+    assert ask(Q.upper_triangular(OneMatrix(3, 3))) is False
+    assert ask(Q.triangular(X), Q.unit_triangular(X))
+    assert ask(Q.upper_triangular(X**3), Q.upper_triangular(X))
+    assert ask(Q.lower_triangular(X**3), Q.lower_triangular(X))
+
+
+def test_diagonal():
+    assert ask(Q.diagonal(X + Z.T + Identity(2)), Q.diagonal(X) &
+               Q.diagonal(Z)) is True
+    assert ask(Q.diagonal(ZeroMatrix(3, 3)))
+    assert ask(Q.diagonal(OneMatrix(1, 1))) is True
+    assert ask(Q.diagonal(OneMatrix(3, 3))) is False
+    assert ask(Q.lower_triangular(X) & Q.upper_triangular(X), Q.diagonal(X))
+    assert ask(Q.diagonal(X), Q.lower_triangular(X) & Q.upper_triangular(X))
+    assert ask(Q.symmetric(X), Q.diagonal(X))
+    assert ask(Q.triangular(X), Q.diagonal(X))
+    assert ask(Q.diagonal(C0x0))
+    assert ask(Q.diagonal(A1x1))
+    assert ask(Q.diagonal(A1x1 + B1x1))
+    assert ask(Q.diagonal(A1x1*B1x1))
+    assert ask(Q.diagonal(V1.T*V2))
+    assert ask(Q.diagonal(V1.T*(X + Z)*V1))
+    assert ask(Q.diagonal(MatrixSlice(Y, (0, 1), (1, 2)))) is True
+    assert ask(Q.diagonal(V1.T*(V1 + V2))) is True
+    assert ask(Q.diagonal(X**3), Q.diagonal(X))
+    assert ask(Q.diagonal(Identity(3)))
+    assert ask(Q.diagonal(DiagMatrix(V1)))
+    assert ask(Q.diagonal(DiagonalMatrix(X)))
+
+
+def test_non_atoms():
+    assert ask(Q.real(Trace(X)), Q.positive(Trace(X)))
+
+@XFAIL
+def test_non_trivial_implies():
+    X = MatrixSymbol('X', 3, 3)
+    Y = MatrixSymbol('Y', 3, 3)
+    assert ask(Q.lower_triangular(X+Y), Q.lower_triangular(X) &
+               Q.lower_triangular(Y)) is True
+    assert ask(Q.triangular(X), Q.lower_triangular(X)) is True
+    assert ask(Q.triangular(X+Y), Q.lower_triangular(X) &
+               Q.lower_triangular(Y)) is True
+
+def test_MatrixSlice():
+    X = MatrixSymbol('X', 4, 4)
+    B = MatrixSlice(X, (1, 3), (1, 3))
+    C = MatrixSlice(X, (0, 3), (1, 3))
+    assert ask(Q.symmetric(B), Q.symmetric(X))
+    assert ask(Q.invertible(B), Q.invertible(X))
+    assert ask(Q.diagonal(B), Q.diagonal(X))
+    assert ask(Q.orthogonal(B), Q.orthogonal(X))
+    assert ask(Q.upper_triangular(B), Q.upper_triangular(X))
+
+    assert not ask(Q.symmetric(C), Q.symmetric(X))
+    assert not ask(Q.invertible(C), Q.invertible(X))
+    assert not ask(Q.diagonal(C), Q.diagonal(X))
+    assert not ask(Q.orthogonal(C), Q.orthogonal(X))
+    assert not ask(Q.upper_triangular(C), Q.upper_triangular(X))
+
+def test_det_trace_positive():
+    X = MatrixSymbol('X', 4, 4)
+    assert ask(Q.positive(Trace(X)), Q.positive_definite(X))
+    assert ask(Q.positive(Determinant(X)), Q.positive_definite(X))
+
+def test_field_assumptions():
+    X = MatrixSymbol('X', 4, 4)
+    Y = MatrixSymbol('Y', 4, 4)
+    assert ask(Q.real_elements(X), Q.real_elements(X))
+    assert not ask(Q.integer_elements(X), Q.real_elements(X))
+    assert ask(Q.complex_elements(X), Q.real_elements(X))
+    assert ask(Q.complex_elements(X**2), Q.real_elements(X))
+    assert ask(Q.real_elements(X**2), Q.integer_elements(X))
+    assert ask(Q.real_elements(X+Y), Q.real_elements(X)) is None
+    assert ask(Q.real_elements(X+Y), Q.real_elements(X) & Q.real_elements(Y))
+    from sympy.matrices.expressions.hadamard import HadamardProduct
+    assert ask(Q.real_elements(HadamardProduct(X, Y)),
+                    Q.real_elements(X) & Q.real_elements(Y))
+    assert ask(Q.complex_elements(X+Y), Q.real_elements(X) & Q.complex_elements(Y))
+
+    assert ask(Q.real_elements(X.T), Q.real_elements(X))
+    assert ask(Q.real_elements(X.I), Q.real_elements(X) & Q.invertible(X))
+    assert ask(Q.real_elements(Trace(X)), Q.real_elements(X))
+    assert ask(Q.integer_elements(Determinant(X)), Q.integer_elements(X))
+    assert not ask(Q.integer_elements(X.I), Q.integer_elements(X))
+    alpha = Symbol('alpha')
+    assert ask(Q.real_elements(alpha*X), Q.real_elements(X) & Q.real(alpha))
+    assert ask(Q.real_elements(LofLU(X)), Q.real_elements(X))
+    e = Symbol('e', integer=True, negative=True)
+    assert ask(Q.real_elements(X**e), Q.real_elements(X) & Q.invertible(X))
+    assert ask(Q.real_elements(X**e), Q.real_elements(X)) is None
+
+def test_matrix_element_sets():
+    X = MatrixSymbol('X', 4, 4)
+    assert ask(Q.real(X[1, 2]), Q.real_elements(X))
+    assert ask(Q.integer(X[1, 2]), Q.integer_elements(X))
+    assert ask(Q.complex(X[1, 2]), Q.complex_elements(X))
+    assert ask(Q.integer_elements(Identity(3)))
+    assert ask(Q.integer_elements(ZeroMatrix(3, 3)))
+    assert ask(Q.integer_elements(OneMatrix(3, 3)))
+    from sympy.matrices.expressions.fourier import DFT
+    assert ask(Q.complex_elements(DFT(3)))
+
+
+def test_matrix_element_sets_slices_blocks():
+    X = MatrixSymbol('X', 4, 4)
+    assert ask(Q.integer_elements(X[:, 3]), Q.integer_elements(X))
+    assert ask(Q.integer_elements(BlockMatrix([[X], [X]])),
+                        Q.integer_elements(X))
+
+def test_matrix_element_sets_determinant_trace():
+    assert ask(Q.integer(Determinant(X)), Q.integer_elements(X))
+    assert ask(Q.integer(Trace(X)), Q.integer_elements(X))

lib/python3.12/site-packages/sympy/assumptions/tests/test_refine.py

@@ -0,0 +1,227 @@
+from sympy.assumptions.ask import Q
+from sympy.assumptions.refine import refine
+from sympy.core.expr import Expr
+from sympy.core.numbers import (I, Rational, nan, pi)
+from sympy.core.singleton import S
+from sympy.core.symbol import Symbol
+from sympy.functions.elementary.complexes import (Abs, arg, im, re, sign)
+from sympy.functions.elementary.exponential import exp
+from sympy.functions.elementary.miscellaneous import sqrt
+from sympy.functions.elementary.trigonometric import (atan, atan2)
+from sympy.abc import w, x, y, z
+from sympy.core.relational import Eq, Ne
+from sympy.functions.elementary.piecewise import Piecewise
+from sympy.matrices.expressions.matexpr import MatrixSymbol
+
+
+def test_Abs():
+    assert refine(Abs(x), Q.positive(x)) == x
+    assert refine(1 + Abs(x), Q.positive(x)) == 1 + x
+    assert refine(Abs(x), Q.negative(x)) == -x
+    assert refine(1 + Abs(x), Q.negative(x)) == 1 - x
+
+    assert refine(Abs(x**2)) != x**2
+    assert refine(Abs(x**2), Q.real(x)) == x**2
+
+
+def test_pow1():
+    assert refine((-1)**x, Q.even(x)) == 1
+    assert refine((-1)**x, Q.odd(x)) == -1
+    assert refine((-2)**x, Q.even(x)) == 2**x
+
+    # nested powers
+    assert refine(sqrt(x**2)) != Abs(x)
+    assert refine(sqrt(x**2), Q.complex(x)) != Abs(x)
+    assert refine(sqrt(x**2), Q.real(x)) == Abs(x)
+    assert refine(sqrt(x**2), Q.positive(x)) == x
+    assert refine((x**3)**Rational(1, 3)) != x
+
+    assert refine((x**3)**Rational(1, 3), Q.real(x)) != x
+    assert refine((x**3)**Rational(1, 3), Q.positive(x)) == x
+
+    assert refine(sqrt(1/x), Q.real(x)) != 1/sqrt(x)
+    assert refine(sqrt(1/x), Q.positive(x)) == 1/sqrt(x)
+
+    # powers of (-1)
+    assert refine((-1)**(x + y), Q.even(x)) == (-1)**y
+    assert refine((-1)**(x + y + z), Q.odd(x) & Q.odd(z)) == (-1)**y
+    assert refine((-1)**(x + y + 1), Q.odd(x)) == (-1)**y
+    assert refine((-1)**(x + y + 2), Q.odd(x)) == (-1)**(y + 1)
+    assert refine((-1)**(x + 3)) == (-1)**(x + 1)
+
+    # continuation
+    assert refine((-1)**((-1)**x/2 - S.Half), Q.integer(x)) == (-1)**x
+    assert refine((-1)**((-1)**x/2 + S.Half), Q.integer(x)) == (-1)**(x + 1)
+    assert refine((-1)**((-1)**x/2 + 5*S.Half), Q.integer(x)) == (-1)**(x + 1)
+
+
+def test_pow2():
+    assert refine((-1)**((-1)**x/2 - 7*S.Half), Q.integer(x)) == (-1)**(x + 1)
+    assert refine((-1)**((-1)**x/2 - 9*S.Half), Q.integer(x)) == (-1)**x
+
+    # powers of Abs
+    assert refine(Abs(x)**2, Q.real(x)) == x**2
+    assert refine(Abs(x)**3, Q.real(x)) == Abs(x)**3
+    assert refine(Abs(x)**2) == Abs(x)**2
+
+
+def test_exp():
+    x = Symbol('x', integer=True)
+    assert refine(exp(pi*I*2*x)) == 1
+    assert refine(exp(pi*I*2*(x + S.Half))) == -1
+    assert refine(exp(pi*I*2*(x + Rational(1, 4)))) == I
+    assert refine(exp(pi*I*2*(x + Rational(3, 4)))) == -I
+
+
+def test_Piecewise():
+    assert refine(Piecewise((1, x < 0), (3, True)), (x < 0)) == 1
+    assert refine(Piecewise((1, x < 0), (3, True)), ~(x < 0)) == 3
+    assert refine(Piecewise((1, x < 0), (3, True)), (y < 0)) == \
+        Piecewise((1, x < 0), (3, True))
+    assert refine(Piecewise((1, x > 0), (3, True)), (x > 0)) == 1
+    assert refine(Piecewise((1, x > 0), (3, True)), ~(x > 0)) == 3
+    assert refine(Piecewise((1, x > 0), (3, True)), (y > 0)) == \
+        Piecewise((1, x > 0), (3, True))
+    assert refine(Piecewise((1, x <= 0), (3, True)), (x <= 0)) == 1
+    assert refine(Piecewise((1, x <= 0), (3, True)), ~(x <= 0)) == 3
+    assert refine(Piecewise((1, x <= 0), (3, True)), (y <= 0)) == \
+        Piecewise((1, x <= 0), (3, True))
+    assert refine(Piecewise((1, x >= 0), (3, True)), (x >= 0)) == 1
+    assert refine(Piecewise((1, x >= 0), (3, True)), ~(x >= 0)) == 3
+    assert refine(Piecewise((1, x >= 0), (3, True)), (y >= 0)) == \
+        Piecewise((1, x >= 0), (3, True))
+    assert refine(Piecewise((1, Eq(x, 0)), (3, True)), (Eq(x, 0)))\
+        == 1
+    assert refine(Piecewise((1, Eq(x, 0)), (3, True)), (Eq(0, x)))\
+        == 1
+    assert refine(Piecewise((1, Eq(x, 0)), (3, True)), ~(Eq(x, 0)))\
+        == 3
+    assert refine(Piecewise((1, Eq(x, 0)), (3, True)), ~(Eq(0, x)))\
+        == 3
+    assert refine(Piecewise((1, Eq(x, 0)), (3, True)), (Eq(y, 0)))\
+        == Piecewise((1, Eq(x, 0)), (3, True))
+    assert refine(Piecewise((1, Ne(x, 0)), (3, True)), (Ne(x, 0)))\
+        == 1
+    assert refine(Piecewise((1, Ne(x, 0)), (3, True)), ~(Ne(x, 0)))\
+        == 3
+    assert refine(Piecewise((1, Ne(x, 0)), (3, True)), (Ne(y, 0)))\
+        == Piecewise((1, Ne(x, 0)), (3, True))
+
+
+def test_atan2():
+    assert refine(atan2(y, x), Q.real(y) & Q.positive(x)) == atan(y/x)
+    assert refine(atan2(y, x), Q.negative(y) & Q.positive(x)) == atan(y/x)
+    assert refine(atan2(y, x), Q.negative(y) & Q.negative(x)) == atan(y/x) - pi
+    assert refine(atan2(y, x), Q.positive(y) & Q.negative(x)) == atan(y/x) + pi
+    assert refine(atan2(y, x), Q.zero(y) & Q.negative(x)) == pi
+    assert refine(atan2(y, x), Q.positive(y) & Q.zero(x)) == pi/2
+    assert refine(atan2(y, x), Q.negative(y) & Q.zero(x)) == -pi/2
+    assert refine(atan2(y, x), Q.zero(y) & Q.zero(x)) is nan
+
+
+def test_re():
+    assert refine(re(x), Q.real(x)) == x
+    assert refine(re(x), Q.imaginary(x)) is S.Zero
+    assert refine(re(x+y), Q.real(x) & Q.real(y)) == x + y
+    assert refine(re(x+y), Q.real(x) & Q.imaginary(y)) == x
+    assert refine(re(x*y), Q.real(x) & Q.real(y)) == x * y
+    assert refine(re(x*y), Q.real(x) & Q.imaginary(y)) == 0
+    assert refine(re(x*y*z), Q.real(x) & Q.real(y) & Q.real(z)) == x * y * z
+
+
+def test_im():
+    assert refine(im(x), Q.imaginary(x)) == -I*x
+    assert refine(im(x), Q.real(x)) is S.Zero
+    assert refine(im(x+y), Q.imaginary(x) & Q.imaginary(y)) == -I*x - I*y
+    assert refine(im(x+y), Q.real(x) & Q.imaginary(y)) == -I*y
+    assert refine(im(x*y), Q.imaginary(x) & Q.real(y)) == -I*x*y
+    assert refine(im(x*y), Q.imaginary(x) & Q.imaginary(y)) == 0
+    assert refine(im(1/x), Q.imaginary(x)) == -I/x
+    assert refine(im(x*y*z), Q.imaginary(x) & Q.imaginary(y)
+        & Q.imaginary(z)) == -I*x*y*z
+
+
+def test_complex():
+    assert refine(re(1/(x + I*y)), Q.real(x) & Q.real(y)) == \
+        x/(x**2 + y**2)
+    assert refine(im(1/(x + I*y)), Q.real(x) & Q.real(y)) == \
+        -y/(x**2 + y**2)
+    assert refine(re((w + I*x) * (y + I*z)), Q.real(w) & Q.real(x) & Q.real(y)
+        & Q.real(z)) == w*y - x*z
+    assert refine(im((w + I*x) * (y + I*z)), Q.real(w) & Q.real(x) & Q.real(y)
+        & Q.real(z)) == w*z + x*y
+
+
+def test_sign():
+    x = Symbol('x', real = True)
+    assert refine(sign(x), Q.positive(x)) == 1
+    assert refine(sign(x), Q.negative(x)) == -1
+    assert refine(sign(x), Q.zero(x)) == 0
+    assert refine(sign(x), True) == sign(x)
+    assert refine(sign(Abs(x)), Q.nonzero(x)) == 1
+
+    x = Symbol('x', imaginary=True)
+    assert refine(sign(x), Q.positive(im(x))) == S.ImaginaryUnit
+    assert refine(sign(x), Q.negative(im(x))) == -S.ImaginaryUnit
+    assert refine(sign(x), True) == sign(x)
+
+    x = Symbol('x', complex=True)
+    assert refine(sign(x), Q.zero(x)) == 0
+
+def test_arg():
+    x = Symbol('x', complex = True)
+    assert refine(arg(x), Q.positive(x)) == 0
+    assert refine(arg(x), Q.negative(x)) == pi
+
+def test_func_args():
+    class MyClass(Expr):
+        # A class with nontrivial .func
+
+        def __init__(self, *args):
+            self.my_member = ""
+
+        @property
+        def func(self):
+            def my_func(*args):
+                obj = MyClass(*args)
+                obj.my_member = self.my_member
+                return obj
+            return my_func
+
+    x = MyClass()
+    x.my_member = "A very important value"
+    assert x.my_member == refine(x).my_member
+
+def test_issue_refine_9384():
+    assert refine(Piecewise((1, x < 0), (0, True)), Q.positive(x)) == 0
+    assert refine(Piecewise((1, x < 0), (0, True)), Q.negative(x)) == 1
+    assert refine(Piecewise((1, x > 0), (0, True)), Q.positive(x)) == 1
+    assert refine(Piecewise((1, x > 0), (0, True)), Q.negative(x)) == 0
+
+
+def test_eval_refine():
+    class MockExpr(Expr):
+        def _eval_refine(self, assumptions):
+            return True
+
+    mock_obj = MockExpr()
+    assert refine(mock_obj)
+
+def test_refine_issue_12724():
+    expr1 = refine(Abs(x * y), Q.positive(x))
+    expr2 = refine(Abs(x * y * z), Q.positive(x))
+    assert expr1 == x * Abs(y)
+    assert expr2 == x * Abs(y * z)
+    y1 = Symbol('y1', real = True)
+    expr3 = refine(Abs(x * y1**2 * z), Q.positive(x))
+    assert expr3 == x * y1**2 * Abs(z)
+
+
+def test_matrixelement():
+    x = MatrixSymbol('x', 3, 3)
+    i = Symbol('i', positive = True)
+    j = Symbol('j', positive = True)
+    assert refine(x[0, 1], Q.symmetric(x)) == x[0, 1]
+    assert refine(x[1, 0], Q.symmetric(x)) == x[0, 1]
+    assert refine(x[i, j], Q.symmetric(x)) == x[j, i]
+    assert refine(x[j, i], Q.symmetric(x)) == x[j, i]

lib/python3.12/site-packages/sympy/assumptions/tests/test_rel_queries.py

@@ -0,0 +1,172 @@
+from sympy.assumptions.lra_satask import lra_satask
+from sympy.logic.algorithms.lra_theory import UnhandledInput
+from sympy.assumptions.ask import Q, ask
+
+from sympy.core import symbols, Symbol
+from sympy.matrices.expressions.matexpr import MatrixSymbol
+from sympy.core.numbers import I
+
+from sympy.testing.pytest import raises, XFAIL
+x, y, z = symbols("x y z", real=True)
+
+def test_lra_satask():
+    im = Symbol('im', imaginary=True)
+
+    # test preprocessing of unequalities is working correctly
+    assert lra_satask(Q.eq(x, 1), ~Q.ne(x, 0)) is False
+    assert lra_satask(Q.eq(x, 0), ~Q.ne(x, 0)) is True
+    assert lra_satask(~Q.ne(x, 0), Q.eq(x, 0)) is True
+    assert lra_satask(~Q.eq(x, 0), Q.eq(x, 0)) is False
+    assert lra_satask(Q.ne(x, 0), Q.eq(x, 0)) is False
+
+    # basic tests
+    assert lra_satask(Q.ne(x, x)) is False
+    assert lra_satask(Q.eq(x, x)) is True
+    assert lra_satask(Q.gt(x, 0), Q.gt(x, 1)) is True
+
+    # check that True/False are handled
+    assert lra_satask(Q.gt(x, 0), True) is None
+    assert raises(ValueError, lambda: lra_satask(Q.gt(x, 0), False))
+
+    # check imaginary numbers are correctly handled
+    # (im * I).is_real returns True so this is an edge case
+    raises(UnhandledInput, lambda: lra_satask(Q.gt(im * I, 0), Q.gt(im * I, 0)))
+
+    # check matrix inputs
+    X = MatrixSymbol("X", 2, 2)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(X, 2) & Q.gt(X, 3)))
+
+
+def test_old_assumptions():
+    # test unhandled old assumptions
+    w = symbols("w")
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", rational=False, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", odd=True, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", even=True, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", prime=True, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", composite=True, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", integer=True, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+    w = symbols("w", integer=False, real=True)
+    raises(UnhandledInput, lambda: lra_satask(Q.lt(w, 2) & Q.gt(w, 3)))
+
+    # test handled
+    w = symbols("w", positive=True, real=True)
+    assert lra_satask(Q.le(w, 0)) is False
+    assert lra_satask(Q.gt(w, 0)) is True
+    w = symbols("w", negative=True, real=True)
+    assert lra_satask(Q.lt(w, 0)) is True
+    assert lra_satask(Q.ge(w, 0)) is False
+    w = symbols("w", zero=True, real=True)
+    assert lra_satask(Q.eq(w, 0)) is True
+    assert lra_satask(Q.ne(w, 0)) is False
+    w = symbols("w", nonzero=True, real=True)
+    assert lra_satask(Q.ne(w, 0)) is True
+    assert lra_satask(Q.eq(w, 1)) is None
+    w = symbols("w", nonpositive=True, real=True)
+    assert lra_satask(Q.le(w, 0)) is True
+    assert lra_satask(Q.gt(w, 0)) is False
+    w = symbols("w", nonnegative=True, real=True)
+    assert lra_satask(Q.ge(w, 0)) is True
+    assert lra_satask(Q.lt(w, 0)) is False
+
+
+def test_rel_queries():
+    assert ask(Q.lt(x, 2) & Q.gt(x, 3)) is False
+    assert ask(Q.positive(x - z), (x > y) & (y > z)) is True
+    assert ask(x + y > 2, (x < 0) & (y <0)) is False
+    assert ask(x > z, (x > y) & (y > z)) is True
+
+
+def test_unhandled_queries():
+    X = MatrixSymbol("X", 2, 2)
+    assert ask(Q.lt(X, 2) & Q.gt(X, 3)) is None
+
+
+def test_all_pred():
+    # test usable pred
+    assert lra_satask(Q.extended_positive(x), (x > 2)) is True
+    assert lra_satask(Q.positive_infinite(x)) is False
+    assert lra_satask(Q.negative_infinite(x)) is False
+
+    # test disallowed pred
+    raises(UnhandledInput, lambda: lra_satask((x > 0), (x > 2) & Q.prime(x)))
+    raises(UnhandledInput, lambda: lra_satask((x > 0), (x > 2) & Q.composite(x)))
+    raises(UnhandledInput, lambda: lra_satask((x > 0), (x > 2) & Q.odd(x)))
+    raises(UnhandledInput, lambda: lra_satask((x > 0), (x > 2) & Q.even(x)))
+    raises(UnhandledInput, lambda: lra_satask((x > 0), (x > 2) & Q.integer(x)))
+
+
+def test_number_line_properties():
+    # From:
+    # https://en.wikipedia.org/wiki/Inequality_(mathematics)#Properties_on_the_number_line
+
+    a, b, c = symbols("a b c", real=True)
+
+    # Transitivity
+    # If a <= b and b <= c, then a <= c.
+    assert ask(a <= c, (a <= b) & (b <= c)) is True
+    # If a <= b and b < c, then a < c.
+    assert ask(a < c, (a <= b) & (b < c)) is True
+    # If a < b and b <= c, then a < c.
+    assert ask(a < c, (a < b) & (b <= c)) is True
+
+    # Addition and subtraction
+    # If a <= b, then a + c <= b + c and a - c <= b - c.
+    assert ask(a + c <= b + c, a <= b) is True
+    assert ask(a - c <= b - c, a <= b) is True
+
+
+@XFAIL
+def test_failing_number_line_properties():
+    # From:
+    # https://en.wikipedia.org/wiki/Inequality_(mathematics)#Properties_on_the_number_line
+
+    a, b, c = symbols("a b c", real=True)
+
+    # Multiplication and division
+    # If a <= b and c > 0, then ac <= bc and a/c <= b/c. (True for non-zero c)
+    assert ask(a*c <= b*c, (a <= b) & (c > 0) & ~ Q.zero(c)) is True
+    assert ask(a/c <= b/c, (a <= b) & (c > 0) & ~ Q.zero(c)) is True
+    # If a <= b and c < 0, then ac >= bc and a/c >= b/c. (True for non-zero c)
+    assert ask(a*c >= b*c, (a <= b) & (c < 0) & ~ Q.zero(c)) is True
+    assert ask(a/c >= b/c, (a <= b) & (c < 0) & ~ Q.zero(c)) is True
+
+    # Additive inverse
+    # If a <= b, then -a >= -b.
+    assert ask(-a >= -b, a <= b) is True
+
+    # Multiplicative inverse
+    # For a, b that are both negative or both positive:
+    # If a <= b, then 1/a >= 1/b .
+    assert ask(1/a >= 1/b, (a <= b) & Q.positive(x) & Q.positive(b)) is True
+    assert ask(1/a >= 1/b, (a <= b) & Q.negative(x) & Q.negative(b)) is True
+
+
+def test_equality():
+    # test symetry and reflexivity
+    assert ask(Q.eq(x, x)) is True
+    assert ask(Q.eq(y, x), Q.eq(x, y)) is True
+    assert ask(Q.eq(y, x), ~Q.eq(z, z) | Q.eq(x, y)) is True
+
+    # test transitivity
+    assert ask(Q.eq(x,z), Q.eq(x,y) & Q.eq(y,z)) is True
+
+
+@XFAIL
+def test_equality_failing():
+    # Note that implementing the substitution property of equality
+    # most likely requires a redesign of the new assumptions.
+    # See issue #25485 for why this is the case and general ideas
+    # about how things could be redesigned.
+
+    # test substitution property
+    assert ask(Q.prime(x), Q.eq(x, y) & Q.prime(y)) is True
+    assert ask(Q.real(x), Q.eq(x, y) & Q.real(y)) is True
+    assert ask(Q.imaginary(x), Q.eq(x, y) & Q.imaginary(y)) is True

lib/python3.12/site-packages/sympy/assumptions/tests/test_satask.py

@@ -0,0 +1,378 @@
+from sympy.assumptions.ask import Q
+from sympy.assumptions.assume import assuming
+from sympy.core.numbers import (I, pi)
+from sympy.core.relational import (Eq, Gt)
+from sympy.core.singleton import S
+from sympy.core.symbol import symbols
+from sympy.functions.elementary.complexes import Abs
+from sympy.logic.boolalg import Implies
+from sympy.matrices.expressions.matexpr import MatrixSymbol
+from sympy.assumptions.cnf import CNF, Literal
+from sympy.assumptions.satask import (satask, extract_predargs,
+    get_relevant_clsfacts)
+
+from sympy.testing.pytest import raises, XFAIL
+
+
+x, y, z = symbols('x y z')
+
+
+def test_satask():
+    # No relevant facts
+    assert satask(Q.real(x), Q.real(x)) is True
+    assert satask(Q.real(x), ~Q.real(x)) is False
+    assert satask(Q.real(x)) is None
+
+    assert satask(Q.real(x), Q.positive(x)) is True
+    assert satask(Q.positive(x), Q.real(x)) is None
+    assert satask(Q.real(x), ~Q.positive(x)) is None
+    assert satask(Q.positive(x), ~Q.real(x)) is False
+
+    raises(ValueError, lambda: satask(Q.real(x), Q.real(x) & ~Q.real(x)))
+
+    with assuming(Q.positive(x)):
+        assert satask(Q.real(x)) is True
+        assert satask(~Q.positive(x)) is False
+        raises(ValueError, lambda: satask(Q.real(x), ~Q.positive(x)))
+
+    assert satask(Q.zero(x), Q.nonzero(x)) is False
+    assert satask(Q.positive(x), Q.zero(x)) is False
+    assert satask(Q.real(x), Q.zero(x)) is True
+    assert satask(Q.zero(x), Q.zero(x*y)) is None
+    assert satask(Q.zero(x*y), Q.zero(x))
+
+
+def test_zero():
+    """
+    Everything in this test doesn't work with the ask handlers, and most
+    things would be very difficult or impossible to make work under that
+    model.
+
+    """
+    assert satask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) is True
+    assert satask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) is True
+
+    assert satask(Implies(Q.zero(x), Q.zero(x*y))) is True
+
+    # This one in particular requires computing the fixed-point of the
+    # relevant facts, because going from Q.nonzero(x*y) -> ~Q.zero(x*y) and
+    # Q.zero(x*y) -> Equivalent(Q.zero(x*y), Q.zero(x) | Q.zero(y)) takes two
+    # steps.
+    assert satask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) is False
+
+    assert satask(Q.zero(x), Q.zero(x**2)) is True
+
+
+def test_zero_positive():
+    assert satask(Q.zero(x + y), Q.positive(x) & Q.positive(y)) is False
+    assert satask(Q.positive(x) & Q.positive(y), Q.zero(x + y)) is False
+    assert satask(Q.nonzero(x + y), Q.positive(x) & Q.positive(y)) is True
+    assert satask(Q.positive(x) & Q.positive(y), Q.nonzero(x + y)) is None
+
+    # This one requires several levels of forward chaining
+    assert satask(Q.zero(x*(x + y)), Q.positive(x) & Q.positive(y)) is False
+
+    assert satask(Q.positive(pi*x*y + 1), Q.positive(x) & Q.positive(y)) is True
+    assert satask(Q.positive(pi*x*y - 5), Q.positive(x) & Q.positive(y)) is None
+
+
+def test_zero_pow():
+    assert satask(Q.zero(x**y), Q.zero(x) & Q.positive(y)) is True
+    assert satask(Q.zero(x**y), Q.nonzero(x) & Q.zero(y)) is False
+
+    assert satask(Q.zero(x), Q.zero(x**y)) is True
+
+    assert satask(Q.zero(x**y), Q.zero(x)) is None
+
+
+@XFAIL
+# Requires correct Q.square calculation first
+def test_invertible():
+    A = MatrixSymbol('A', 5, 5)
+    B = MatrixSymbol('B', 5, 5)
+    assert satask(Q.invertible(A*B), Q.invertible(A) & Q.invertible(B)) is True
+    assert satask(Q.invertible(A), Q.invertible(A*B)) is True
+    assert satask(Q.invertible(A) & Q.invertible(B), Q.invertible(A*B)) is True
+
+
+def test_prime():
+    assert satask(Q.prime(5)) is True
+    assert satask(Q.prime(6)) is False
+    assert satask(Q.prime(-5)) is False
+
+    assert satask(Q.prime(x*y), Q.integer(x) & Q.integer(y)) is None
+    assert satask(Q.prime(x*y), Q.prime(x) & Q.prime(y)) is False
+
+
+def test_old_assump():
+    assert satask(Q.positive(1)) is True
+    assert satask(Q.positive(-1)) is False
+    assert satask(Q.positive(0)) is False
+    assert satask(Q.positive(I)) is False
+    assert satask(Q.positive(pi)) is True
+
+    assert satask(Q.negative(1)) is False
+    assert satask(Q.negative(-1)) is True
+    assert satask(Q.negative(0)) is False
+    assert satask(Q.negative(I)) is False
+    assert satask(Q.negative(pi)) is False
+
+    assert satask(Q.zero(1)) is False
+    assert satask(Q.zero(-1)) is False
+    assert satask(Q.zero(0)) is True
+    assert satask(Q.zero(I)) is False
+    assert satask(Q.zero(pi)) is False
+
+    assert satask(Q.nonzero(1)) is True
+    assert satask(Q.nonzero(-1)) is True
+    assert satask(Q.nonzero(0)) is False
+    assert satask(Q.nonzero(I)) is False
+    assert satask(Q.nonzero(pi)) is True
+
+    assert satask(Q.nonpositive(1)) is False
+    assert satask(Q.nonpositive(-1)) is True
+    assert satask(Q.nonpositive(0)) is True
+    assert satask(Q.nonpositive(I)) is False
+    assert satask(Q.nonpositive(pi)) is False
+
+    assert satask(Q.nonnegative(1)) is True
+    assert satask(Q.nonnegative(-1)) is False
+    assert satask(Q.nonnegative(0)) is True
+    assert satask(Q.nonnegative(I)) is False
+    assert satask(Q.nonnegative(pi)) is True
+
+
+def test_rational_irrational():
+    assert satask(Q.irrational(2)) is False
+    assert satask(Q.rational(2)) is True
+    assert satask(Q.irrational(pi)) is True
+    assert satask(Q.rational(pi)) is False
+    assert satask(Q.irrational(I)) is False
+    assert satask(Q.rational(I)) is False
+
+    assert satask(Q.irrational(x*y*z), Q.irrational(x) & Q.irrational(y) &
+        Q.rational(z)) is None
+    assert satask(Q.irrational(x*y*z), Q.irrational(x) & Q.rational(y) &
+        Q.rational(z)) is True
+    assert satask(Q.irrational(pi*x*y), Q.rational(x) & Q.rational(y)) is True
+
+    assert satask(Q.irrational(x + y + z), Q.irrational(x) & Q.irrational(y) &
+        Q.rational(z)) is None
+    assert satask(Q.irrational(x + y + z), Q.irrational(x) & Q.rational(y) &
+        Q.rational(z)) is True
+    assert satask(Q.irrational(pi + x + y), Q.rational(x) & Q.rational(y)) is True
+
+    assert satask(Q.irrational(x*y*z), Q.rational(x) & Q.rational(y) &
+        Q.rational(z)) is False
+    assert satask(Q.rational(x*y*z), Q.rational(x) & Q.rational(y) &
+        Q.rational(z)) is True
+
+    assert satask(Q.irrational(x + y + z), Q.rational(x) & Q.rational(y) &
+        Q.rational(z)) is False
+    assert satask(Q.rational(x + y + z), Q.rational(x) & Q.rational(y) &
+        Q.rational(z)) is True
+
+
+def test_even_satask():
+    assert satask(Q.even(2)) is True
+    assert satask(Q.even(3)) is False
+
+    assert satask(Q.even(x*y), Q.even(x) & Q.odd(y)) is True
+    assert satask(Q.even(x*y), Q.even(x) & Q.integer(y)) is True
+    assert satask(Q.even(x*y), Q.even(x) & Q.even(y)) is True
+    assert satask(Q.even(x*y), Q.odd(x) & Q.odd(y)) is False
+    assert satask(Q.even(x*y), Q.even(x)) is None
+    assert satask(Q.even(x*y), Q.odd(x) & Q.integer(y)) is None
+    assert satask(Q.even(x*y), Q.odd(x) & Q.odd(y)) is False
+
+    assert satask(Q.even(abs(x)), Q.even(x)) is True
+    assert satask(Q.even(abs(x)), Q.odd(x)) is False
+    assert satask(Q.even(x), Q.even(abs(x))) is None # x could be complex
+
+
+def test_odd_satask():
+    assert satask(Q.odd(2)) is False
+    assert satask(Q.odd(3)) is True
+
+    assert satask(Q.odd(x*y), Q.even(x) & Q.odd(y)) is False
+    assert satask(Q.odd(x*y), Q.even(x) & Q.integer(y)) is False
+    assert satask(Q.odd(x*y), Q.even(x) & Q.even(y)) is False
+    assert satask(Q.odd(x*y), Q.odd(x) & Q.odd(y)) is True
+    assert satask(Q.odd(x*y), Q.even(x)) is None
+    assert satask(Q.odd(x*y), Q.odd(x) & Q.integer(y)) is None
+    assert satask(Q.odd(x*y), Q.odd(x) & Q.odd(y)) is True
+
+    assert satask(Q.odd(abs(x)), Q.even(x)) is False
+    assert satask(Q.odd(abs(x)), Q.odd(x)) is True
+    assert satask(Q.odd(x), Q.odd(abs(x))) is None # x could be complex
+
+
+def test_integer():
+    assert satask(Q.integer(1)) is True
+    assert satask(Q.integer(S.Half)) is False
+
+    assert satask(Q.integer(x + y), Q.integer(x) & Q.integer(y)) is True
+    assert satask(Q.integer(x + y), Q.integer(x)) is None
+
+    assert satask(Q.integer(x + y), Q.integer(x) & ~Q.integer(y)) is False
+    assert satask(Q.integer(x + y + z), Q.integer(x) & Q.integer(y) &
+        ~Q.integer(z)) is False
+    assert satask(Q.integer(x + y + z), Q.integer(x) & ~Q.integer(y) &
+        ~Q.integer(z)) is None
+    assert satask(Q.integer(x + y + z), Q.integer(x) & ~Q.integer(y)) is None
+    assert satask(Q.integer(x + y), Q.integer(x) & Q.irrational(y)) is False
+
+    assert satask(Q.integer(x*y), Q.integer(x) & Q.integer(y)) is True
+    assert satask(Q.integer(x*y), Q.integer(x)) is None
+
+    assert satask(Q.integer(x*y), Q.integer(x) & ~Q.integer(y)) is None
+    assert satask(Q.integer(x*y), Q.integer(x) & ~Q.rational(y)) is False
+    assert satask(Q.integer(x*y*z), Q.integer(x) & Q.integer(y) &
+        ~Q.rational(z)) is False
+    assert satask(Q.integer(x*y*z), Q.integer(x) & ~Q.rational(y) &
+        ~Q.rational(z)) is None
+    assert satask(Q.integer(x*y*z), Q.integer(x) & ~Q.rational(y)) is None
+    assert satask(Q.integer(x*y), Q.integer(x) & Q.irrational(y)) is False
+
+
+def test_abs():
+    assert satask(Q.nonnegative(abs(x))) is True
+    assert satask(Q.positive(abs(x)), ~Q.zero(x)) is True
+    assert satask(Q.zero(x), ~Q.zero(abs(x))) is False
+    assert satask(Q.zero(x), Q.zero(abs(x))) is True
+    assert satask(Q.nonzero(x), ~Q.zero(abs(x))) is None # x could be complex
+    assert satask(Q.zero(abs(x)), Q.zero(x)) is True
+
+
+def test_imaginary():
+    assert satask(Q.imaginary(2*I)) is True
+    assert satask(Q.imaginary(x*y), Q.imaginary(x)) is None
+    assert satask(Q.imaginary(x*y), Q.imaginary(x) & Q.real(y)) is True
+    assert satask(Q.imaginary(x), Q.real(x)) is False
+    assert satask(Q.imaginary(1)) is False
+    assert satask(Q.imaginary(x*y), Q.real(x) & Q.real(y)) is False
+    assert satask(Q.imaginary(x + y), Q.real(x) & Q.real(y)) is False
+
+
+def test_real():
+    assert satask(Q.real(x*y), Q.real(x) & Q.real(y)) is True
+    assert satask(Q.real(x + y), Q.real(x) & Q.real(y)) is True
+    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y) & Q.real(z)) is True
+    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y)) is None
+    assert satask(Q.real(x*y*z), Q.real(x) & Q.real(y) & Q.imaginary(z)) is False
+    assert satask(Q.real(x + y + z), Q.real(x) & Q.real(y) & Q.real(z)) is True
+    assert satask(Q.real(x + y + z), Q.real(x) & Q.real(y)) is None
+
+
+def test_pos_neg():
+    assert satask(~Q.positive(x), Q.negative(x)) is True
+    assert satask(~Q.negative(x), Q.positive(x)) is True
+    assert satask(Q.positive(x + y), Q.positive(x) & Q.positive(y)) is True
+    assert satask(Q.negative(x + y), Q.negative(x) & Q.negative(y)) is True
+    assert satask(Q.positive(x + y), Q.negative(x) & Q.negative(y)) is False
+    assert satask(Q.negative(x + y), Q.positive(x) & Q.positive(y)) is False
+
+
+def test_pow_pos_neg():
+    assert satask(Q.nonnegative(x**2), Q.positive(x)) is True
+    assert satask(Q.nonpositive(x**2), Q.positive(x)) is False
+    assert satask(Q.positive(x**2), Q.positive(x)) is True
+    assert satask(Q.negative(x**2), Q.positive(x)) is False
+    assert satask(Q.real(x**2), Q.positive(x)) is True
+
+    assert satask(Q.nonnegative(x**2), Q.negative(x)) is True
+    assert satask(Q.nonpositive(x**2), Q.negative(x)) is False
+    assert satask(Q.positive(x**2), Q.negative(x)) is True
+    assert satask(Q.negative(x**2), Q.negative(x)) is False
+    assert satask(Q.real(x**2), Q.negative(x)) is True
+
+    assert satask(Q.nonnegative(x**2), Q.nonnegative(x)) is True
+    assert satask(Q.nonpositive(x**2), Q.nonnegative(x)) is None
+    assert satask(Q.positive(x**2), Q.nonnegative(x)) is None
+    assert satask(Q.negative(x**2), Q.nonnegative(x)) is False
+    assert satask(Q.real(x**2), Q.nonnegative(x)) is True
+
+    assert satask(Q.nonnegative(x**2), Q.nonpositive(x)) is True
+    assert satask(Q.nonpositive(x**2), Q.nonpositive(x)) is None
+    assert satask(Q.positive(x**2), Q.nonpositive(x)) is None
+    assert satask(Q.negative(x**2), Q.nonpositive(x)) is False
+    assert satask(Q.real(x**2), Q.nonpositive(x)) is True
+
+    assert satask(Q.nonnegative(x**3), Q.positive(x)) is True
+    assert satask(Q.nonpositive(x**3), Q.positive(x)) is False
+    assert satask(Q.positive(x**3), Q.positive(x)) is True
+    assert satask(Q.negative(x**3), Q.positive(x)) is False
+    assert satask(Q.real(x**3), Q.positive(x)) is True
+
+    assert satask(Q.nonnegative(x**3), Q.negative(x)) is False
+    assert satask(Q.nonpositive(x**3), Q.negative(x)) is True
+    assert satask(Q.positive(x**3), Q.negative(x)) is False
+    assert satask(Q.negative(x**3), Q.negative(x)) is True
+    assert satask(Q.real(x**3), Q.negative(x)) is True
+
+    assert satask(Q.nonnegative(x**3), Q.nonnegative(x)) is True
+    assert satask(Q.nonpositive(x**3), Q.nonnegative(x)) is None
+    assert satask(Q.positive(x**3), Q.nonnegative(x)) is None
+    assert satask(Q.negative(x**3), Q.nonnegative(x)) is False
+    assert satask(Q.real(x**3), Q.nonnegative(x)) is True
+
+    assert satask(Q.nonnegative(x**3), Q.nonpositive(x)) is None
+    assert satask(Q.nonpositive(x**3), Q.nonpositive(x)) is True
+    assert satask(Q.positive(x**3), Q.nonpositive(x)) is False
+    assert satask(Q.negative(x**3), Q.nonpositive(x)) is None
+    assert satask(Q.real(x**3), Q.nonpositive(x)) is True
+
+    # If x is zero, x**negative is not real.
+    assert satask(Q.nonnegative(x**-2), Q.nonpositive(x)) is None
+    assert satask(Q.nonpositive(x**-2), Q.nonpositive(x)) is None
+    assert satask(Q.positive(x**-2), Q.nonpositive(x)) is None
+    assert satask(Q.negative(x**-2), Q.nonpositive(x)) is None
+    assert satask(Q.real(x**-2), Q.nonpositive(x)) is None
+
+    # We could deduce things for negative powers if x is nonzero, but it
+    # isn't implemented yet.
+
+
+def test_prime_composite():
+    assert satask(Q.prime(x), Q.composite(x)) is False
+    assert satask(Q.composite(x), Q.prime(x)) is False
+    assert satask(Q.composite(x), ~Q.prime(x)) is None
+    assert satask(Q.prime(x), ~Q.composite(x)) is None
+    # since 1 is neither prime nor composite the following should hold
+    assert satask(Q.prime(x), Q.integer(x) & Q.positive(x) & ~Q.composite(x)) is None
+    assert satask(Q.prime(2)) is True
+    assert satask(Q.prime(4)) is False
+    assert satask(Q.prime(1)) is False
+    assert satask(Q.composite(1)) is False
+
+
+def test_extract_predargs():
+    props = CNF.from_prop(Q.zero(Abs(x*y)) & Q.zero(x*y))
+    assump = CNF.from_prop(Q.zero(x))
+    context = CNF.from_prop(Q.zero(y))
+    assert extract_predargs(props) == {Abs(x*y), x*y}
+    assert extract_predargs(props, assump) == {Abs(x*y), x*y, x}
+    assert extract_predargs(props, assump, context) == {Abs(x*y), x*y, x, y}
+
+    props = CNF.from_prop(Eq(x, y))
+    assump = CNF.from_prop(Gt(y, z))
+    assert extract_predargs(props, assump) == {x, y, z}
+
+
+def test_get_relevant_clsfacts():
+    exprs = {Abs(x*y)}
+    exprs, facts = get_relevant_clsfacts(exprs)
+    assert exprs == {x*y}
+    assert facts.clauses == \
+        {frozenset({Literal(Q.odd(Abs(x*y)), False), Literal(Q.odd(x*y), True)}),
+        frozenset({Literal(Q.zero(Abs(x*y)), False), Literal(Q.zero(x*y), True)}),
+        frozenset({Literal(Q.even(Abs(x*y)), False), Literal(Q.even(x*y), True)}),
+        frozenset({Literal(Q.zero(Abs(x*y)), True), Literal(Q.zero(x*y), False)}),
+        frozenset({Literal(Q.even(Abs(x*y)), False),
+                    Literal(Q.odd(Abs(x*y)), False),
+                    Literal(Q.odd(x*y), True)}),
+        frozenset({Literal(Q.even(Abs(x*y)), False),
+                    Literal(Q.even(x*y), True),
+                    Literal(Q.odd(Abs(x*y)), False)}),
+        frozenset({Literal(Q.positive(Abs(x*y)), False),
+                    Literal(Q.zero(Abs(x*y)), False)})}

lib/python3.12/site-packages/sympy/assumptions/tests/test_sathandlers.py

@@ -0,0 +1,50 @@
+from sympy.assumptions.ask import Q
+from sympy.core.basic import Basic
+from sympy.core.expr import Expr
+from sympy.core.mul import Mul
+from sympy.core.symbol import symbols
+from sympy.logic.boolalg import (And, Or)
+
+from sympy.assumptions.sathandlers import (ClassFactRegistry, allargs,
+    anyarg, exactlyonearg,)
+
+x, y, z = symbols('x y z')
+
+
+def test_class_handler_registry():
+    my_handler_registry = ClassFactRegistry()
+
+    # The predicate doesn't matter here, so just pass
+    @my_handler_registry.register(Mul)
+    def fact1(expr):
+        pass
+    @my_handler_registry.multiregister(Expr)
+    def fact2(expr):
+        pass
+
+    assert my_handler_registry[Basic] == (frozenset(), frozenset())
+    assert my_handler_registry[Expr] == (frozenset(), frozenset({fact2}))
+    assert my_handler_registry[Mul] == (frozenset({fact1}), frozenset({fact2}))
+
+
+def test_allargs():
+    assert allargs(x, Q.zero(x), x*y) == And(Q.zero(x), Q.zero(y))
+    assert allargs(x, Q.positive(x) | Q.negative(x), x*y) == And(Q.positive(x) | Q.negative(x), Q.positive(y) | Q.negative(y))
+
+
+def test_anyarg():
+    assert anyarg(x, Q.zero(x), x*y) == Or(Q.zero(x), Q.zero(y))
+    assert anyarg(x, Q.positive(x) & Q.negative(x), x*y) == \
+        Or(Q.positive(x) & Q.negative(x), Q.positive(y) & Q.negative(y))
+
+
+def test_exactlyonearg():
+    assert exactlyonearg(x, Q.zero(x), x*y) == \
+        Or(Q.zero(x) & ~Q.zero(y), Q.zero(y) & ~Q.zero(x))
+    assert exactlyonearg(x, Q.zero(x), x*y*z) == \
+        Or(Q.zero(x) & ~Q.zero(y) & ~Q.zero(z), Q.zero(y)
+        & ~Q.zero(x) & ~Q.zero(z), Q.zero(z) & ~Q.zero(x) & ~Q.zero(y))
+    assert exactlyonearg(x, Q.positive(x) | Q.negative(x), x*y) == \
+        Or((Q.positive(x) | Q.negative(x)) &
+        ~(Q.positive(y) | Q.negative(y)), (Q.positive(y) | Q.negative(y)) &
+        ~(Q.positive(x) | Q.negative(x)))

lib/python3.12/site-packages/sympy/assumptions/tests/test_wrapper.py

@@ -0,0 +1,39 @@
+from sympy.assumptions.ask import Q
+from sympy.assumptions.wrapper import (AssumptionsWrapper, is_infinite,
+    is_extended_real)
+from sympy.core.symbol import Symbol
+from sympy.core.assumptions import _assume_defined
+
+
+def test_all_predicates():
+    for fact in _assume_defined:
+        method_name = f'_eval_is_{fact}'
+        assert hasattr(AssumptionsWrapper, method_name)
+
+
+def test_AssumptionsWrapper():
+    x = Symbol('x', positive=True)
+    y = Symbol('y')
+    assert AssumptionsWrapper(x).is_positive
+    assert AssumptionsWrapper(y).is_positive is None
+    assert AssumptionsWrapper(y, Q.positive(y)).is_positive
+
+
+def test_is_infinite():
+    x = Symbol('x', infinite=True)
+    y = Symbol('y', infinite=False)
+    z = Symbol('z')
+    assert is_infinite(x)
+    assert not is_infinite(y)
+    assert is_infinite(z) is None
+    assert is_infinite(z, Q.infinite(z))
+
+
+def test_is_extended_real():
+    x = Symbol('x', extended_real=True)
+    y = Symbol('y', extended_real=False)
+    z = Symbol('z')
+    assert is_extended_real(x)
+    assert not is_extended_real(y)
+    assert is_extended_real(z) is None
+    assert is_extended_real(z, Q.extended_real(z))

lib/python3.12/site-packages/sympy/assumptions/wrapper.py

@@ -0,0 +1,164 @@
+"""
+Functions and wrapper object to call assumption property and predicate
+query with same syntax.
+
+In SymPy, there are two assumption systems. Old assumption system is
+defined in sympy/core/assumptions, and it can be accessed by attribute
+such as ``x.is_even``. New assumption system is defined in
+sympy/assumptions, and it can be accessed by predicates such as
+``Q.even(x)``.
+
+Old assumption is fast, while new assumptions can freely take local facts.
+In general, old assumption is used in evaluation method and new assumption
+is used in refinement method.
+
+In most cases, both evaluation and refinement follow the same process, and
+the only difference is which assumption system is used. This module provides
+``is_[...]()`` functions and ``AssumptionsWrapper()`` class which allows
+using two systems with same syntax so that parallel code implementation can be
+avoided.
+
+Examples
+========
+
+For multiple use, use ``AssumptionsWrapper()``.
+
+>>> from sympy import Q, Symbol
+>>> from sympy.assumptions.wrapper import AssumptionsWrapper
+>>> x = Symbol('x')
+>>> _x = AssumptionsWrapper(x, Q.even(x))
+>>> _x.is_integer
+True
+>>> _x.is_odd
+False
+
+For single use, use ``is_[...]()`` functions.
+
+>>> from sympy.assumptions.wrapper import is_infinite
+>>> a = Symbol('a')
+>>> print(is_infinite(a))
+None
+>>> is_infinite(a, Q.finite(a))
+False
+
+"""
+
+from sympy.assumptions import ask, Q
+from sympy.core.basic import Basic
+from sympy.core.sympify import _sympify
+
+
+def make_eval_method(fact):
+    def getit(self):
+        pred = getattr(Q, fact)
+        ret = ask(pred(self.expr), self.assumptions)
+        return ret
+    return getit
+
+
+# we subclass Basic to use the fact deduction and caching
+class AssumptionsWrapper(Basic):
+    """
+    Wrapper over ``Basic`` instances to call predicate query by
+    ``.is_[...]`` property
+
+    Parameters
+    ==========
+
+    expr : Basic
+
+    assumptions : Boolean, optional
+
+    Examples
+    ========
+
+    >>> from sympy import Q, Symbol
+    >>> from sympy.assumptions.wrapper import AssumptionsWrapper
+    >>> x = Symbol('x', even=True)
+    >>> AssumptionsWrapper(x).is_integer
+    True
+    >>> y = Symbol('y')
+    >>> AssumptionsWrapper(y, Q.even(y)).is_integer
+    True
+
+    With ``AssumptionsWrapper``, both evaluation and refinement can be supported
+    by single implementation.
+
+    >>> from sympy import Function
+    >>> class MyAbs(Function):
+    ...     @classmethod
+    ...     def eval(cls, x, assumptions=True):
+    ...         _x = AssumptionsWrapper(x, assumptions)
+    ...         if _x.is_nonnegative:
+    ...             return x
+    ...         if _x.is_negative:
+    ...             return -x
+    ...     def _eval_refine(self, assumptions):
+    ...         return MyAbs.eval(self.args[0], assumptions)
+    >>> MyAbs(x)
+    MyAbs(x)
+    >>> MyAbs(x).refine(Q.positive(x))
+    x
+    >>> MyAbs(Symbol('y', negative=True))
+    -y
+
+    """
+    def __new__(cls, expr, assumptions=None):
+        if assumptions is None:
+            return expr
+        obj = super().__new__(cls, expr, _sympify(assumptions))
+        obj.expr = expr
+        obj.assumptions = assumptions
+        return obj
+
+    _eval_is_algebraic = make_eval_method("algebraic")
+    _eval_is_antihermitian = make_eval_method("antihermitian")
+    _eval_is_commutative = make_eval_method("commutative")
+    _eval_is_complex = make_eval_method("complex")
+    _eval_is_composite = make_eval_method("composite")
+    _eval_is_even = make_eval_method("even")
+    _eval_is_extended_negative = make_eval_method("extended_negative")
+    _eval_is_extended_nonnegative = make_eval_method("extended_nonnegative")
+    _eval_is_extended_nonpositive = make_eval_method("extended_nonpositive")
+    _eval_is_extended_nonzero = make_eval_method("extended_nonzero")
+    _eval_is_extended_positive = make_eval_method("extended_positive")
+    _eval_is_extended_real = make_eval_method("extended_real")
+    _eval_is_finite = make_eval_method("finite")
+    _eval_is_hermitian = make_eval_method("hermitian")
+    _eval_is_imaginary = make_eval_method("imaginary")
+    _eval_is_infinite = make_eval_method("infinite")
+    _eval_is_integer = make_eval_method("integer")
+    _eval_is_irrational = make_eval_method("irrational")
+    _eval_is_negative = make_eval_method("negative")
+    _eval_is_noninteger = make_eval_method("noninteger")
+    _eval_is_nonnegative = make_eval_method("nonnegative")
+    _eval_is_nonpositive = make_eval_method("nonpositive")
+    _eval_is_nonzero = make_eval_method("nonzero")
+    _eval_is_odd = make_eval_method("odd")
+    _eval_is_polar = make_eval_method("polar")
+    _eval_is_positive = make_eval_method("positive")
+    _eval_is_prime = make_eval_method("prime")
+    _eval_is_rational = make_eval_method("rational")
+    _eval_is_real = make_eval_method("real")
+    _eval_is_transcendental = make_eval_method("transcendental")
+    _eval_is_zero = make_eval_method("zero")
+
+
+# one shot functions which are faster than AssumptionsWrapper
+
+def is_infinite(obj, assumptions=None):
+    if assumptions is None:
+        return obj.is_infinite
+    return ask(Q.infinite(obj), assumptions)
+
+
+def is_extended_real(obj, assumptions=None):
+    if assumptions is None:
+        return obj.is_extended_real
+    return ask(Q.extended_real(obj), assumptions)
+
+
+def is_extended_nonnegative(obj, assumptions=None):
+    if assumptions is None:
+        return obj.is_extended_nonnegative
+    return ask(Q.extended_nonnegative(obj), assumptions)