Spaces:
Sleeping
Sleeping
File size: 8,391 Bytes
6a86ad5 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 |
"""
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
|