Function match_all_theorems

dd.py:978–1005

Match all instances of all theorems (rules).

(
    g: gh.Graph, theorems: list[pr.Theorem], goal: pr.Clause
)

def match_all_theorems(
    g: gh.Graph, theorems: list[pr.Theorem], goal: pr.Clause
) -> dict[pr.Theorem, dict[pr.Theorem, dict[str, gm.Point]]]:
  """Match all instances of all theorems (rules)."""
  cache = cache_match(g)
  # for BFS, collect all potential matches
  # and then do it at the same time
  theorem2mappings = {}

  # Step 1: list all matches
  for _, theorem in theorems.items():
    name = theorem.name
    if name.split('_')[-1] in [
        'acompute',
        'rcompute',
        'fixl',
        'fixc',
        'fixb',
        'fixt',
        'fixp',
    ]:
      if goal and goal.name != name:
        continue

    mappings = match_one_theorem(g, cache, theorem)
    if len(mappings):  # pylint: disable=g-explicit-length-test
      theorem2mappings[theorem] = list(mappings)
  return theorem2mappings


def bfs_one_level(