"""Module for querying SymPy objects about assumptions."""
from __future__ import print_function, division
from sympy.core import sympify
from sympy.core.cache import cacheit
from sympy.core.relational import Relational
from sympy.logic.boolalg import (to_cnf, And, Not, Or, Implies, Equivalent,
BooleanFunction, BooleanAtom)
from sympy.logic.inference import satisfiable
from sympy.assumptions.assume import (global_assumptions, Predicate,
AppliedPredicate)
from sympy.core.decorators import deprecated
from sympy.utilities.decorator import memoize_property
# Deprecated predicates should be added to this list
deprecated_predicates = [
'bounded',
'infinity',
'infinitesimal'
]
# Memoization storage for predicates
predicate_storage = {}
predicate_memo = memoize_property(predicate_storage)
# 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.
[docs]class AssumptionKeys(object):
"""
This class contains all the supported keys by ``ask``.
"""
@predicate_memo
def hermitian(self):
"""
Hermitian predicate.
``ask(Q.hermitian(x))`` is true iff ``x`` belongs to the set of
Hermitian operators.
References
==========
.. [1] http://mathworld.wolfram.com/HermitianOperator.html
"""
# TODO: Add examples
return Predicate('hermitian')
@predicate_memo
def antihermitian(self):
"""
Antihermitian predicate.
``Q.antihermitian(x)`` is true iff ``x`` belongs to the field of
antihermitian operators, i.e., operators in the form ``x*I``, where
``x`` is Hermitian.
References
==========
.. [1] http://mathworld.wolfram.com/HermitianOperator.html
"""
# TODO: Add examples
return Predicate('antihermitian')
@predicate_memo
def real(self):
r"""
Real number predicate.
``Q.real(x)`` is true iff ``x`` is a real number, i.e., it is in the
interval `(-\infty, \infty)`. Note that, in particular the infinities
are not real. Use ``Q.extended_real`` if you want to consider those as
well.
A few important facts about reals:
- Every real number is positive, negative, or zero. Furthermore,
because these sets are pairwise disjoint, each real number is exactly
one of those three.
- Every real number is also complex.
- Every real number is finite.
- Every real number is either rational or irrational.
- Every real number is either algebraic or transcendental.
- The facts ``Q.negative``, ``Q.zero``, ``Q.positive``,
``Q.nonnegative``, ``Q.nonpositive``, ``Q.nonzero``, ``Q.integer``,
``Q.rational``, and ``Q.irrational`` all imply ``Q.real``, as do all
facts that imply those facts.
- The facts ``Q.algebraic``, and ``Q.transcendental`` do not imply
``Q.real``; they imply ``Q.complex``. An algebraic or transcendental
number may or may not be real.
- The "non" facts (i.e., ``Q.nonnegative``, ``Q.nonzero``,
``Q.nonpositive`` and ``Q.noninteger``) are not equivalent to not the
fact, but rather, not the fact *and* ``Q.real``. For example,
``Q.nonnegative`` means ``~Q.negative & Q.real``. So for example,
``I`` is not nonnegative, nonzero, or nonpositive.
Examples
========
>>> from sympy import Q, ask, symbols
>>> x = symbols('x')
>>> ask(Q.real(x), Q.positive(x))
True
>>> ask(Q.real(0))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Real_number
"""
return Predicate('real')
@predicate_memo
def extended_real(self):
r"""
Extended real predicate.
``Q.extended_real(x)`` is true iff ``x`` is a real number or
`\{-\infty, \infty\}`.
See documentation of ``Q.real`` for more information about related facts.
Examples
========
>>> from sympy import ask, Q, oo, I
>>> ask(Q.extended_real(1))
True
>>> ask(Q.extended_real(I))
False
>>> ask(Q.extended_real(oo))
True
"""
return Predicate('extended_real')
@predicate_memo
def imaginary(self):
"""
Imaginary number predicate.
``Q.imaginary(x)`` is true iff ``x`` can be written as a real
number multiplied by the imaginary unit ``I``. Please note that ``0``
is not considered to be an imaginary number.
Examples
========
>>> from sympy import Q, ask, I
>>> ask(Q.imaginary(3*I))
True
>>> ask(Q.imaginary(2 + 3*I))
False
>>> ask(Q.imaginary(0))
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Imaginary_number
"""
return Predicate('imaginary')
@predicate_memo
def complex(self):
"""
Complex number predicate.
``Q.complex(x)`` is true iff ``x`` belongs to the set of complex
numbers. Note that every complex number is finite.
Examples
========
>>> from sympy import Q, Symbol, ask, I, oo
>>> x = Symbol('x')
>>> ask(Q.complex(0))
True
>>> ask(Q.complex(2 + 3*I))
True
>>> ask(Q.complex(oo))
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Complex_number
"""
return Predicate('complex')
@predicate_memo
def algebraic(self):
r"""
Algebraic number predicate.
``Q.algebraic(x)`` is true iff ``x`` belongs to the set of
algebraic numbers. ``x`` is algebraic if there is some polynomial
in ``p(x)\in \mathbb\{Q\}[x]`` such that ``p(x) = 0``.
Examples
========
>>> from sympy import ask, Q, sqrt, I, pi
>>> ask(Q.algebraic(sqrt(2)))
True
>>> ask(Q.algebraic(I))
True
>>> ask(Q.algebraic(pi))
False
References
==========
.. [1] http://en.wikipedia.org/wiki/Algebraic_number
"""
return Predicate('algebraic')
@predicate_memo
def transcendental(self):
"""
Transcedental number predicate.
``Q.transcendental(x)`` is true iff ``x`` belongs to the set of
transcendental numbers. A transcendental number is a real
or complex number that is not algebraic.
"""
# TODO: Add examples
return Predicate('transcendental')
@predicate_memo
def integer(self):
"""
Integer predicate.
``Q.integer(x)`` is true iff ``x`` belongs to the set of integer numbers.
Examples
========
>>> from sympy import Q, ask, S
>>> ask(Q.integer(5))
True
>>> ask(Q.integer(S(1)/2))
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Integer
"""
return Predicate('integer')
@predicate_memo
def rational(self):
"""
Rational number predicate.
``Q.rational(x)`` is true iff ``x`` belongs to the set of
rational numbers.
Examples
========
>>> from sympy import ask, Q, pi, S
>>> ask(Q.rational(0))
True
>>> ask(Q.rational(S(1)/2))
True
>>> ask(Q.rational(pi))
False
References
==========
https://en.wikipedia.org/wiki/Rational_number
"""
return Predicate('rational')
@predicate_memo
def irrational(self):
"""
Irrational number predicate.
``Q.irrational(x)`` is true iff ``x`` is any real number that
cannot be expressed as a ratio of integers.
Examples
========
>>> from sympy import ask, Q, pi, S, I
>>> ask(Q.irrational(0))
False
>>> ask(Q.irrational(S(1)/2))
False
>>> ask(Q.irrational(pi))
True
>>> ask(Q.irrational(I))
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Irrational_number
"""
return Predicate('irrational')
@predicate_memo
def finite(self):
"""
Finite predicate.
``Q.finite(x)`` is true if ``x`` is neither an infinity
nor a ``NaN``. In other words, ``ask(Q.finite(x))`` is true for all ``x``
having a bounded absolute value.
Examples
========
>>> from sympy import Q, ask, Symbol, S, oo, I
>>> x = Symbol('x')
>>> ask(Q.finite(S.NaN))
False
>>> ask(Q.finite(oo))
False
>>> ask(Q.finite(1))
True
>>> ask(Q.finite(2 + 3*I))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Finite
"""
return Predicate('finite')
@predicate_memo
@deprecated(useinstead="finite", issue=9425, deprecated_since_version="1.0")
def bounded(self):
"""
See documentation of ``Q.finite``.
"""
return Predicate('finite')
@predicate_memo
def infinite(self):
"""
Infinite number predicate.
``Q.infinite(x)`` is true iff the absolute value of ``x`` is
infinity.
"""
# TODO: Add examples
return Predicate('infinite')
@predicate_memo
@deprecated(useinstead="infinite", issue=9426, deprecated_since_version="1.0")
def infinity(self):
"""
See documentation of ``Q.infinite``.
"""
return Predicate('infinite')
@predicate_memo
@deprecated(useinstead="zero", issue=9675, deprecated_since_version="1.0")
def infinitesimal(self):
"""
See documentation of ``Q.zero``.
"""
return Predicate('zero')
@predicate_memo
def positive(self):
r"""
Positive real number predicate.
``Q.positive(x)`` is true iff ``x`` is real and `x > 0`, that is if ``x``
is in the interval `(0, \infty)`. In particular, infinity is not
positive.
A few important facts about positive numbers:
- Note that ``Q.nonpositive`` and ``~Q.positive`` are *not* the same
thing. ``~Q.positive(x)`` simply means that ``x`` is not positive,
whereas ``Q.nonpositive(x)`` means that ``x`` is real and not
positive, i.e., ``Q.nonpositive(x)`` is logically equivalent to
`Q.negative(x) | Q.zero(x)``. So for example, ``~Q.positive(I)`` is
true, whereas ``Q.nonpositive(I)`` is false.
- See the documentation of ``Q.real`` for more information about
related facts.
Examples
========
>>> from sympy import Q, ask, symbols, I
>>> x = symbols('x')
>>> ask(Q.positive(x), Q.real(x) & ~Q.negative(x) & ~Q.zero(x))
True
>>> ask(Q.positive(1))
True
>>> ask(Q.nonpositive(I))
False
>>> ask(~Q.positive(I))
True
"""
return Predicate('positive')
@predicate_memo
def negative(self):
r"""
Negative number predicate.
``Q.negative(x)`` is true iff ``x`` is a real number and :math:`x < 0`, that is,
it is in the interval :math:`(-\infty, 0)`. Note in particular that negative
infinity is not negative.
A few important facts about negative numbers:
- Note that ``Q.nonnegative`` and ``~Q.negative`` are *not* the same
thing. ``~Q.negative(x)`` simply means that ``x`` is not negative,
whereas ``Q.nonnegative(x)`` means that ``x`` is real and not
negative, i.e., ``Q.nonnegative(x)`` is logically equivalent to
``Q.zero(x) | Q.positive(x)``. So for example, ``~Q.negative(I)`` is
true, whereas ``Q.nonnegative(I)`` is false.
- See the documentation of ``Q.real`` for more information about
related facts.
Examples
========
>>> from sympy import Q, ask, symbols, I
>>> x = symbols('x')
>>> ask(Q.negative(x), Q.real(x) & ~Q.positive(x) & ~Q.zero(x))
True
>>> ask(Q.negative(-1))
True
>>> ask(Q.nonnegative(I))
False
>>> ask(~Q.negative(I))
True
"""
return Predicate('negative')
@predicate_memo
def zero(self):
"""
Zero number predicate.
``ask(Q.zero(x))`` is true iff the value of ``x`` is zero.
Examples
========
>>> from sympy import ask, Q, oo, symbols
>>> x, y = symbols('x, y')
>>> ask(Q.zero(0))
True
>>> ask(Q.zero(1/oo))
True
>>> ask(Q.zero(0*oo))
False
>>> ask(Q.zero(1))
False
>>> ask(Q.zero(x*y), Q.zero(x) | Q.zero(y))
True
"""
return Predicate('zero')
@predicate_memo
def nonzero(self):
"""
Nonzero real number predicate.
``ask(Q.nonzero(x))`` is true iff ``x`` is real and ``x`` is not zero. Note in
particular that ``Q.nonzero(x)`` is false if ``x`` is not real. Use
``~Q.zero(x)`` if you want the negation of being zero without any real
assumptions.
A few important facts about nonzero numbers:
- ``Q.nonzero`` is logically equivalent to ``Q.positive | Q.negative``.
- See the documentation of ``Q.real`` for more information about
related facts.
Examples
========
>>> from sympy import Q, ask, symbols, I, oo
>>> x = symbols('x')
>>> print(ask(Q.nonzero(x), ~Q.zero(x)))
None
>>> ask(Q.nonzero(x), Q.positive(x))
True
>>> ask(Q.nonzero(x), Q.zero(x))
False
>>> ask(Q.nonzero(0))
False
>>> ask(Q.nonzero(I))
False
>>> ask(~Q.zero(I))
True
>>> ask(Q.nonzero(oo)) #doctest: +SKIP
False
"""
return Predicate('nonzero')
@predicate_memo
def nonpositive(self):
"""
Nonpositive real number predicate.
``ask(Q.nonpositive(x))`` is true iff ``x`` belongs to the set of
negative numbers including zero.
- Note that ``Q.nonpositive`` and ``~Q.positive`` are *not* the same
thing. ``~Q.positive(x)`` simply means that ``x`` is not positive,
whereas ``Q.nonpositive(x)`` means that ``x`` is real and not
positive, i.e., ``Q.nonpositive(x)`` is logically equivalent to
`Q.negative(x) | Q.zero(x)``. So for example, ``~Q.positive(I)`` is
true, whereas ``Q.nonpositive(I)`` is false.
Examples
========
>>> from sympy import Q, ask, I
>>> ask(Q.nonpositive(-1))
True
>>> ask(Q.nonpositive(0))
True
>>> ask(Q.nonpositive(1))
False
>>> ask(Q.nonpositive(I))
False
>>> ask(Q.nonpositive(-I))
False
"""
return Predicate('nonpositive')
@predicate_memo
def nonnegative(self):
"""
Nonnegative real number predicate.
``ask(Q.nonnegative(x))`` is true iff ``x`` belongs to the set of
positive numbers including zero.
- Note that ``Q.nonnegative`` and ``~Q.negative`` are *not* the same
thing. ``~Q.negative(x)`` simply means that ``x`` is not negative,
whereas ``Q.nonnegative(x)`` means that ``x`` is real and not
negative, i.e., ``Q.nonnegative(x)`` is logically equivalent to
``Q.zero(x) | Q.positive(x)``. So for example, ``~Q.negative(I)`` is
true, whereas ``Q.nonnegative(I)`` is false.
Examples
========
>>> from sympy import Q, ask, I
>>> ask(Q.nonnegative(1))
True
>>> ask(Q.nonnegative(0))
True
>>> ask(Q.nonnegative(-1))
False
>>> ask(Q.nonnegative(I))
False
>>> ask(Q.nonnegative(-I))
False
"""
return Predicate('nonnegative')
@predicate_memo
def even(self):
"""
Even number predicate.
``ask(Q.even(x))`` is true iff ``x`` belongs to the set of even
integers.
Examples
========
>>> from sympy import Q, ask, pi
>>> ask(Q.even(0))
True
>>> ask(Q.even(2))
True
>>> ask(Q.even(3))
False
>>> ask(Q.even(pi))
False
"""
return Predicate('even')
@predicate_memo
def odd(self):
"""
Odd number predicate.
``ask(Q.odd(x))`` is true iff ``x`` belongs to the set of odd numbers.
Examples
========
>>> from sympy import Q, ask, pi
>>> ask(Q.odd(0))
False
>>> ask(Q.odd(2))
False
>>> ask(Q.odd(3))
True
>>> ask(Q.odd(pi))
False
"""
return Predicate('odd')
@predicate_memo
def prime(self):
"""
Prime number predicate.
``ask(Q.prime(x))`` is true iff ``x`` is a natural number greater
than 1 that has no positive divisors other than ``1`` and the
number itself.
Examples
========
>>> from sympy import Q, ask
>>> ask(Q.prime(0))
False
>>> ask(Q.prime(1))
False
>>> ask(Q.prime(2))
True
>>> ask(Q.prime(20))
False
>>> ask(Q.prime(-3))
False
"""
return Predicate('prime')
@predicate_memo
def composite(self):
"""
Composite number predicate.
``ask(Q.composite(x))`` is true iff ``x`` is a positive integer and has
at least one positive divisor other than ``1`` and the number itself.
Examples
========
>>> from sympy import Q, ask
>>> ask(Q.composite(0))
False
>>> ask(Q.composite(1))
False
>>> ask(Q.composite(2))
False
>>> ask(Q.composite(20))
True
"""
return Predicate('composite')
@predicate_memo
def commutative(self):
"""
Commutative predicate.
``ask(Q.commutative(x))`` is true iff ``x`` commutes with any other
object with respect to multiplication operation.
"""
# TODO: Add examples
return Predicate('commutative')
@predicate_memo
def is_true(self):
"""
Generic predicate.
``ask(Q.is_true(x))`` is true iff ``x`` is true. This only makes
sense if ``x`` is a predicate.
Examples
========
>>> from sympy import ask, Q, symbols
>>> x = symbols('x')
>>> ask(Q.is_true(True))
True
"""
return Predicate('is_true')
@predicate_memo
def symmetric(self):
"""
Symmetric matrix predicate.
``Q.symmetric(x)`` is true iff ``x`` is a square matrix and is equal to
its transpose. Every square diagonal matrix is a symmetric matrix.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('Y', 2, 3)
>>> Z = MatrixSymbol('Z', 2, 2)
>>> ask(Q.symmetric(X*Z), Q.symmetric(X) & Q.symmetric(Z))
True
>>> ask(Q.symmetric(X + Z), Q.symmetric(X) & Q.symmetric(Z))
True
>>> ask(Q.symmetric(Y))
False
References
==========
.. [1] https://en.wikipedia.org/wiki/Symmetric_matrix
"""
# TODO: Add handlers to make these keys work with
# actual matrices and add more examples in the docstring.
return Predicate('symmetric')
@predicate_memo
def invertible(self):
"""
Invertible matrix predicate.
``Q.invertible(x)`` is true iff ``x`` is an invertible matrix.
A square matrix is called invertible only if its determinant is 0.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('Y', 2, 3)
>>> Z = MatrixSymbol('Z', 2, 2)
>>> ask(Q.invertible(X*Y), Q.invertible(X))
False
>>> ask(Q.invertible(X*Z), Q.invertible(X) & Q.invertible(Z))
True
>>> ask(Q.invertible(X), Q.fullrank(X) & Q.square(X))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Invertible_matrix
"""
return Predicate('invertible')
@predicate_memo
def orthogonal(self):
"""
Orthogonal matrix predicate.
``Q.orthogonal(x)`` is true iff ``x`` is an orthogonal matrix.
A square matrix ``M`` is an orthogonal matrix if it satisfies
``M^TM = MM^T = I`` where ``M^T`` is the transpose matrix of
``M`` and ``I`` is an identity matrix. Note that an orthogonal
matrix is necessarily invertible.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, Identity
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('Y', 2, 3)
>>> Z = MatrixSymbol('Z', 2, 2)
>>> ask(Q.orthogonal(Y))
False
>>> ask(Q.orthogonal(X*Z*X), Q.orthogonal(X) & Q.orthogonal(Z))
True
>>> ask(Q.orthogonal(Identity(3)))
True
>>> ask(Q.invertible(X), Q.orthogonal(X))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Orthogonal_matrix
"""
return Predicate('orthogonal')
@predicate_memo
def unitary(self):
"""
Unitary matrix predicate.
``Q.unitary(x)`` is true iff ``x`` is a unitary matrix.
Unitary matrix is an analogue to orthogonal matrix. A square
matrix ``M`` with complex elements is unitary if :math:``M^TM = MM^T= I``
where :math:``M^T`` is the conjugate transpose matrix of ``M``.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, Identity
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('Y', 2, 3)
>>> Z = MatrixSymbol('Z', 2, 2)
>>> ask(Q.unitary(Y))
False
>>> ask(Q.unitary(X*Z*X), Q.unitary(X) & Q.unitary(Z))
True
>>> ask(Q.unitary(Identity(3)))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Unitary_matrix
"""
return Predicate('unitary')
@predicate_memo
def positive_definite(self):
r"""
Positive definite matrix predicate.
If ``M`` is a :math:``n \times n`` symmetric real matrix, it is said
to be positive definite if :math:`Z^TMZ` is positive for
every non-zero column vector ``Z`` of ``n`` real numbers.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, Identity
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('Y', 2, 3)
>>> Z = MatrixSymbol('Z', 2, 2)
>>> ask(Q.positive_definite(Y))
False
>>> ask(Q.positive_definite(Identity(3)))
True
>>> ask(Q.positive_definite(X + Z), Q.positive_definite(X) &
... Q.positive_definite(Z))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Positive-definite_matrix
"""
return Predicate('positive_definite')
@predicate_memo
def upper_triangular(self):
"""
Upper triangular matrix predicate.
A matrix ``M`` is called upper triangular matrix if :math:`M_{ij}=0`
for :math:`i<j`.
Examples
========
>>> from sympy import Q, ask, ZeroMatrix, Identity
>>> ask(Q.upper_triangular(Identity(3)))
True
>>> ask(Q.upper_triangular(ZeroMatrix(3, 3)))
True
References
==========
.. [1] http://mathworld.wolfram.com/UpperTriangularMatrix.html
"""
return Predicate('upper_triangular')
@predicate_memo
def lower_triangular(self):
"""
Lower triangular matrix predicate.
A matrix ``M`` is called lower triangular matrix if :math:`a_{ij}=0`
for :math:`i>j`.
Examples
========
>>> from sympy import Q, ask, ZeroMatrix, Identity
>>> ask(Q.lower_triangular(Identity(3)))
True
>>> ask(Q.lower_triangular(ZeroMatrix(3, 3)))
True
References
==========
.. [1] http://mathworld.wolfram.com/LowerTriangularMatrix.html
"""
return Predicate('lower_triangular')
@predicate_memo
def diagonal(self):
"""
Diagonal matrix predicate.
``Q.diagonal(x)`` is true iff ``x`` is a diagonal matrix. A diagonal
matrix is a matrix in which the entries outside the main diagonal
are all zero.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, ZeroMatrix
>>> X = MatrixSymbol('X', 2, 2)
>>> ask(Q.diagonal(ZeroMatrix(3, 3)))
True
>>> ask(Q.diagonal(X), Q.lower_triangular(X) &
... Q.upper_triangular(X))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Diagonal_matrix
"""
return Predicate('diagonal')
@predicate_memo
def fullrank(self):
"""
Fullrank matrix predicate.
``Q.fullrank(x)`` is true iff ``x`` is a full rank matrix.
A matrix is full rank if all rows and columns of the matrix
are linearly independent. A square matrix is full rank iff
its determinant is nonzero.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, ZeroMatrix, Identity
>>> X = MatrixSymbol('X', 2, 2)
>>> ask(Q.fullrank(X.T), Q.fullrank(X))
True
>>> ask(Q.fullrank(ZeroMatrix(3, 3)))
False
>>> ask(Q.fullrank(Identity(3)))
True
"""
return Predicate('fullrank')
@predicate_memo
def square(self):
"""
Square matrix predicate.
``Q.square(x)`` is true iff ``x`` is a square matrix. A square matrix
is a matrix with the same number of rows and columns.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol, ZeroMatrix, Identity
>>> X = MatrixSymbol('X', 2, 2)
>>> Y = MatrixSymbol('X', 2, 3)
>>> ask(Q.square(X))
True
>>> ask(Q.square(Y))
False
>>> ask(Q.square(ZeroMatrix(3, 3)))
True
>>> ask(Q.square(Identity(3)))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Square_matrix
"""
return Predicate('square')
@predicate_memo
def integer_elements(self):
"""
Integer elements matrix predicate.
``Q.integer_elements(x)`` is true iff all the elements of ``x``
are integers.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.integer(X[1, 2]), Q.integer_elements(X))
True
"""
return Predicate('integer_elements')
@predicate_memo
def real_elements(self):
"""
Real elements matrix predicate.
``Q.real_elements(x)`` is true iff all the elements of ``x``
are real numbers.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.real(X[1, 2]), Q.real_elements(X))
True
"""
return Predicate('real_elements')
@predicate_memo
def complex_elements(self):
"""
Complex elements matrix predicate.
``Q.complex_elements(x)`` is true iff all the elements of ``x``
are complex numbers.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.complex(X[1, 2]), Q.complex_elements(X))
True
>>> ask(Q.complex_elements(X), Q.integer_elements(X))
True
"""
return Predicate('complex_elements')
@predicate_memo
def singular(self):
"""
Singular matrix predicate.
A matrix is singular iff the value of its determinant is 0.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.singular(X), Q.invertible(X))
False
>>> ask(Q.singular(X), ~Q.invertible(X))
True
References
==========
.. [1] http://mathworld.wolfram.com/SingularMatrix.html
"""
return Predicate('singular')
@predicate_memo
def normal(self):
"""
Normal matrix predicate.
A matrix is normal if it commutes with its conjugate transpose.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.normal(X), Q.unitary(X))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Normal_matrix
"""
return Predicate('normal')
@predicate_memo
def triangular(self):
"""
Triangular matrix predicate.
``Q.triangular(X)`` is true if ``X`` is one that is either lower
triangular or upper triangular.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.triangular(X), Q.upper_triangular(X))
True
>>> ask(Q.triangular(X), Q.lower_triangular(X))
True
References
==========
.. [1] https://en.wikipedia.org/wiki/Triangular_matrix
"""
return Predicate('triangular')
@predicate_memo
def unit_triangular(self):
"""
Unit triangular matrix predicate.
A unit triangular matrix is a triangular matrix with 1s
on the diagonal.
Examples
========
>>> from sympy import Q, ask, MatrixSymbol
>>> X = MatrixSymbol('X', 4, 4)
>>> ask(Q.triangular(X), Q.unit_triangular(X))
True
"""
return Predicate('unit_triangular')
Q = AssumptionKeys()
def _extract_facts(expr, symbol, check_reversed_rel=True):
"""
Helper for ask().
Extracts the facts relevant to the symbol from an assumption.
Returns None if there is nothing to extract.
"""
if isinstance(symbol, Relational):
if check_reversed_rel:
rev = _extract_facts(expr, symbol.reversed, False)
if rev is not None:
return rev
if isinstance(expr, bool):
return
if not expr.has(symbol):
return
if isinstance(expr, AppliedPredicate):
if expr.arg == symbol:
return expr.func
else:
return
if isinstance(expr, Not) and expr.args[0].func in (And, Or):
cls = Or if expr.args[0] == And else And
expr = cls(*[~arg for arg in expr.args[0].args])
args = [_extract_facts(arg, symbol) for arg in expr.args]
if isinstance(expr, And):
args = [x for x in args if x is not None]
if args:
return expr.func(*args)
if args and all(x != None for x in args):
return expr.func(*args)
[docs]def ask(proposition, assumptions=True, context=global_assumptions):
"""
Method for inferring properties about objects.
**Syntax**
* ask(proposition)
* ask(proposition, assumptions)
where ``proposition`` is any boolean expression
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(x*y), Q.integer(x) & Q.integer(y))
False
**Remarks**
Relations in assumptions are not implemented (yet), so the following
will not give a meaningful result.
>>> ask(Q.positive(x), Q.is_true(x > 0)) # doctest: +SKIP
It is however a work in progress.
"""
from sympy.assumptions.satask import satask
if not isinstance(proposition, (BooleanFunction, AppliedPredicate, bool, BooleanAtom)):
raise TypeError("proposition must be a valid logical expression")
if not isinstance(assumptions, (BooleanFunction, AppliedPredicate, bool, BooleanAtom)):
raise TypeError("assumptions must be a valid logical expression")
if isinstance(proposition, AppliedPredicate):
key, expr = proposition.func, sympify(proposition.arg)
else:
key, expr = Q.is_true, sympify(proposition)
assumptions = And(assumptions, And(*context))
assumptions = to_cnf(assumptions)
local_facts = _extract_facts(assumptions, expr)
known_facts_cnf = get_known_facts_cnf()
known_facts_dict = get_known_facts_dict()
if local_facts and satisfiable(And(local_facts, known_facts_cnf)) is False:
raise ValueError("inconsistent assumptions %s" % assumptions)
# direct resolution method, no logic
res = key(expr)._eval_ask(assumptions)
if res is not None:
return bool(res)
if local_facts is None:
return satask(proposition, assumptions=assumptions, context=context)
# See if there's a straight-forward conclusion we can make for the inference
if local_facts.is_Atom:
if key in known_facts_dict[local_facts]:
return True
if Not(key) in known_facts_dict[local_facts]:
return False
elif (local_facts.func is And and
all(k in known_facts_dict for k in local_facts.args)):
for assum in local_facts.args:
if assum.is_Atom:
if key in known_facts_dict[assum]:
return True
if Not(key) in known_facts_dict[assum]:
return False
elif assum.func is Not and assum.args[0].is_Atom:
if key in known_facts_dict[assum]:
return False
if Not(key) in known_facts_dict[assum]:
return True
elif (isinstance(key, Predicate) and
local_facts.func is Not and local_facts.args[0].is_Atom):
if local_facts.args[0] in known_facts_dict[key]:
return False
# Failing all else, we do a full logical inference
res = ask_full_inference(key, local_facts, known_facts_cnf)
if res is None:
return satask(proposition, assumptions=assumptions, context=context)
return res
[docs]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
[docs]def register_handler(key, handler):
"""
Register a handler in the ask system. key must be a string and handler a
class inheriting from AskHandler::
>>> from sympy.assumptions import register_handler, ask, Q
>>> from sympy.assumptions.handlers import AskHandler
>>> class MersenneHandler(AskHandler):
... # Mersenne numbers are in the form 2**n + 1, n integer
... @staticmethod
... def Integer(expr, assumptions):
... from sympy import log
... return ask(Q.integer(log(expr + 1, 2)))
>>> register_handler('mersenne', MersenneHandler)
>>> ask(Q.mersenne(7))
True
"""
if type(key) is Predicate:
key = key.name
try:
getattr(Q, key).add_handler(handler)
except AttributeError:
setattr(Q, key, Predicate(key, handlers=[handler]))
[docs]def remove_handler(key, handler):
"""Removes a handler from the ask system. Same syntax as register_handler"""
if type(key) is Predicate:
key = key.name
getattr(Q, key).remove_handler(handler)
def single_fact_lookup(known_facts_keys, known_facts_cnf):
# Compute the quick lookup for single facts
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)
return mapping
[docs]def compute_known_facts(known_facts, known_facts_keys):
"""Compute the various forms of knowledge compilation used by the
assumptions system.
This function is typically applied to the results of the ``get_known_facts``
and ``get_known_facts_keys`` functions defined at the bottom of
this file.
"""
from textwrap import dedent, wrap
fact_string = dedent('''\
"""
The contents of this file are the return value of
``sympy.assumptions.ask.compute_known_facts``.
Do NOT manually edit this file.
Instead, run ./bin/ask_update.py.
"""
from sympy.core.cache import cacheit
from sympy.logic.boolalg import And, Not, Or
from sympy.assumptions.ask import Q
# -{ Known facts in Conjunctive Normal Form }-
@cacheit
def get_known_facts_cnf():
return And(
%s
)
# -{ Known facts in compressed sets }-
@cacheit
def get_known_facts_dict():
return {
%s
}
''')
# Compute the known facts in CNF form for logical inference
LINE = ",\n "
HANG = ' '*8
cnf = to_cnf(known_facts)
c = LINE.join([str(a) for a in cnf.args])
mapping = single_fact_lookup(known_facts_keys, cnf)
items = sorted(mapping.items(), key=str)
keys = [str(i[0]) for i in items]
values = ['set(%s)' % sorted(i[1], key=str) for i in items]
m = LINE.join(['\n'.join(
wrap("%s: %s" % (k, v),
subsequent_indent=HANG,
break_long_words=False))
for k, v in zip(keys, values)]) + ','
return fact_string % (c, m)
# handlers tells us what ask handler we should use
# for a particular key
_val_template = 'sympy.assumptions.handlers.%s'
_handlers = [
("antihermitian", "sets.AskAntiHermitianHandler"),
("finite", "calculus.AskFiniteHandler"),
("commutative", "AskCommutativeHandler"),
("complex", "sets.AskComplexHandler"),
("composite", "ntheory.AskCompositeHandler"),
("even", "ntheory.AskEvenHandler"),
("extended_real", "sets.AskExtendedRealHandler"),
("hermitian", "sets.AskHermitianHandler"),
("imaginary", "sets.AskImaginaryHandler"),
("integer", "sets.AskIntegerHandler"),
("irrational", "sets.AskIrrationalHandler"),
("rational", "sets.AskRationalHandler"),
("negative", "order.AskNegativeHandler"),
("nonzero", "order.AskNonZeroHandler"),
("nonpositive", "order.AskNonPositiveHandler"),
("nonnegative", "order.AskNonNegativeHandler"),
("zero", "order.AskZeroHandler"),
("positive", "order.AskPositiveHandler"),
("prime", "ntheory.AskPrimeHandler"),
("real", "sets.AskRealHandler"),
("odd", "ntheory.AskOddHandler"),
("algebraic", "sets.AskAlgebraicHandler"),
("is_true", "common.TautologicalHandler"),
("symmetric", "matrices.AskSymmetricHandler"),
("invertible", "matrices.AskInvertibleHandler"),
("orthogonal", "matrices.AskOrthogonalHandler"),
("unitary", "matrices.AskUnitaryHandler"),
("positive_definite", "matrices.AskPositiveDefiniteHandler"),
("upper_triangular", "matrices.AskUpperTriangularHandler"),
("lower_triangular", "matrices.AskLowerTriangularHandler"),
("diagonal", "matrices.AskDiagonalHandler"),
("fullrank", "matrices.AskFullRankHandler"),
("square", "matrices.AskSquareHandler"),
("integer_elements", "matrices.AskIntegerElementsHandler"),
("real_elements", "matrices.AskRealElementsHandler"),
("complex_elements", "matrices.AskComplexElementsHandler"),
]
for name, value in _handlers:
register_handler(name, _val_template % value)
@cacheit
def get_known_facts_keys():
return [
getattr(Q, attr)
for attr in Q.__class__.__dict__
if not (attr.startswith('__') or
attr in deprecated_predicates)]
@cacheit
def get_known_facts():
return And(
Implies(Q.infinite, ~Q.finite),
Implies(Q.real, Q.complex),
Implies(Q.real, Q.hermitian),
Equivalent(Q.extended_real, Q.real | Q.infinite),
Equivalent(Q.even | Q.odd, Q.integer),
Implies(Q.even, ~Q.odd),
Equivalent(Q.prime, Q.integer & Q.positive & ~Q.composite),
Implies(Q.integer, Q.rational),
Implies(Q.rational, Q.algebraic),
Implies(Q.algebraic, Q.complex),
Equivalent(Q.transcendental | Q.algebraic, Q.complex),
Implies(Q.transcendental, ~Q.algebraic),
Implies(Q.imaginary, Q.complex & ~Q.real),
Implies(Q.imaginary, Q.antihermitian),
Implies(Q.antihermitian, ~Q.hermitian),
Equivalent(Q.irrational | Q.rational, Q.real),
Implies(Q.irrational, ~Q.rational),
Implies(Q.zero, Q.even),
Equivalent(Q.real, Q.negative | Q.zero | Q.positive),
Implies(Q.zero, ~Q.negative & ~Q.positive),
Implies(Q.negative, ~Q.positive),
Equivalent(Q.nonnegative, Q.zero | Q.positive),
Equivalent(Q.nonpositive, Q.zero | Q.negative),
Equivalent(Q.nonzero, Q.negative | Q.positive),
Implies(Q.orthogonal, Q.positive_definite),
Implies(Q.orthogonal, Q.unitary),
Implies(Q.unitary & Q.real, Q.orthogonal),
Implies(Q.unitary, Q.normal),
Implies(Q.unitary, Q.invertible),
Implies(Q.normal, Q.square),
Implies(Q.diagonal, Q.normal),
Implies(Q.positive_definite, Q.invertible),
Implies(Q.diagonal, Q.upper_triangular),
Implies(Q.diagonal, Q.lower_triangular),
Implies(Q.lower_triangular, Q.triangular),
Implies(Q.upper_triangular, Q.triangular),
Implies(Q.triangular, Q.upper_triangular | Q.lower_triangular),
Implies(Q.upper_triangular & Q.lower_triangular, Q.diagonal),
Implies(Q.diagonal, Q.symmetric),
Implies(Q.unit_triangular, Q.triangular),
Implies(Q.invertible, Q.fullrank),
Implies(Q.invertible, Q.square),
Implies(Q.symmetric, Q.square),
Implies(Q.fullrank & Q.square, Q.invertible),
Equivalent(Q.invertible, ~Q.singular),
Implies(Q.integer_elements, Q.real_elements),
Implies(Q.real_elements, Q.complex_elements),
)
from sympy.assumptions.ask_generated import (
get_known_facts_dict, get_known_facts_cnf)
