code: def get_relevant_clsfacts(exprs, relevant_facts=None):
      """
      Extract relevant facts from the items in *exprs*. Facts are defined in
      ``assumptions.sathandlers`` module.
  
      This function is recursively called by ``get_all_relevant_facts()``.
  
      Parameters
      ==========
  
      exprs : set
          Expressions whose relevant facts are searched.
  
      relevant_facts : sympy.assumptions.cnf.CNF, optional.
          Pre-discovered relevant facts.
  
      Returns
      =======
  
      exprs : set
          Candidates for next relevant fact searching.
  
      relevant_facts : sympy.assumptions.cnf.CNF
          Updated relevant facts.
  
      Examples
      ========
  
      Here, we will see how facts relevant to ``Abs(x*y)`` are recursively
      extracted. On the first run, set containing the expression is passed
      without pre-discovered relevant facts. The result is a set containing
      candidates for next run, and ``CNF()`` instance containing facts
      which are relevant to ``Abs`` and its argument.
  
      >>> from sympy import Abs
      >>> from sympy.assumptions.satask import get_relevant_clsfacts
      >>> from sympy.abc import x, y
      >>> exprs = {Abs(x*y)}
      >>> exprs, facts = get_relevant_clsfacts(exprs)
      >>> exprs
      {x*y}
      >>> facts.clauses #doctest: +SKIP
      {frozenset({Literal(Q.odd(Abs(x*y)), False), Literal(Q.odd(x*y), True)}),
      frozenset({Literal(Q.zero(Abs(x*y)), False), Literal(Q.zero(x*y), True)}),
      frozenset({Literal(Q.even(Abs(x*y)), False), Literal(Q.even(x*y), True)}),
      frozenset({Literal(Q.zero(Abs(x*y)), True), Literal(Q.zero(x*y), False)}),
      frozenset({Literal(Q.even(Abs(x*y)), False),
                  Literal(Q.odd(Abs(x*y)), False),
                  Literal(Q.odd(x*y), True)}),
      frozenset({Literal(Q.even(Abs(x*y)), False),
                  Literal(Q.even(x*y), True),
                  Literal(Q.odd(Abs(x*y)), False)}),
      frozenset({Literal(Q.positive(Abs(x*y)), False),
                  Literal(Q.zero(Abs(x*y)), False)})}
  
      We pass the first run's results to the second run, and get the expressions
      for next run and updated facts.
  
      >>> exprs, facts = get_relevant_clsfacts(exprs, relevant_facts=facts)
      >>> exprs
      {x, y}
  
      On final run, no more candidate is returned thus we know that all
      relevant facts are successfully retrieved.
  
      >>> exprs, facts = get_relevant_clsfacts(exprs, relevant_facts=facts)
      >>> exprs
      set()
  
      """
      if not relevant_facts:
          relevant_facts = CNF()
  
      newexprs = set()
      for expr in exprs:
          for fact in class_fact_registry(expr):
              newfact = CNF.to_CNF(fact)
              relevant_facts = relevant_facts._and(newfact)
              for key in newfact.all_predicates():
                  if isinstance(key, AppliedPredicate):
                      newexprs |= set(key.arguments)
  
      return newexprs - exprs, relevant_facts
  
file_path: sympy/sympy/assumptions/satask.py
imports: from sympy.core.singleton import S
  from sympy.core.symbol import Symbol
  from sympy.core.kind import NumberKind, UndefinedKind
  from sympy.assumptions.ask_generated import get_all_known_matrix_facts, get_all_known_number_facts
  from sympy.assumptions.assume import global_assumptions, AppliedPredicate
  from sympy.assumptions.sathandlers import class_fact_registry
  from sympy.core import oo
  from sympy.logic.inference import satisfiable
  from sympy.assumptions.cnf import CNF, EncodedCNF
  from sympy.matrices.kind import MatrixKind
label_desc: Use image node_id 5 for calling a global function with example usage: get_relevant_clsfacts(exprs, relevant_facts) and returns: unknown,  relevant_facts