Add files using upload-large-folder tool

lib/python3.10/site-packages/sympy/algebras/__init__.py

@@ -0,0 +1,3 @@
+from .quaternion import Quaternion
+
+__all__ = ["Quaternion",]

lib/python3.10/site-packages/sympy/algebras/quaternion.py

@@ -0,0 +1,1667 @@
+from sympy.core.numbers import Rational
+from sympy.core.singleton import S
+from sympy.core.relational import is_eq
+from sympy.functions.elementary.complexes import (conjugate, im, re, sign)
+from sympy.functions.elementary.exponential import (exp, log as ln)
+from sympy.functions.elementary.miscellaneous import sqrt
+from sympy.functions.elementary.trigonometric import (acos, asin, atan2)
+from sympy.functions.elementary.trigonometric import (cos, sin)
+from sympy.simplify.trigsimp import trigsimp
+from sympy.integrals.integrals import integrate
+from sympy.matrices.dense import MutableDenseMatrix as Matrix
+from sympy.core.sympify import sympify, _sympify
+from sympy.core.expr import Expr
+from sympy.core.logic import fuzzy_not, fuzzy_or
+from sympy.utilities.misc import as_int
+
+from mpmath.libmp.libmpf import prec_to_dps
+
+
+def _check_norm(elements, norm):
+    """validate if input norm is consistent"""
+    if norm is not None and norm.is_number:
+        if norm.is_positive is False:
+            raise ValueError("Input norm must be positive.")
+
+        numerical = all(i.is_number and i.is_real is True for i in elements)
+        if numerical and is_eq(norm**2, sum(i**2 for i in elements)) is False:
+            raise ValueError("Incompatible value for norm.")
+
+
+def _is_extrinsic(seq):
+    """validate seq and return True if seq is lowercase and False if uppercase"""
+    if type(seq) != str:
+        raise ValueError('Expected seq to be a string.')
+    if len(seq) != 3:
+        raise ValueError("Expected 3 axes, got `{}`.".format(seq))
+
+    intrinsic = seq.isupper()
+    extrinsic = seq.islower()
+    if not (intrinsic or extrinsic):
+        raise ValueError("seq must either be fully uppercase (for extrinsic "
+                         "rotations), or fully lowercase, for intrinsic "
+                         "rotations).")
+
+    i, j, k = seq.lower()
+    if (i == j) or (j == k):
+        raise ValueError("Consecutive axes must be different")
+
+    bad = set(seq) - set('xyzXYZ')
+    if bad:
+        raise ValueError("Expected axes from `seq` to be from "
+                         "['x', 'y', 'z'] or ['X', 'Y', 'Z'], "
+                         "got {}".format(''.join(bad)))
+
+    return extrinsic
+
+
+class Quaternion(Expr):
+    """Provides basic quaternion operations.
+    Quaternion objects can be instantiated as ``Quaternion(a, b, c, d)``
+    as in $q = a + bi + cj + dk$.
+
+    Parameters
+    ==========
+
+    norm : None or number
+        Pre-defined quaternion norm. If a value is given, Quaternion.norm
+        returns this pre-defined value instead of calculating the norm
+
+    Examples
+    ========
+
+    >>> from sympy import Quaternion
+    >>> q = Quaternion(1, 2, 3, 4)
+    >>> q
+    1 + 2*i + 3*j + 4*k
+
+    Quaternions over complex fields can be defined as:
+
+    >>> from sympy import Quaternion
+    >>> from sympy import symbols, I
+    >>> x = symbols('x')
+    >>> q1 = Quaternion(x, x**3, x, x**2, real_field = False)
+    >>> q2 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+    >>> q1
+    x + x**3*i + x*j + x**2*k
+    >>> q2
+    (3 + 4*I) + (2 + 5*I)*i + 0*j + (7 + 8*I)*k
+
+    Defining symbolic unit quaternions:
+
+    >>> from sympy import Quaternion
+    >>> from sympy.abc import w, x, y, z
+    >>> q = Quaternion(w, x, y, z, norm=1)
+    >>> q
+    w + x*i + y*j + z*k
+    >>> q.norm()
+    1
+
+    References
+    ==========
+
+    .. [1] https://www.euclideanspace.com/maths/algebra/realNormedAlgebra/quaternions/
+    .. [2] https://en.wikipedia.org/wiki/Quaternion
+
+    """
+    _op_priority = 11.0
+
+    is_commutative = False
+
+    def __new__(cls, a=0, b=0, c=0, d=0, real_field=True, norm=None):
+        a, b, c, d = map(sympify, (a, b, c, d))
+
+        if any(i.is_commutative is False for i in [a, b, c, d]):
+            raise ValueError("arguments have to be commutative")
+        obj = super().__new__(cls, a, b, c, d)
+        obj._real_field = real_field
+        obj.set_norm(norm)
+        return obj
+
+    def set_norm(self, norm):
+        """Sets norm of an already instantiated quaternion.
+
+        Parameters
+        ==========
+
+        norm : None or number
+            Pre-defined quaternion norm. If a value is given, Quaternion.norm
+            returns this pre-defined value instead of calculating the norm
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> q = Quaternion(a, b, c, d)
+        >>> q.norm()
+        sqrt(a**2 + b**2 + c**2 + d**2)
+
+        Setting the norm:
+
+        >>> q.set_norm(1)
+        >>> q.norm()
+        1
+
+        Removing set norm:
+
+        >>> q.set_norm(None)
+        >>> q.norm()
+        sqrt(a**2 + b**2 + c**2 + d**2)
+
+        """
+        norm = sympify(norm)
+        _check_norm(self.args, norm)
+        self._norm = norm
+
+    @property
+    def a(self):
+        return self.args[0]
+
+    @property
+    def b(self):
+        return self.args[1]
+
+    @property
+    def c(self):
+        return self.args[2]
+
+    @property
+    def d(self):
+        return self.args[3]
+
+    @property
+    def real_field(self):
+        return self._real_field
+
+    @property
+    def product_matrix_left(self):
+        r"""Returns 4 x 4 Matrix equivalent to a Hamilton product from the
+        left. This can be useful when treating quaternion elements as column
+        vectors. Given a quaternion $q = a + bi + cj + dk$ where a, b, c and d
+        are real numbers, the product matrix from the left is:
+
+        .. math::
+
+            M  =  \begin{bmatrix} a  &-b  &-c  &-d \\
+                                  b  & a  &-d  & c \\
+                                  c  & d  & a  &-b \\
+                                  d  &-c  & b  & a \end{bmatrix}
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> q1 = Quaternion(1, 0, 0, 1)
+        >>> q2 = Quaternion(a, b, c, d)
+        >>> q1.product_matrix_left
+        Matrix([
+        [1, 0,  0, -1],
+        [0, 1, -1,  0],
+        [0, 1,  1,  0],
+        [1, 0,  0,  1]])
+
+        >>> q1.product_matrix_left * q2.to_Matrix()
+        Matrix([
+        [a - d],
+        [b - c],
+        [b + c],
+        [a + d]])
+
+        This is equivalent to:
+
+        >>> (q1 * q2).to_Matrix()
+        Matrix([
+        [a - d],
+        [b - c],
+        [b + c],
+        [a + d]])
+        """
+        return Matrix([
+                [self.a, -self.b, -self.c, -self.d],
+                [self.b, self.a, -self.d, self.c],
+                [self.c, self.d, self.a, -self.b],
+                [self.d, -self.c, self.b, self.a]])
+
+    @property
+    def product_matrix_right(self):
+        r"""Returns 4 x 4 Matrix equivalent to a Hamilton product from the
+        right. This can be useful when treating quaternion elements as column
+        vectors. Given a quaternion $q = a + bi + cj + dk$ where a, b, c and d
+        are real numbers, the product matrix from the left is:
+
+        .. math::
+
+            M  =  \begin{bmatrix} a  &-b  &-c  &-d \\
+                                  b  & a  & d  &-c \\
+                                  c  &-d  & a  & b \\
+                                  d  & c  &-b  & a \end{bmatrix}
+
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> q1 = Quaternion(a, b, c, d)
+        >>> q2 = Quaternion(1, 0, 0, 1)
+        >>> q2.product_matrix_right
+        Matrix([
+        [1, 0, 0, -1],
+        [0, 1, 1, 0],
+        [0, -1, 1, 0],
+        [1, 0, 0, 1]])
+
+        Note the switched arguments: the matrix represents the quaternion on
+        the right, but is still considered as a matrix multiplication from the
+        left.
+
+        >>> q2.product_matrix_right * q1.to_Matrix()
+        Matrix([
+        [ a - d],
+        [ b + c],
+        [-b + c],
+        [ a + d]])
+
+        This is equivalent to:
+
+        >>> (q1 * q2).to_Matrix()
+        Matrix([
+        [ a - d],
+        [ b + c],
+        [-b + c],
+        [ a + d]])
+        """
+        return Matrix([
+                [self.a, -self.b, -self.c, -self.d],
+                [self.b, self.a, self.d, -self.c],
+                [self.c, -self.d, self.a, self.b],
+                [self.d, self.c, -self.b, self.a]])
+
+    def to_Matrix(self, vector_only=False):
+        """Returns elements of quaternion as a column vector.
+        By default, a ``Matrix`` of length 4 is returned, with the real part as the
+        first element.
+        If ``vector_only`` is ``True``, returns only imaginary part as a Matrix of
+        length 3.
+
+        Parameters
+        ==========
+
+        vector_only : bool
+            If True, only imaginary part is returned.
+            Default value: False
+
+        Returns
+        =======
+
+        Matrix
+            A column vector constructed by the elements of the quaternion.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> q = Quaternion(a, b, c, d)
+        >>> q
+        a + b*i + c*j + d*k
+
+        >>> q.to_Matrix()
+        Matrix([
+        [a],
+        [b],
+        [c],
+        [d]])
+
+
+        >>> q.to_Matrix(vector_only=True)
+        Matrix([
+        [b],
+        [c],
+        [d]])
+
+        """
+        if vector_only:
+            return Matrix(self.args[1:])
+        else:
+            return Matrix(self.args)
+
+    @classmethod
+    def from_Matrix(cls, elements):
+        """Returns quaternion from elements of a column vector`.
+        If vector_only is True, returns only imaginary part as a Matrix of
+        length 3.
+
+        Parameters
+        ==========
+
+        elements : Matrix, list or tuple of length 3 or 4. If length is 3,
+            assume real part is zero.
+            Default value: False
+
+        Returns
+        =======
+
+        Quaternion
+            A quaternion created from the input elements.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> q = Quaternion.from_Matrix([a, b, c, d])
+        >>> q
+        a + b*i + c*j + d*k
+
+        >>> q = Quaternion.from_Matrix([b, c, d])
+        >>> q
+        0 + b*i + c*j + d*k
+
+        """
+        length = len(elements)
+        if length != 3 and length != 4:
+            raise ValueError("Input elements must have length 3 or 4, got {} "
+                             "elements".format(length))
+
+        if length == 3:
+            return Quaternion(0, *elements)
+        else:
+            return Quaternion(*elements)
+
+    @classmethod
+    def from_euler(cls, angles, seq):
+        """Returns quaternion equivalent to rotation represented by the Euler
+        angles, in the sequence defined by ``seq``.
+
+        Parameters
+        ==========
+
+        angles : list, tuple or Matrix of 3 numbers
+            The Euler angles (in radians).
+        seq : string of length 3
+            Represents the sequence of rotations.
+            For extrinsic rotations, seq must be all lowercase and its elements
+            must be from the set ``{'x', 'y', 'z'}``
+            For intrinsic rotations, seq must be all uppercase and its elements
+            must be from the set ``{'X', 'Y', 'Z'}``
+
+        Returns
+        =======
+
+        Quaternion
+            The normalized rotation quaternion calculated from the Euler angles
+            in the given sequence.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import pi
+        >>> q = Quaternion.from_euler([pi/2, 0, 0], 'xyz')
+        >>> q
+        sqrt(2)/2 + sqrt(2)/2*i + 0*j + 0*k
+
+        >>> q = Quaternion.from_euler([0, pi/2, pi] , 'zyz')
+        >>> q
+        0 + (-sqrt(2)/2)*i + 0*j + sqrt(2)/2*k
+
+        >>> q = Quaternion.from_euler([0, pi/2, pi] , 'ZYZ')
+        >>> q
+        0 + sqrt(2)/2*i + 0*j + sqrt(2)/2*k
+
+        """
+
+        if len(angles) != 3:
+            raise ValueError("3 angles must be given.")
+
+        extrinsic = _is_extrinsic(seq)
+        i, j, k = seq.lower()
+
+        # get elementary basis vectors
+        ei = [1 if n == i else 0 for n in 'xyz']
+        ej = [1 if n == j else 0 for n in 'xyz']
+        ek = [1 if n == k else 0 for n in 'xyz']
+
+        # calculate distinct quaternions
+        qi = cls.from_axis_angle(ei, angles[0])
+        qj = cls.from_axis_angle(ej, angles[1])
+        qk = cls.from_axis_angle(ek, angles[2])
+
+        if extrinsic:
+            return trigsimp(qk * qj * qi)
+        else:
+            return trigsimp(qi * qj * qk)
+
+    def to_euler(self, seq, angle_addition=True, avoid_square_root=False):
+        r"""Returns Euler angles representing same rotation as the quaternion,
+        in the sequence given by ``seq``. This implements the method described
+        in [1]_.
+
+        For degenerate cases (gymbal lock cases), the third angle is
+        set to zero.
+
+        Parameters
+        ==========
+
+        seq : string of length 3
+            Represents the sequence of rotations.
+            For extrinsic rotations, seq must be all lowercase and its elements
+            must be from the set ``{'x', 'y', 'z'}``
+            For intrinsic rotations, seq must be all uppercase and its elements
+            must be from the set ``{'X', 'Y', 'Z'}``
+
+        angle_addition : bool
+            When True, first and third angles are given as an addition and
+            subtraction of two simpler ``atan2`` expressions. When False, the
+            first and third angles are each given by a single more complicated
+            ``atan2`` expression. This equivalent expression is given by:
+
+            .. math::
+
+                \operatorname{atan_2} (b,a) \pm \operatorname{atan_2} (d,c) =
+                \operatorname{atan_2} (bc\pm ad, ac\mp bd)
+
+            Default value: True
+
+        avoid_square_root : bool
+            When True, the second angle is calculated with an expression based
+            on ``acos``, which is slightly more complicated but avoids a square
+            root. When False, second angle is calculated with ``atan2``, which
+            is simpler and can be better for numerical reasons (some
+            numerical implementations of ``acos`` have problems near zero).
+            Default value: False
+
+
+        Returns
+        =======
+
+        Tuple
+            The Euler angles calculated from the quaternion
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import a, b, c, d
+        >>> euler = Quaternion(a, b, c, d).to_euler('zyz')
+        >>> euler
+        (-atan2(-b, c) + atan2(d, a),
+         2*atan2(sqrt(b**2 + c**2), sqrt(a**2 + d**2)),
+         atan2(-b, c) + atan2(d, a))
+
+
+        References
+        ==========
+
+        .. [1] https://doi.org/10.1371/journal.pone.0276302
+
+        """
+        if self.is_zero_quaternion():
+            raise ValueError('Cannot convert a quaternion with norm 0.')
+
+        angles = [0, 0, 0]
+
+        extrinsic = _is_extrinsic(seq)
+        i, j, k = seq.lower()
+
+        # get index corresponding to elementary basis vectors
+        i = 'xyz'.index(i) + 1
+        j = 'xyz'.index(j) + 1
+        k = 'xyz'.index(k) + 1
+
+        if not extrinsic:
+            i, k = k, i
+
+        # check if sequence is symmetric
+        symmetric = i == k
+        if symmetric:
+            k = 6 - i - j
+
+        # parity of the permutation
+        sign = (i - j) * (j - k) * (k - i) // 2
+
+        # permutate elements
+        elements = [self.a, self.b, self.c, self.d]
+        a = elements[0]
+        b = elements[i]
+        c = elements[j]
+        d = elements[k] * sign
+
+        if not symmetric:
+            a, b, c, d = a - c, b + d, c + a, d - b
+
+        if avoid_square_root:
+            if symmetric:
+                n2 = self.norm()**2
+                angles[1] = acos((a * a + b * b - c * c - d * d) / n2)
+            else:
+                n2 = 2 * self.norm()**2
+                angles[1] = asin((c * c + d * d - a * a - b * b) / n2)
+        else:
+            angles[1] = 2 * atan2(sqrt(c * c + d * d), sqrt(a * a + b * b))
+            if not symmetric:
+                angles[1] -= S.Pi / 2
+
+        # Check for singularities in numerical cases
+        case = 0
+        if is_eq(c, S.Zero) and is_eq(d, S.Zero):
+            case = 1
+        if is_eq(a, S.Zero) and is_eq(b, S.Zero):
+            case = 2
+
+        if case == 0:
+            if angle_addition:
+                angles[0] = atan2(b, a) + atan2(d, c)
+                angles[2] = atan2(b, a) - atan2(d, c)
+            else:
+                angles[0] = atan2(b*c + a*d, a*c - b*d)
+                angles[2] = atan2(b*c - a*d, a*c + b*d)
+
+        else:  # any degenerate case
+            angles[2 * (not extrinsic)] = S.Zero
+            if case == 1:
+                angles[2 * extrinsic] = 2 * atan2(b, a)
+            else:
+                angles[2 * extrinsic] = 2 * atan2(d, c)
+                angles[2 * extrinsic] *= (-1 if extrinsic else 1)
+
+        # for Tait-Bryan angles
+        if not symmetric:
+            angles[0] *= sign
+
+        if extrinsic:
+            return tuple(angles[::-1])
+        else:
+            return tuple(angles)
+
+    @classmethod
+    def from_axis_angle(cls, vector, angle):
+        """Returns a rotation quaternion given the axis and the angle of rotation.
+
+        Parameters
+        ==========
+
+        vector : tuple of three numbers
+            The vector representation of the given axis.
+        angle : number
+            The angle by which axis is rotated (in radians).
+
+        Returns
+        =======
+
+        Quaternion
+            The normalized rotation quaternion calculated from the given axis and the angle of rotation.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import pi, sqrt
+        >>> q = Quaternion.from_axis_angle((sqrt(3)/3, sqrt(3)/3, sqrt(3)/3), 2*pi/3)
+        >>> q
+        1/2 + 1/2*i + 1/2*j + 1/2*k
+
+        """
+        (x, y, z) = vector
+        norm = sqrt(x**2 + y**2 + z**2)
+        (x, y, z) = (x / norm, y / norm, z / norm)
+        s = sin(angle * S.Half)
+        a = cos(angle * S.Half)
+        b = x * s
+        c = y * s
+        d = z * s
+
+        # note that this quaternion is already normalized by construction:
+        # c^2 + (s*x)^2 + (s*y)^2 + (s*z)^2 = c^2 + s^2*(x^2 + y^2 + z^2) = c^2 + s^2 * 1 = c^2 + s^2 = 1
+        # so, what we return is a normalized quaternion
+
+        return cls(a, b, c, d)
+
+    @classmethod
+    def from_rotation_matrix(cls, M):
+        """Returns the equivalent quaternion of a matrix. The quaternion will be normalized
+        only if the matrix is special orthogonal (orthogonal and det(M) = 1).
+
+        Parameters
+        ==========
+
+        M : Matrix
+            Input matrix to be converted to equivalent quaternion. M must be special
+            orthogonal (orthogonal and det(M) = 1) for the quaternion to be normalized.
+
+        Returns
+        =======
+
+        Quaternion
+            The quaternion equivalent to given matrix.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import Matrix, symbols, cos, sin, trigsimp
+        >>> x = symbols('x')
+        >>> M = Matrix([[cos(x), -sin(x), 0], [sin(x), cos(x), 0], [0, 0, 1]])
+        >>> q = trigsimp(Quaternion.from_rotation_matrix(M))
+        >>> q
+        sqrt(2)*sqrt(cos(x) + 1)/2 + 0*i + 0*j + sqrt(2 - 2*cos(x))*sign(sin(x))/2*k
+
+        """
+
+        absQ = M.det()**Rational(1, 3)
+
+        a = sqrt(absQ + M[0, 0] + M[1, 1] + M[2, 2]) / 2
+        b = sqrt(absQ + M[0, 0] - M[1, 1] - M[2, 2]) / 2
+        c = sqrt(absQ - M[0, 0] + M[1, 1] - M[2, 2]) / 2
+        d = sqrt(absQ - M[0, 0] - M[1, 1] + M[2, 2]) / 2
+
+        b = b * sign(M[2, 1] - M[1, 2])
+        c = c * sign(M[0, 2] - M[2, 0])
+        d = d * sign(M[1, 0] - M[0, 1])
+
+        return Quaternion(a, b, c, d)
+
+    def __add__(self, other):
+        return self.add(other)
+
+    def __radd__(self, other):
+        return self.add(other)
+
+    def __sub__(self, other):
+        return self.add(other*-1)
+
+    def __mul__(self, other):
+        return self._generic_mul(self, _sympify(other))
+
+    def __rmul__(self, other):
+        return self._generic_mul(_sympify(other), self)
+
+    def __pow__(self, p):
+        return self.pow(p)
+
+    def __neg__(self):
+        return Quaternion(-self.a, -self.b, -self.c, -self.d)
+
+    def __truediv__(self, other):
+        return self * sympify(other)**-1
+
+    def __rtruediv__(self, other):
+        return sympify(other) * self**-1
+
+    def _eval_Integral(self, *args):
+        return self.integrate(*args)
+
+    def diff(self, *symbols, **kwargs):
+        kwargs.setdefault('evaluate', True)
+        return self.func(*[a.diff(*symbols, **kwargs) for a  in self.args])
+
+    def add(self, other):
+        """Adds quaternions.
+
+        Parameters
+        ==========
+
+        other : Quaternion
+            The quaternion to add to current (self) quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            The resultant quaternion after adding self to other
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import symbols
+        >>> q1 = Quaternion(1, 2, 3, 4)
+        >>> q2 = Quaternion(5, 6, 7, 8)
+        >>> q1.add(q2)
+        6 + 8*i + 10*j + 12*k
+        >>> q1 + 5
+        6 + 2*i + 3*j + 4*k
+        >>> x = symbols('x', real = True)
+        >>> q1.add(x)
+        (x + 1) + 2*i + 3*j + 4*k
+
+        Quaternions over complex fields :
+
+        >>> from sympy import Quaternion
+        >>> from sympy import I
+        >>> q3 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+        >>> q3.add(2 + 3*I)
+        (5 + 7*I) + (2 + 5*I)*i + 0*j + (7 + 8*I)*k
+
+        """
+        q1 = self
+        q2 = sympify(other)
+
+        # If q2 is a number or a SymPy expression instead of a quaternion
+        if not isinstance(q2, Quaternion):
+            if q1.real_field and q2.is_complex:
+                return Quaternion(re(q2) + q1.a, im(q2) + q1.b, q1.c, q1.d)
+            elif q2.is_commutative:
+                return Quaternion(q1.a + q2, q1.b, q1.c, q1.d)
+            else:
+                raise ValueError("Only commutative expressions can be added with a Quaternion.")
+
+        return Quaternion(q1.a + q2.a, q1.b + q2.b, q1.c + q2.c, q1.d
+                          + q2.d)
+
+    def mul(self, other):
+        """Multiplies quaternions.
+
+        Parameters
+        ==========
+
+        other : Quaternion or symbol
+            The quaternion to multiply to current (self) quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            The resultant quaternion after multiplying self with other
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import symbols
+        >>> q1 = Quaternion(1, 2, 3, 4)
+        >>> q2 = Quaternion(5, 6, 7, 8)
+        >>> q1.mul(q2)
+        (-60) + 12*i + 30*j + 24*k
+        >>> q1.mul(2)
+        2 + 4*i + 6*j + 8*k
+        >>> x = symbols('x', real = True)
+        >>> q1.mul(x)
+        x + 2*x*i + 3*x*j + 4*x*k
+
+        Quaternions over complex fields :
+
+        >>> from sympy import Quaternion
+        >>> from sympy import I
+        >>> q3 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+        >>> q3.mul(2 + 3*I)
+        (2 + 3*I)*(3 + 4*I) + (2 + 3*I)*(2 + 5*I)*i + 0*j + (2 + 3*I)*(7 + 8*I)*k
+
+        """
+        return self._generic_mul(self, _sympify(other))
+
+    @staticmethod
+    def _generic_mul(q1, q2):
+        """Generic multiplication.
+
+        Parameters
+        ==========
+
+        q1 : Quaternion or symbol
+        q2 : Quaternion or symbol
+
+        It is important to note that if neither q1 nor q2 is a Quaternion,
+        this function simply returns q1 * q2.
+
+        Returns
+        =======
+
+        Quaternion
+            The resultant quaternion after multiplying q1 and q2
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import Symbol, S
+        >>> q1 = Quaternion(1, 2, 3, 4)
+        >>> q2 = Quaternion(5, 6, 7, 8)
+        >>> Quaternion._generic_mul(q1, q2)
+        (-60) + 12*i + 30*j + 24*k
+        >>> Quaternion._generic_mul(q1, S(2))
+        2 + 4*i + 6*j + 8*k
+        >>> x = Symbol('x', real = True)
+        >>> Quaternion._generic_mul(q1, x)
+        x + 2*x*i + 3*x*j + 4*x*k
+
+        Quaternions over complex fields :
+
+        >>> from sympy import I
+        >>> q3 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+        >>> Quaternion._generic_mul(q3, 2 + 3*I)
+        (2 + 3*I)*(3 + 4*I) + (2 + 3*I)*(2 + 5*I)*i + 0*j + (2 + 3*I)*(7 + 8*I)*k
+
+        """
+        # None is a Quaternion:
+        if not isinstance(q1, Quaternion) and not isinstance(q2, Quaternion):
+            return q1 * q2
+
+        # If q1 is a number or a SymPy expression instead of a quaternion
+        if not isinstance(q1, Quaternion):
+            if q2.real_field and q1.is_complex:
+                return Quaternion(re(q1), im(q1), 0, 0) * q2
+            elif q1.is_commutative:
+                return Quaternion(q1 * q2.a, q1 * q2.b, q1 * q2.c, q1 * q2.d)
+            else:
+                raise ValueError("Only commutative expressions can be multiplied with a Quaternion.")
+
+        # If q2 is a number or a SymPy expression instead of a quaternion
+        if not isinstance(q2, Quaternion):
+            if q1.real_field and q2.is_complex:
+                return q1 * Quaternion(re(q2), im(q2), 0, 0)
+            elif q2.is_commutative:
+                return Quaternion(q2 * q1.a, q2 * q1.b, q2 * q1.c, q2 * q1.d)
+            else:
+                raise ValueError("Only commutative expressions can be multiplied with a Quaternion.")
+
+        # If any of the quaternions has a fixed norm, pre-compute norm
+        if q1._norm is None and q2._norm is None:
+            norm = None
+        else:
+            norm = q1.norm() * q2.norm()
+
+        return Quaternion(-q1.b*q2.b - q1.c*q2.c - q1.d*q2.d + q1.a*q2.a,
+                          q1.b*q2.a + q1.c*q2.d - q1.d*q2.c + q1.a*q2.b,
+                          -q1.b*q2.d + q1.c*q2.a + q1.d*q2.b + q1.a*q2.c,
+                          q1.b*q2.c - q1.c*q2.b + q1.d*q2.a + q1.a * q2.d,
+                          norm=norm)
+
+    def _eval_conjugate(self):
+        """Returns the conjugate of the quaternion."""
+        q = self
+        return Quaternion(q.a, -q.b, -q.c, -q.d, norm=q._norm)
+
+    def norm(self):
+        """Returns the norm of the quaternion."""
+        if self._norm is None:  # check if norm is pre-defined
+            q = self
+            # trigsimp is used to simplify sin(x)^2 + cos(x)^2 (these terms
+            # arise when from_axis_angle is used).
+            return sqrt(trigsimp(q.a**2 + q.b**2 + q.c**2 + q.d**2))
+
+        return self._norm
+
+    def normalize(self):
+        """Returns the normalized form of the quaternion."""
+        q = self
+        return q * (1/q.norm())
+
+    def inverse(self):
+        """Returns the inverse of the quaternion."""
+        q = self
+        if not q.norm():
+            raise ValueError("Cannot compute inverse for a quaternion with zero norm")
+        return conjugate(q) * (1/q.norm()**2)
+
+    def pow(self, p):
+        """Finds the pth power of the quaternion.
+
+        Parameters
+        ==========
+
+        p : int
+            Power to be applied on quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            Returns the p-th power of the current quaternion.
+            Returns the inverse if p = -1.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.pow(4)
+        668 + (-224)*i + (-336)*j + (-448)*k
+
+        """
+        try:
+            q, p = self, as_int(p)
+        except ValueError:
+            return NotImplemented
+
+        if p < 0:
+            q, p = q.inverse(), -p
+
+        if p == 1:
+            return q
+
+        res = Quaternion(1, 0, 0, 0)
+        while p > 0:
+            if p & 1:
+                res *= q
+            q *= q
+            p >>= 1
+
+        return res
+
+    def exp(self):
+        """Returns the exponential of $q$, given by $e^q$.
+
+        Returns
+        =======
+
+        Quaternion
+            The exponential of the quaternion.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.exp()
+        E*cos(sqrt(29))
+        + 2*sqrt(29)*E*sin(sqrt(29))/29*i
+        + 3*sqrt(29)*E*sin(sqrt(29))/29*j
+        + 4*sqrt(29)*E*sin(sqrt(29))/29*k
+
+        """
+        # exp(q) = e^a(cos||v|| + v/||v||*sin||v||)
+        q = self
+        vector_norm = sqrt(q.b**2 + q.c**2 + q.d**2)
+        a = exp(q.a) * cos(vector_norm)
+        b = exp(q.a) * sin(vector_norm) * q.b / vector_norm
+        c = exp(q.a) * sin(vector_norm) * q.c / vector_norm
+        d = exp(q.a) * sin(vector_norm) * q.d / vector_norm
+
+        return Quaternion(a, b, c, d)
+
+    def log(self):
+        r"""Returns the logarithm of the quaternion, given by $\log q$.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.log()
+        log(sqrt(30))
+        + 2*sqrt(29)*acos(sqrt(30)/30)/29*i
+        + 3*sqrt(29)*acos(sqrt(30)/30)/29*j
+        + 4*sqrt(29)*acos(sqrt(30)/30)/29*k
+
+        """
+        # log(q) = log||q|| + v/||v||*arccos(a/||q||)
+        q = self
+        vector_norm = sqrt(q.b**2 + q.c**2 + q.d**2)
+        q_norm = q.norm()
+        a = ln(q_norm)
+        b = q.b * acos(q.a / q_norm) / vector_norm
+        c = q.c * acos(q.a / q_norm) / vector_norm
+        d = q.d * acos(q.a / q_norm) / vector_norm
+
+        return Quaternion(a, b, c, d)
+
+    def _eval_subs(self, *args):
+        elements = [i.subs(*args) for i in self.args]
+        norm = self._norm
+        if norm is not None:
+            norm = norm.subs(*args)
+        _check_norm(elements, norm)
+        return Quaternion(*elements, norm=norm)
+
+    def _eval_evalf(self, prec):
+        """Returns the floating point approximations (decimal numbers) of the quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            Floating point approximations of quaternion(self)
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import sqrt
+        >>> q = Quaternion(1/sqrt(1), 1/sqrt(2), 1/sqrt(3), 1/sqrt(4))
+        >>> q.evalf()
+        1.00000000000000
+        + 0.707106781186547*i
+        + 0.577350269189626*j
+        + 0.500000000000000*k
+
+        """
+        nprec = prec_to_dps(prec)
+        return Quaternion(*[arg.evalf(n=nprec) for arg in self.args])
+
+    def pow_cos_sin(self, p):
+        """Computes the pth power in the cos-sin form.
+
+        Parameters
+        ==========
+
+        p : int
+            Power to be applied on quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            The p-th power in the cos-sin form.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.pow_cos_sin(4)
+        900*cos(4*acos(sqrt(30)/30))
+        + 1800*sqrt(29)*sin(4*acos(sqrt(30)/30))/29*i
+        + 2700*sqrt(29)*sin(4*acos(sqrt(30)/30))/29*j
+        + 3600*sqrt(29)*sin(4*acos(sqrt(30)/30))/29*k
+
+        """
+        # q = ||q||*(cos(a) + u*sin(a))
+        # q^p = ||q||^p * (cos(p*a) + u*sin(p*a))
+
+        q = self
+        (v, angle) = q.to_axis_angle()
+        q2 = Quaternion.from_axis_angle(v, p * angle)
+        return q2 * (q.norm()**p)
+
+    def integrate(self, *args):
+        """Computes integration of quaternion.
+
+        Returns
+        =======
+
+        Quaternion
+            Integration of the quaternion(self) with the given variable.
+
+        Examples
+        ========
+
+        Indefinite Integral of quaternion :
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import x
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.integrate(x)
+        x + 2*x*i + 3*x*j + 4*x*k
+
+        Definite integral of quaternion :
+
+        >>> from sympy import Quaternion
+        >>> from sympy.abc import x
+        >>> q = Quaternion(1, 2, 3, 4)
+        >>> q.integrate((x, 1, 5))
+        4 + 8*i + 12*j + 16*k
+
+        """
+        # TODO: is this expression correct?
+        return Quaternion(integrate(self.a, *args), integrate(self.b, *args),
+                          integrate(self.c, *args), integrate(self.d, *args))
+
+    @staticmethod
+    def rotate_point(pin, r):
+        """Returns the coordinates of the point pin (a 3 tuple) after rotation.
+
+        Parameters
+        ==========
+
+        pin : tuple
+            A 3-element tuple of coordinates of a point which needs to be
+            rotated.
+        r : Quaternion or tuple
+            Axis and angle of rotation.
+
+            It's important to note that when r is a tuple, it must be of the form
+            (axis, angle)
+
+        Returns
+        =======
+
+        tuple
+            The coordinates of the point after rotation.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import symbols, trigsimp, cos, sin
+        >>> x = symbols('x')
+        >>> q = Quaternion(cos(x/2), 0, 0, sin(x/2))
+        >>> trigsimp(Quaternion.rotate_point((1, 1, 1), q))
+        (sqrt(2)*cos(x + pi/4), sqrt(2)*sin(x + pi/4), 1)
+        >>> (axis, angle) = q.to_axis_angle()
+        >>> trigsimp(Quaternion.rotate_point((1, 1, 1), (axis, angle)))
+        (sqrt(2)*cos(x + pi/4), sqrt(2)*sin(x + pi/4), 1)
+
+        """
+        if isinstance(r, tuple):
+            # if r is of the form (vector, angle)
+            q = Quaternion.from_axis_angle(r[0], r[1])
+        else:
+            # if r is a quaternion
+            q = r.normalize()
+        pout = q * Quaternion(0, pin[0], pin[1], pin[2]) * conjugate(q)
+        return (pout.b, pout.c, pout.d)
+
+    def to_axis_angle(self):
+        """Returns the axis and angle of rotation of a quaternion.
+
+        Returns
+        =======
+
+        tuple
+            Tuple of (axis, angle)
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> q = Quaternion(1, 1, 1, 1)
+        >>> (axis, angle) = q.to_axis_angle()
+        >>> axis
+        (sqrt(3)/3, sqrt(3)/3, sqrt(3)/3)
+        >>> angle
+        2*pi/3
+
+        """
+        q = self
+        if q.a.is_negative:
+            q = q * -1
+
+        q = q.normalize()
+        angle = trigsimp(2 * acos(q.a))
+
+        # Since quaternion is normalised, q.a is less than 1.
+        s = sqrt(1 - q.a*q.a)
+
+        x = trigsimp(q.b / s)
+        y = trigsimp(q.c / s)
+        z = trigsimp(q.d / s)
+
+        v = (x, y, z)
+        t = (v, angle)
+
+        return t
+
+    def to_rotation_matrix(self, v=None, homogeneous=True):
+        """Returns the equivalent rotation transformation matrix of the quaternion
+        which represents rotation about the origin if ``v`` is not passed.
+
+        Parameters
+        ==========
+
+        v : tuple or None
+            Default value: None
+        homogeneous : bool
+            When True, gives an expression that may be more efficient for
+            symbolic calculations but less so for direct evaluation. Both
+            formulas are mathematically equivalent.
+            Default value: True
+
+        Returns
+        =======
+
+        tuple
+            Returns the equivalent rotation transformation matrix of the quaternion
+            which represents rotation about the origin if v is not passed.
+
+        Examples
+        ========
+
+        >>> from sympy import Quaternion
+        >>> from sympy import symbols, trigsimp, cos, sin
+        >>> x = symbols('x')
+        >>> q = Quaternion(cos(x/2), 0, 0, sin(x/2))
+        >>> trigsimp(q.to_rotation_matrix())
+        Matrix([
+        [cos(x), -sin(x), 0],
+        [sin(x),  cos(x), 0],
+        [     0,       0, 1]])
+
+        Generates a 4x4 transformation matrix (used for rotation about a point
+        other than the origin) if the point(v) is passed as an argument.
+        """
+
+        q = self
+        s = q.norm()**-2
+
+        # diagonal elements are different according to parameter normal
+        if homogeneous:
+            m00 = s*(q.a**2 + q.b**2 - q.c**2 - q.d**2)
+            m11 = s*(q.a**2 - q.b**2 + q.c**2 - q.d**2)
+            m22 = s*(q.a**2 - q.b**2 - q.c**2 + q.d**2)
+        else:
+            m00 = 1 - 2*s*(q.c**2 + q.d**2)
+            m11 = 1 - 2*s*(q.b**2 + q.d**2)
+            m22 = 1 - 2*s*(q.b**2 + q.c**2)
+
+        m01 = 2*s*(q.b*q.c - q.d*q.a)
+        m02 = 2*s*(q.b*q.d + q.c*q.a)
+
+        m10 = 2*s*(q.b*q.c + q.d*q.a)
+        m12 = 2*s*(q.c*q.d - q.b*q.a)
+
+        m20 = 2*s*(q.b*q.d - q.c*q.a)
+        m21 = 2*s*(q.c*q.d + q.b*q.a)
+
+        if not v:
+            return Matrix([[m00, m01, m02], [m10, m11, m12], [m20, m21, m22]])
+
+        else:
+            (x, y, z) = v
+
+            m03 = x - x*m00 - y*m01 - z*m02
+            m13 = y - x*m10 - y*m11 - z*m12
+            m23 = z - x*m20 - y*m21 - z*m22
+            m30 = m31 = m32 = 0
+            m33 = 1
+
+            return Matrix([[m00, m01, m02, m03], [m10, m11, m12, m13],
+                          [m20, m21, m22, m23], [m30, m31, m32, m33]])
+
+    def scalar_part(self):
+        r"""Returns scalar part($\mathbf{S}(q)$) of the quaternion q.
+
+        Explanation
+        ===========
+
+        Given a quaternion $q = a + bi + cj + dk$, returns $\mathbf{S}(q) = a$.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(4, 8, 13, 12)
+        >>> q.scalar_part()
+        4
+
+        """
+
+        return self.a
+
+    def vector_part(self):
+        r"""
+        Returns $\mathbf{V}(q)$, the vector part of the quaternion $q$.
+
+        Explanation
+        ===========
+
+        Given a quaternion $q = a + bi + cj + dk$, returns $\mathbf{V}(q) = bi + cj + dk$.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(1, 1, 1, 1)
+        >>> q.vector_part()
+        0 + 1*i + 1*j + 1*k
+
+        >>> q = Quaternion(4, 8, 13, 12)
+        >>> q.vector_part()
+        0 + 8*i + 13*j + 12*k
+
+        """
+
+        return Quaternion(0, self.b, self.c, self.d)
+
+    def axis(self):
+        r"""
+        Returns $\mathbf{Ax}(q)$, the axis of the quaternion $q$.
+
+        Explanation
+        ===========
+
+        Given a quaternion $q = a + bi + cj + dk$, returns $\mathbf{Ax}(q)$  i.e., the versor of the vector part of that quaternion
+        equal to $\mathbf{U}[\mathbf{V}(q)]$.
+        The axis is always an imaginary unit with square equal to $-1 + 0i + 0j + 0k$.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(1, 1, 1, 1)
+        >>> q.axis()
+        0 + sqrt(3)/3*i + sqrt(3)/3*j + sqrt(3)/3*k
+
+        See Also
+        ========
+
+        vector_part
+
+        """
+        axis = self.vector_part().normalize()
+
+        return Quaternion(0, axis.b, axis.c, axis.d)
+
+    def is_pure(self):
+        """
+        Returns true if the quaternion is pure, false if the quaternion is not pure
+        or returns none if it is unknown.
+
+        Explanation
+        ===========
+
+        A pure quaternion (also a vector quaternion) is a quaternion with scalar
+        part equal to 0.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(0, 8, 13, 12)
+        >>> q.is_pure()
+        True
+
+        See Also
+        ========
+        scalar_part
+
+        """
+
+        return self.a.is_zero
+
+    def is_zero_quaternion(self):
+        """
+        Returns true if the quaternion is a zero quaternion or false if it is not a zero quaternion
+        and None if the value is unknown.
+
+        Explanation
+        ===========
+
+        A zero quaternion is a quaternion with both scalar part and
+        vector part equal to 0.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(1, 0, 0, 0)
+        >>> q.is_zero_quaternion()
+        False
+
+        >>> q = Quaternion(0, 0, 0, 0)
+        >>> q.is_zero_quaternion()
+        True
+
+        See Also
+        ========
+        scalar_part
+        vector_part
+
+        """
+
+        return self.norm().is_zero
+
+    def angle(self):
+        r"""
+        Returns the angle of the quaternion measured in the real-axis plane.
+
+        Explanation
+        ===========
+
+        Given a quaternion $q = a + bi + cj + dk$ where $a$, $b$, $c$ and $d$
+        are real numbers, returns the angle of the quaternion given by
+
+        .. math::
+            \theta := 2 \operatorname{atan_2}\left(\sqrt{b^2 + c^2 + d^2}, {a}\right)
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(1, 4, 4, 4)
+        >>> q.angle()
+        2*atan(4*sqrt(3))
+
+        """
+
+        return 2 * atan2(self.vector_part().norm(), self.scalar_part())
+
+
+    def arc_coplanar(self, other):
+        """
+        Returns True if the transformation arcs represented by the input quaternions happen in the same plane.
+
+        Explanation
+        ===========
+
+        Two quaternions are said to be coplanar (in this arc sense) when their axes are parallel.
+        The plane of a quaternion is the one normal to its axis.
+
+        Parameters
+        ==========
+
+        other : a Quaternion
+
+        Returns
+        =======
+
+        True : if the planes of the two quaternions are the same, apart from its orientation/sign.
+        False : if the planes of the two quaternions are not the same, apart from its orientation/sign.
+        None : if plane of either of the quaternion is unknown.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q1 = Quaternion(1, 4, 4, 4)
+        >>> q2 = Quaternion(3, 8, 8, 8)
+        >>> Quaternion.arc_coplanar(q1, q2)
+        True
+
+        >>> q1 = Quaternion(2, 8, 13, 12)
+        >>> Quaternion.arc_coplanar(q1, q2)
+        False
+
+        See Also
+        ========
+
+        vector_coplanar
+        is_pure
+
+        """
+        if (self.is_zero_quaternion()) or (other.is_zero_quaternion()):
+            raise ValueError('Neither of the given quaternions can be 0')
+
+        return fuzzy_or([(self.axis() - other.axis()).is_zero_quaternion(), (self.axis() + other.axis()).is_zero_quaternion()])
+
+    @classmethod
+    def vector_coplanar(cls, q1, q2, q3):
+        r"""
+        Returns True if the axis of the pure quaternions seen as 3D vectors
+        ``q1``, ``q2``, and ``q3`` are coplanar.
+
+        Explanation
+        ===========
+
+        Three pure quaternions are vector coplanar if the quaternions seen as 3D vectors are coplanar.
+
+        Parameters
+        ==========
+
+        q1
+            A pure Quaternion.
+        q2
+            A pure Quaternion.
+        q3
+            A pure Quaternion.
+
+        Returns
+        =======
+
+        True : if the axis of the pure quaternions seen as 3D vectors
+        q1, q2, and q3 are coplanar.
+        False : if the axis of the pure quaternions seen as 3D vectors
+        q1, q2, and q3 are not coplanar.
+        None : if the axis of the pure quaternions seen as 3D vectors
+        q1, q2, and q3 are coplanar is unknown.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q1 = Quaternion(0, 4, 4, 4)
+        >>> q2 = Quaternion(0, 8, 8, 8)
+        >>> q3 = Quaternion(0, 24, 24, 24)
+        >>> Quaternion.vector_coplanar(q1, q2, q3)
+        True
+
+        >>> q1 = Quaternion(0, 8, 16, 8)
+        >>> q2 = Quaternion(0, 8, 3, 12)
+        >>> Quaternion.vector_coplanar(q1, q2, q3)
+        False
+
+        See Also
+        ========
+
+        axis
+        is_pure
+
+        """
+
+        if fuzzy_not(q1.is_pure()) or fuzzy_not(q2.is_pure()) or fuzzy_not(q3.is_pure()):
+            raise ValueError('The given quaternions must be pure')
+
+        M = Matrix([[q1.b, q1.c, q1.d], [q2.b, q2.c, q2.d], [q3.b, q3.c, q3.d]]).det()
+        return M.is_zero
+
+    def parallel(self, other):
+        """
+        Returns True if the two pure quaternions seen as 3D vectors are parallel.
+
+        Explanation
+        ===========
+
+        Two pure quaternions are called parallel when their vector product is commutative which
+        implies that the quaternions seen as 3D vectors have same direction.
+
+        Parameters
+        ==========
+
+        other : a Quaternion
+
+        Returns
+        =======
+
+        True : if the two pure quaternions seen as 3D vectors are parallel.
+        False : if the two pure quaternions seen as 3D vectors are not parallel.
+        None : if the two pure quaternions seen as 3D vectors are parallel is unknown.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(0, 4, 4, 4)
+        >>> q1 = Quaternion(0, 8, 8, 8)
+        >>> q.parallel(q1)
+        True
+
+        >>> q1 = Quaternion(0, 8, 13, 12)
+        >>> q.parallel(q1)
+        False
+
+        """
+
+        if fuzzy_not(self.is_pure()) or fuzzy_not(other.is_pure()):
+            raise ValueError('The provided quaternions must be pure')
+
+        return (self*other - other*self).is_zero_quaternion()
+
+    def orthogonal(self, other):
+        """
+        Returns the orthogonality of two quaternions.
+
+        Explanation
+        ===========
+
+        Two pure quaternions are called orthogonal when their product is anti-commutative.
+
+        Parameters
+        ==========
+
+        other : a Quaternion
+
+        Returns
+        =======
+
+        True : if the two pure quaternions seen as 3D vectors are orthogonal.
+        False : if the two pure quaternions seen as 3D vectors are not orthogonal.
+        None : if the two pure quaternions seen as 3D vectors are orthogonal is unknown.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(0, 4, 4, 4)
+        >>> q1 = Quaternion(0, 8, 8, 8)
+        >>> q.orthogonal(q1)
+        False
+
+        >>> q1 = Quaternion(0, 2, 2, 0)
+        >>> q = Quaternion(0, 2, -2, 0)
+        >>> q.orthogonal(q1)
+        True
+
+        """
+
+        if fuzzy_not(self.is_pure()) or fuzzy_not(other.is_pure()):
+            raise ValueError('The given quaternions must be pure')
+
+        return (self*other + other*self).is_zero_quaternion()
+
+    def index_vector(self):
+        r"""
+        Returns the index vector of the quaternion.
+
+        Explanation
+        ===========
+
+        The index vector is given by $\mathbf{T}(q)$, the norm (or magnitude) of
+        the quaternion $q$, multiplied by $\mathbf{Ax}(q)$, the axis of $q$.
+
+        Returns
+        =======
+
+        Quaternion: representing index vector of the provided quaternion.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(2, 4, 2, 4)
+        >>> q.index_vector()
+        0 + 4*sqrt(10)/3*i + 2*sqrt(10)/3*j + 4*sqrt(10)/3*k
+
+        See Also
+        ========
+
+        axis
+        norm
+
+        """
+
+        return self.norm() * self.axis()
+
+    def mensor(self):
+        """
+        Returns the natural logarithm of the norm(magnitude) of the quaternion.
+
+        Examples
+        ========
+
+        >>> from sympy.algebras.quaternion import Quaternion
+        >>> q = Quaternion(2, 4, 2, 4)
+        >>> q.mensor()
+        log(2*sqrt(10))
+        >>> q.norm()
+        2*sqrt(10)
+
+        See Also
+        ========
+
+        norm
+
+        """
+
+        return ln(self.norm())

