Spaces:
Sleeping
Sleeping
| """ | |
| 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 | |
| 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 | |
| } | |
| 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 | |
| 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 | |
| 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 | |
| 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 | |