Coverage for sympy/assumptions/satask.py : 21%

from __future__ import print_function, division 

from sympy.core import oo, Tuple 

from sympy.assumptions.assume import global_assumptions, AppliedPredicate 

from sympy.logic.inference import satisfiable 

from sympy.logic.boolalg import And 

from sympy.assumptions.ask_generated import get_known_facts_cnf 

from sympy.assumptions.sathandlers import fact_registry 

def satask(proposition, assumptions=True, context=global_assumptions, 

use_known_facts=True, iterations=oo): 

relevant_facts = get_all_relevant_facts(proposition, assumptions, context, 

use_known_facts=use_known_facts, iterations=iterations) 

can_be_true = satisfiable(And(proposition, assumptions, 

relevant_facts, *context)) 

can_be_false = satisfiable(And(~proposition, assumptions, 

relevant_facts, *context)) 

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: 

# TODO: Run additional checks to see which combination of the 

# assumptions, global_assumptions, and relevant_facts are 

# inconsistent. 

raise ValueError("Inconsistent assumptions") 

def get_relevant_facts(proposition, assumptions=(True,), 

context=global_assumptions, use_known_facts=True, exprs=None, 

relevant_facts=None): 

newexprs = set() 

if not exprs: 

keys = proposition.atoms(AppliedPredicate) 

# XXX: We need this since True/False are not Basic 

keys |= Tuple(*assumptions).atoms(AppliedPredicate) 

if context: 

keys |= And(*context).atoms(AppliedPredicate) 

exprs = {key.args[0] for key in keys} 

if not relevant_facts: 

relevant_facts = set([]) 

if use_known_facts: 

for expr in exprs: 

relevant_facts.add(get_known_facts_cnf().rcall(expr)) 

for expr in exprs: 

for fact in fact_registry[expr.func]: 

newfact = fact.rcall(expr) 

relevant_facts.add(newfact) 

newexprs |= set([key.args[0] for key in 

newfact.atoms(AppliedPredicate)]) 

return relevant_facts, newexprs - exprs 

def get_all_relevant_facts(proposition, assumptions=True, 

context=global_assumptions, use_known_facts=True, iterations=oo): 

# The relevant facts might introduce new keys, e.g., Q.zero(x*y) will 

# introduce the keys Q.zero(x) and Q.zero(y), so we need to run it until 

# we stop getting new things. Hopefully this strategy won't lead to an 

# infinite loop in the future. 

i = 0 

relevant_facts = set() 

exprs = None 

while exprs != set(): 

(relevant_facts, exprs) = get_relevant_facts(proposition, 

And.make_args(assumptions), context, 

use_known_facts=use_known_facts, exprs=exprs, 

relevant_facts=relevant_facts) 

i += 1 

if i >= iterations: 

return And(*relevant_facts) 

return And(*relevant_facts)