lib/python3.10/site-packages/sympy/algebras/tests/test_quaternion.py

@@ -0,0 +1,428 @@
+from sympy.testing.pytest import slow
+from sympy.core.function import diff
+from sympy.core.function import expand
+from sympy.core.numbers import (E, I, Rational, pi)
+from sympy.core.singleton import S
+from sympy.core.symbol import (Symbol, symbols)
+from sympy.functions.elementary.complexes import (Abs, conjugate, im, re, sign)
+from sympy.functions.elementary.exponential import log
+from sympy.functions.elementary.miscellaneous import sqrt
+from sympy.functions.elementary.trigonometric import (acos, asin, cos, sin, atan2, atan)
+from sympy.integrals.integrals import integrate
+from sympy.matrices.dense import Matrix
+from sympy.simplify import simplify
+from sympy.simplify.trigsimp import trigsimp
+from sympy.algebras.quaternion import Quaternion
+from sympy.testing.pytest import raises
+import math
+from itertools import permutations, product
+
+w, x, y, z = symbols('w:z')
+phi = symbols('phi')
+
+def test_quaternion_construction():
+    q = Quaternion(w, x, y, z)
+    assert q + q == Quaternion(2*w, 2*x, 2*y, 2*z)
+
+    q2 = Quaternion.from_axis_angle((sqrt(3)/3, sqrt(3)/3, sqrt(3)/3),
+                                    pi*Rational(2, 3))
+    assert q2 == Quaternion(S.Half, S.Half,
+                            S.Half, S.Half)
+
+    M = Matrix([[cos(phi), -sin(phi), 0], [sin(phi), cos(phi), 0], [0, 0, 1]])
+    q3 = trigsimp(Quaternion.from_rotation_matrix(M))
+    assert q3 == Quaternion(
+        sqrt(2)*sqrt(cos(phi) + 1)/2, 0, 0, sqrt(2 - 2*cos(phi))*sign(sin(phi))/2)
+
+    nc = Symbol('nc', commutative=False)
+    raises(ValueError, lambda: Quaternion(w, x, nc, z))
+
+
+def test_quaternion_construction_norm():
+    q1 = Quaternion(*symbols('a:d'))
+
+    q2 = Quaternion(w, x, y, z)
+    assert expand((q1*q2).norm()**2 - (q1.norm()**2 * q2.norm()**2)) == 0
+
+    q3 = Quaternion(w, x, y, z, norm=1)
+    assert (q1 * q3).norm() == q1.norm()
+
+
+def test_issue_25254():
+    # calculating the inverse cached the norm which caused problems
+    # when multiplying
+    p = Quaternion(1, 0, 0, 0)
+    q = Quaternion.from_axis_angle((1, 1, 1), 3 * math.pi/4)
+    qi = q.inverse()  # this operation cached the norm
+    test = q * p * qi
+    assert ((test - p).norm() < 1E-10)
+
+
+def test_to_and_from_Matrix():
+    q = Quaternion(w, x, y, z)
+    q_full = Quaternion.from_Matrix(q.to_Matrix())
+    q_vect = Quaternion.from_Matrix(q.to_Matrix(True))
+    assert (q - q_full).is_zero_quaternion()
+    assert (q.vector_part() - q_vect).is_zero_quaternion()
+
+
+def test_product_matrices():
+    q1 = Quaternion(w, x, y, z)
+    q2 = Quaternion(*(symbols("a:d")))
+    assert (q1 * q2).to_Matrix() == q1.product_matrix_left * q2.to_Matrix()
+    assert (q1 * q2).to_Matrix() == q2.product_matrix_right * q1.to_Matrix()
+
+    R1 = (q1.product_matrix_left * q1.product_matrix_right.T)[1:, 1:]
+    R2 = simplify(q1.to_rotation_matrix()*q1.norm()**2)
+    assert R1 == R2
+
+
+def test_quaternion_axis_angle():
+
+    test_data = [ # axis, angle, expected_quaternion
+        ((1, 0, 0), 0, (1, 0, 0, 0)),
+        ((1, 0, 0), pi/2, (sqrt(2)/2, sqrt(2)/2, 0, 0)),
+        ((0, 1, 0), pi/2, (sqrt(2)/2, 0, sqrt(2)/2, 0)),
+        ((0, 0, 1), pi/2, (sqrt(2)/2, 0, 0, sqrt(2)/2)),
+        ((1, 0, 0), pi, (0, 1, 0, 0)),
+        ((0, 1, 0), pi, (0, 0, 1, 0)),
+        ((0, 0, 1), pi, (0, 0, 0, 1)),
+        ((1, 1, 1), pi, (0, 1/sqrt(3),1/sqrt(3),1/sqrt(3))),
+        ((sqrt(3)/3, sqrt(3)/3, sqrt(3)/3), pi*2/3, (S.Half, S.Half, S.Half, S.Half))
+    ]
+
+    for axis, angle, expected in test_data:
+        assert Quaternion.from_axis_angle(axis, angle) == Quaternion(*expected)
+
+
+def test_quaternion_axis_angle_simplification():
+    result = Quaternion.from_axis_angle((1, 2, 3), asin(4))
+    assert result.a == cos(asin(4)/2)
+    assert result.b == sqrt(14)*sin(asin(4)/2)/14
+    assert result.c == sqrt(14)*sin(asin(4)/2)/7
+    assert result.d == 3*sqrt(14)*sin(asin(4)/2)/14
+
+def test_quaternion_complex_real_addition():
+    a = symbols("a", complex=True)
+    b = symbols("b", real=True)
+    # This symbol is not complex:
+    c = symbols("c", commutative=False)
+
+    q = Quaternion(w, x, y, z)
+    assert a + q == Quaternion(w + re(a), x + im(a), y, z)
+    assert 1 + q == Quaternion(1 + w, x, y, z)
+    assert I + q == Quaternion(w, 1 + x, y, z)
+    assert b + q == Quaternion(w + b, x, y, z)
+    raises(ValueError, lambda: c + q)
+    raises(ValueError, lambda: q * c)
+    raises(ValueError, lambda: c * q)
+
+    assert -q == Quaternion(-w, -x, -y, -z)
+
+    q1 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+    q2 = Quaternion(1, 4, 7, 8)
+
+    assert q1 + (2 + 3*I) == Quaternion(5 + 7*I, 2 + 5*I, 0, 7 + 8*I)
+    assert q2 + (2 + 3*I) == Quaternion(3, 7, 7, 8)
+    assert q1 * (2 + 3*I) == \
+    Quaternion((2 + 3*I)*(3 + 4*I), (2 + 3*I)*(2 + 5*I), 0, (2 + 3*I)*(7 + 8*I))
+    assert q2 * (2 + 3*I) == Quaternion(-10, 11, 38, -5)
+
+    q1 = Quaternion(1, 2, 3, 4)
+    q0 = Quaternion(0, 0, 0, 0)
+    assert q1 + q0 == q1
+    assert q1 - q0 == q1
+    assert q1 - q1 == q0
+
+
+def test_quaternion_subs():
+    q = Quaternion.from_axis_angle((0, 0, 1), phi)
+    assert q.subs(phi, 0) == Quaternion(1, 0, 0, 0)
+
+
+def test_quaternion_evalf():
+    assert (Quaternion(sqrt(2), 0, 0, sqrt(3)).evalf() ==
+            Quaternion(sqrt(2).evalf(), 0, 0, sqrt(3).evalf()))
+    assert (Quaternion(1/sqrt(2), 0, 0, 1/sqrt(2)).evalf() ==
+            Quaternion((1/sqrt(2)).evalf(), 0, 0, (1/sqrt(2)).evalf()))
+
+
+def test_quaternion_functions():
+    q = Quaternion(w, x, y, z)
+    q1 = Quaternion(1, 2, 3, 4)
+    q0 = Quaternion(0, 0, 0, 0)
+
+    assert conjugate(q) == Quaternion(w, -x, -y, -z)
+    assert q.norm() == sqrt(w**2 + x**2 + y**2 + z**2)
+    assert q.normalize() == Quaternion(w, x, y, z) / sqrt(w**2 + x**2 + y**2 + z**2)
+    assert q.inverse() == Quaternion(w, -x, -y, -z) / (w**2 + x**2 + y**2 + z**2)
+    assert q.inverse() == q.pow(-1)
+    raises(ValueError, lambda: q0.inverse())
+    assert q.pow(2) == Quaternion(w**2 - x**2 - y**2 - z**2, 2*w*x, 2*w*y, 2*w*z)
+    assert q**(2) == Quaternion(w**2 - x**2 - y**2 - z**2, 2*w*x, 2*w*y, 2*w*z)
+    assert q1.pow(-2) == Quaternion(
+        Rational(-7, 225), Rational(-1, 225), Rational(-1, 150), Rational(-2, 225))
+    assert q1**(-2) == Quaternion(
+        Rational(-7, 225), Rational(-1, 225), Rational(-1, 150), Rational(-2, 225))
+    assert q1.pow(-0.5) == NotImplemented
+    raises(TypeError, lambda: q1**(-0.5))
+
+    assert q1.exp() == \
+    Quaternion(E * cos(sqrt(29)),
+               2 * sqrt(29) * E * sin(sqrt(29)) / 29,
+               3 * sqrt(29) * E * sin(sqrt(29)) / 29,
+               4 * sqrt(29) * E * sin(sqrt(29)) / 29)
+    assert q1.log() == \
+    Quaternion(log(sqrt(30)),
+               2 * sqrt(29) * acos(sqrt(30)/30) / 29,
+               3 * sqrt(29) * acos(sqrt(30)/30) / 29,
+               4 * sqrt(29) * acos(sqrt(30)/30) / 29)
+
+    assert q1.pow_cos_sin(2) == \
+    Quaternion(30 * cos(2 * acos(sqrt(30)/30)),
+               60 * sqrt(29) * sin(2 * acos(sqrt(30)/30)) / 29,
+               90 * sqrt(29) * sin(2 * acos(sqrt(30)/30)) / 29,
+               120 * sqrt(29) * sin(2 * acos(sqrt(30)/30)) / 29)
+
+    assert diff(Quaternion(x, x, x, x), x) == Quaternion(1, 1, 1, 1)
+
+    assert integrate(Quaternion(x, x, x, x), x) == \
+    Quaternion(x**2 / 2, x**2 / 2, x**2 / 2, x**2 / 2)
+
+    assert Quaternion.rotate_point((1, 1, 1), q1) == (S.One / 5, 1, S(7) / 5)
+    n = Symbol('n')
+    raises(TypeError, lambda: q1**n)
+    n = Symbol('n', integer=True)
+    raises(TypeError, lambda: q1**n)
+
+    assert Quaternion(22, 23, 55, 8).scalar_part() == 22
+    assert Quaternion(w, x, y, z).scalar_part() == w
+
+    assert Quaternion(22, 23, 55, 8).vector_part() == Quaternion(0, 23, 55, 8)
+    assert Quaternion(w, x, y, z).vector_part() == Quaternion(0, x, y, z)
+
+    assert q1.axis() == Quaternion(0, 2*sqrt(29)/29, 3*sqrt(29)/29, 4*sqrt(29)/29)
+    assert q1.axis().pow(2) == Quaternion(-1, 0, 0, 0)
+    assert q0.axis().scalar_part() == 0
+    assert (q.axis() == Quaternion(0,
+                                   x/sqrt(x**2 + y**2 + z**2),
+                                   y/sqrt(x**2 + y**2 + z**2),
+                                   z/sqrt(x**2 + y**2 + z**2)))
+
+    assert q0.is_pure() is True
+    assert q1.is_pure() is False
+    assert Quaternion(0, 0, 0, 3).is_pure() is True
+    assert Quaternion(0, 2, 10, 3).is_pure() is True
+    assert Quaternion(w, 2, 10, 3).is_pure() is None
+
+    assert q1.angle() == 2*atan(sqrt(29))
+    assert q.angle() == 2*atan2(sqrt(x**2 + y**2 + z**2), w)
+
+    assert Quaternion.arc_coplanar(q1, Quaternion(2, 4, 6, 8)) is True
+    assert Quaternion.arc_coplanar(q1, Quaternion(1, -2, -3, -4)) is True
+    assert Quaternion.arc_coplanar(q1, Quaternion(1, 8, 12, 16)) is True
+    assert Quaternion.arc_coplanar(q1, Quaternion(1, 2, 3, 4)) is True
+    assert Quaternion.arc_coplanar(q1, Quaternion(w, 4, 6, 8)) is True
+    assert Quaternion.arc_coplanar(q1, Quaternion(2, 7, 4, 1)) is False
+    assert Quaternion.arc_coplanar(q1, Quaternion(w, x, y, z)) is None
+    raises(ValueError, lambda: Quaternion.arc_coplanar(q1, q0))
+
+    assert Quaternion.vector_coplanar(
+        Quaternion(0, 8, 12, 16),
+        Quaternion(0, 4, 6, 8),
+        Quaternion(0, 2, 3, 4)) is True
+    assert Quaternion.vector_coplanar(
+        Quaternion(0, 0, 0, 0), Quaternion(0, 4, 6, 8), Quaternion(0, 2, 3, 4)) is True
+    assert Quaternion.vector_coplanar(
+        Quaternion(0, 8, 2, 6), Quaternion(0, 1, 6, 6), Quaternion(0, 0, 3, 4)) is False
+    assert Quaternion.vector_coplanar(
+        Quaternion(0, 1, 3, 4),
+        Quaternion(0, 4, w, 6),
+        Quaternion(0, 6, 8, 1)) is None
+    raises(ValueError, lambda:
+        Quaternion.vector_coplanar(q0, Quaternion(0, 4, 6, 8), q1))
+
+    assert Quaternion(0, 1, 2, 3).parallel(Quaternion(0, 2, 4, 6)) is True
+    assert Quaternion(0, 1, 2, 3).parallel(Quaternion(0, 2, 2, 6)) is False
+    assert Quaternion(0, 1, 2, 3).parallel(Quaternion(w, x, y, 6)) is None
+    raises(ValueError, lambda: q0.parallel(q1))
+
+    assert Quaternion(0, 1, 2, 3).orthogonal(Quaternion(0, -2, 1, 0)) is True
+    assert Quaternion(0, 2, 4, 7).orthogonal(Quaternion(0, 2, 2, 6)) is False
+    assert Quaternion(0, 2, 4, 7).orthogonal(Quaternion(w, x, y, 6)) is None
+    raises(ValueError, lambda: q0.orthogonal(q1))
+
+    assert q1.index_vector() == Quaternion(
+        0, 2*sqrt(870)/29,
+        3*sqrt(870)/29,
+        4*sqrt(870)/29)
+    assert Quaternion(0, 3, 9, 4).index_vector() == Quaternion(0, 3, 9, 4)
+
+    assert Quaternion(4, 3, 9, 4).mensor() == log(sqrt(122))
+    assert Quaternion(3, 3, 0, 2).mensor() == log(sqrt(22))
+
+    assert q0.is_zero_quaternion() is True
+    assert q1.is_zero_quaternion() is False
+    assert Quaternion(w, 0, 0, 0).is_zero_quaternion() is None
+
+def test_quaternion_conversions():
+    q1 = Quaternion(1, 2, 3, 4)
+
+    assert q1.to_axis_angle() == ((2 * sqrt(29)/29,
+                                   3 * sqrt(29)/29,
+                                   4 * sqrt(29)/29),
+                                   2 * acos(sqrt(30)/30))
+
+    assert (q1.to_rotation_matrix() ==
+            Matrix([[Rational(-2, 3), Rational(2, 15), Rational(11, 15)],
+                    [Rational(2, 3), Rational(-1, 3), Rational(2, 3)],
+                    [Rational(1, 3), Rational(14, 15), Rational(2, 15)]]))
+
+    assert (q1.to_rotation_matrix((1, 1, 1)) ==
+            Matrix([
+                [Rational(-2, 3), Rational(2, 15), Rational(11, 15), Rational(4, 5)],
+                [Rational(2, 3), Rational(-1, 3), Rational(2, 3), S.Zero],
+                [Rational(1, 3), Rational(14, 15), Rational(2, 15), Rational(-2, 5)],
+                [S.Zero, S.Zero, S.Zero, S.One]]))
+
+    theta = symbols("theta", real=True)
+    q2 = Quaternion(cos(theta/2), 0, 0, sin(theta/2))
+
+    assert trigsimp(q2.to_rotation_matrix()) == Matrix([
+                                               [cos(theta), -sin(theta), 0],
+                                               [sin(theta),  cos(theta), 0],
+                                               [0,           0,          1]])
+
+    assert q2.to_axis_angle() == ((0, 0, sin(theta/2)/Abs(sin(theta/2))),
+                                   2*acos(cos(theta/2)))
+
+    assert trigsimp(q2.to_rotation_matrix((1, 1, 1))) == Matrix([
+               [cos(theta), -sin(theta), 0, sin(theta) - cos(theta) + 1],
+               [sin(theta),  cos(theta), 0, -sin(theta) - cos(theta) + 1],
+               [0,           0,          1,  0],
+               [0,           0,          0,  1]])
+
+
+def test_rotation_matrix_homogeneous():
+    q = Quaternion(w, x, y, z)
+    R1 = q.to_rotation_matrix(homogeneous=True) * q.norm()**2
+    R2 = simplify(q.to_rotation_matrix(homogeneous=False) * q.norm()**2)
+    assert R1 == R2
+
+
+def test_quaternion_rotation_iss1593():
+    """
+    There was a sign mistake in the definition,
+    of the rotation matrix. This tests that particular sign mistake.
+    See issue 1593 for reference.
+    See wikipedia
+    https://en.wikipedia.org/wiki/Quaternions_and_spatial_rotation#Quaternion-derived_rotation_matrix
+    for the correct definition
+    """
+    q = Quaternion(cos(phi/2), sin(phi/2), 0, 0)
+    assert(trigsimp(q.to_rotation_matrix()) == Matrix([
+                [1,        0,         0],
+                [0, cos(phi), -sin(phi)],
+                [0, sin(phi),  cos(phi)]]))
+
+
+def test_quaternion_multiplication():
+    q1 = Quaternion(3 + 4*I, 2 + 5*I, 0, 7 + 8*I, real_field = False)
+    q2 = Quaternion(1, 2, 3, 5)
+    q3 = Quaternion(1, 1, 1, y)
+
+    assert Quaternion._generic_mul(S(4), S.One) == 4
+    assert (Quaternion._generic_mul(S(4), q1) ==
+            Quaternion(12 + 16*I, 8 + 20*I, 0, 28 + 32*I))
+    assert q2.mul(2) == Quaternion(2, 4, 6, 10)
+    assert q2.mul(q3) == Quaternion(-5*y - 4, 3*y - 2, 9 - 2*y, y + 4)
+    assert q2.mul(q3) == q2*q3
+
+    z = symbols('z', complex=True)
+    z_quat = Quaternion(re(z), im(z), 0, 0)
+    q = Quaternion(*symbols('q:4', real=True))
+
+    assert z * q == z_quat * q
+    assert q * z == q * z_quat
+
+
+def test_issue_16318():
+    #for rtruediv
+    q0 = Quaternion(0, 0, 0, 0)
+    raises(ValueError, lambda: 1/q0)
+    #for rotate_point
+    q = Quaternion(1, 2, 3, 4)
+    (axis, angle) = q.to_axis_angle()
+    assert Quaternion.rotate_point((1, 1, 1), (axis, angle)) == (S.One / 5, 1, S(7) / 5)
+    #test for to_axis_angle
+    q = Quaternion(-1, 1, 1, 1)
+    axis = (-sqrt(3)/3, -sqrt(3)/3, -sqrt(3)/3)
+    angle = 2*pi/3
+    assert (axis, angle) == q.to_axis_angle()
+
+
+@slow
+def test_to_euler():
+    q = Quaternion(w, x, y, z)
+    q_normalized = q.normalize()
+
+    seqs = ['zxy', 'zyx', 'zyz', 'zxz']
+    seqs += [seq.upper() for seq in seqs]
+
+    for seq in seqs:
+        euler_from_q = q.to_euler(seq)
+        q_back = simplify(Quaternion.from_euler(euler_from_q, seq))
+        assert q_back == q_normalized
+
+
+def test_to_euler_iss24504():
+    """
+    There was a mistake in the degenerate case testing
+    See issue 24504 for reference.
+    """
+    q = Quaternion.from_euler((phi, 0, 0), 'zyz')
+    assert trigsimp(q.to_euler('zyz'), inverse=True) == (phi, 0, 0)
+
+
+def test_to_euler_numerical_singilarities():
+
+    def test_one_case(angles, seq):
+        q = Quaternion.from_euler(angles, seq)
+        assert q.to_euler(seq) == angles
+
+    # symmetric
+    test_one_case((pi/2,  0, 0), 'zyz')
+    test_one_case((pi/2,  0, 0), 'ZYZ')
+    test_one_case((pi/2,  pi, 0), 'zyz')
+    test_one_case((pi/2,  pi, 0), 'ZYZ')
+
+    # asymmetric
+    test_one_case((pi/2,  pi/2, 0), 'zyx')
+    test_one_case((pi/2,  -pi/2, 0), 'zyx')
+    test_one_case((pi/2,  pi/2, 0), 'ZYX')
+    test_one_case((pi/2,  -pi/2, 0), 'ZYX')
+
+
+@slow
+def test_to_euler_options():
+    def test_one_case(q):
+        angles1 = Matrix(q.to_euler(seq, True, True))
+        angles2 = Matrix(q.to_euler(seq, False, False))
+        angle_errors = simplify(angles1-angles2).evalf()
+        for angle_error in angle_errors:
+            # forcing angles to set {-pi, pi}
+            angle_error = (angle_error + pi) % (2 * pi) - pi
+            assert angle_error < 10e-7
+
+    for xyz in ('xyz', 'XYZ'):
+        for seq_tuple in permutations(xyz):
+            for symmetric in (True, False):
+                if symmetric:
+                    seq = ''.join([seq_tuple[0], seq_tuple[1], seq_tuple[0]])
+                else:
+                    seq = ''.join(seq_tuple)
+
+                for elements in product([-1, 0, 1], repeat=4):
+                    q = Quaternion(*elements)
+                    if not q.is_zero_quaternion():
+                        test_one_case(q)

