# Source code for sympy.assumptions.ask

"""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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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")
[docs] def bounded(self): """ See documentation of Q.finite. """ return Predicate('finite')
@predicate_memo
[docs] 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")
[docs] def infinity(self): """ See documentation of Q.infinite. """ return Predicate('infinite')
@predicate_memo @deprecated(useinstead="zero", issue=9675, deprecated_since_version="1.0")
[docs] def infinitesimal(self): """ See documentation of Q.zero. """ return Predicate('zero')
@predicate_memo
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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
[docs] 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] = set([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