def ask(proposition, assumptions=True, context=global_assumptions):
 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))
 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)
 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
 res = ask_full_inference(key, local_facts, known_facts_cnf)
 if (res is None):
  return satask(proposition, assumptions=assumptions, context=context)
 return res

def ask ( proposition , assumptions = True , context = global_assumptions ) : 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 ) ) 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 ) 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 res = ask_full_inference ( key , local_facts , known_facts_cnf ) if ( res is None ) : return satask ( proposition , assumptions = assumptions , context = context ) return res
display the enhancement to the user .