lib/python3.10/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.10/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.10/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.10/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.10/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.10/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.10/site-packages/sympy/assumptions/handlers/__init__.py

@@ -0,0 +1,13 @@
+"""
+Multipledispatch handlers for ``Predicate`` are implemented here.
+Handlers in this module are not directly imported to other modules in
+order to avoid circular import problem.
+"""
+
+from .common import (AskHandler, CommonHandler,
+    test_closed_group)
+
+__all__ = [
+    'AskHandler', 'CommonHandler',
+    'test_closed_group'
+]

lib/python3.10/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.10/site-packages/sympy/assumptions/handlers/common.py

@@ -0,0 +1,156 @@
+"""
+This module defines base class for handlers and some core handlers:
+``Q.commutative`` and ``Q.is_true``.
+"""
+
+from sympy.assumptions import Q, ask, AppliedPredicate
+from sympy.core import Basic, Symbol
+from sympy.core.logic import _fuzzy_group
+from sympy.core.numbers import NaN, Number
+from sympy.logic.boolalg import (And, BooleanTrue, BooleanFalse, conjuncts,
+    Equivalent, Implies, Not, Or)
+from sympy.utilities.exceptions import sympy_deprecation_warning
+
+from ..predicates.common import CommutativePredicate, IsTruePredicate
+
+
+class AskHandler:
+    """Base class that all Ask Handlers must inherit."""
+    def __new__(cls, *args, **kwargs):
+        sympy_deprecation_warning(
+            """
+            The AskHandler system is deprecated. The AskHandler class should
+            be replaced with the multipledispatch handler of Predicate
+            """,
+            deprecated_since_version="1.8",
+            active_deprecations_target='deprecated-askhandler',
+        )
+        return super().__new__(cls, *args, **kwargs)
+
+
+class CommonHandler(AskHandler):
+    # Deprecated
+    """Defines some useful methods common to most Handlers. """
+
+    @staticmethod
+    def AlwaysTrue(expr, assumptions):
+        return True
+
+    @staticmethod
+    def AlwaysFalse(expr, assumptions):
+        return False
+
+    @staticmethod
+    def AlwaysNone(expr, assumptions):
+        return None
+
+    NaN = AlwaysFalse
+
+
+# CommutativePredicate
+
+@CommutativePredicate.register(Symbol)
+def _(expr, assumptions):
+    """Objects are expected to be commutative unless otherwise stated"""
+    assumps = conjuncts(assumptions)
+    if expr.is_commutative is not None:
+        return expr.is_commutative and not ~Q.commutative(expr) in assumps
+    if Q.commutative(expr) in assumps:
+        return True
+    elif ~Q.commutative(expr) in assumps:
+        return False
+    return True
+
+@CommutativePredicate.register(Basic)
+def _(expr, assumptions):
+    for arg in expr.args:
+        if not ask(Q.commutative(arg), assumptions):
+            return False
+    return True
+
+@CommutativePredicate.register(Number)
+def _(expr, assumptions):
+    return True
+
+@CommutativePredicate.register(NaN)
+def _(expr, assumptions):
+    return True
+
+
+# IsTruePredicate
+
+@IsTruePredicate.register(bool)
+def _(expr, assumptions):
+    return expr
+
+@IsTruePredicate.register(BooleanTrue)
+def _(expr, assumptions):
+    return True
+
+@IsTruePredicate.register(BooleanFalse)
+def _(expr, assumptions):
+    return False
+
+@IsTruePredicate.register(AppliedPredicate)
+def _(expr, assumptions):
+    return ask(expr, assumptions)
+
+@IsTruePredicate.register(Not)
+def _(expr, assumptions):
+    arg = expr.args[0]
+    if arg.is_Symbol:
+        # symbol used as abstract boolean object
+        return None
+    value = ask(arg, assumptions=assumptions)
+    if value in (True, False):
+        return not value
+    else:
+        return None
+
+@IsTruePredicate.register(Or)
+def _(expr, assumptions):
+    result = False
+    for arg in expr.args:
+        p = ask(arg, assumptions=assumptions)
+        if p is True:
+            return True
+        if p is None:
+            result = None
+    return result
+
+@IsTruePredicate.register(And)
+def _(expr, assumptions):
+    result = True
+    for arg in expr.args:
+        p = ask(arg, assumptions=assumptions)
+        if p is False:
+            return False
+        if p is None:
+            result = None
+    return result
+
+@IsTruePredicate.register(Implies)
+def _(expr, assumptions):
+    p, q = expr.args
+    return ask(~p | q, assumptions=assumptions)
+
+@IsTruePredicate.register(Equivalent)
+def _(expr, assumptions):
+    p, q = expr.args
+    pt = ask(p, assumptions=assumptions)
+    if pt is None:
+        return None
+    qt = ask(q, assumptions=assumptions)
+    if qt is None:
+        return None
+    return pt == qt
+
+
+#### Helper methods
+def test_closed_group(expr, assumptions, key):
+    """
+    Test for membership in a group with respect
+    to the current operation.
+    """
+    return _fuzzy_group(
+        (ask(key(a), assumptions) for a in expr.args), quick_exit=True)

lib/python3.10/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.10/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.10/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.10/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.10/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.10/site-packages/sympy/assumptions/predicates/__init__.py

@@ -0,0 +1,5 @@
+"""
+Module to implement predicate classes.
+
+Class of every predicate registered to ``Q`` is defined here.
+"""