Function bfs_one_level

dd.py:1008–1123

Forward deduce one breadth-first level.

(
    g: gh.Graph,
    theorems: list[pr.Theorem],
    level: int,
    controller: pr.Problem,
    verbose: bool = False,
    nm_check: bool = False,
    timeout: int = 600,
)

def bfs_one_level(
    g: gh.Graph,
    theorems: list[pr.Theorem],
    level: int,
    controller: pr.Problem,
    verbose: bool = False,
    nm_check: bool = False,
    timeout: int = 600,
) -> tuple[
    list[pr.Dependency],
    dict[str, list[tuple[gm.Point, ...]]],
    dict[str, list[tuple[gm.Point, ...]]],
    int,
]:
  """Forward deduce one breadth-first level."""

  # Step 1: match all theorems:
  theorem2mappings = match_all_theorems(g, theorems, controller.goal)

  # Step 2: traceback for each deduce:
  theorem2deps = {}
  t0 = time.time()
  for theorem, mappings in theorem2mappings.items():
    if time.time() - t0 > timeout:
      break
    mp_deps = []
    for mp in mappings:
      deps = EmptyDependency(level=level, rule_name=theorem.rule_name)
      fail = False  # finding why deps might fail.

      for p in theorem.premise:
        p_args = [mp[a] for a in p.args]
        # Trivial deps.
        if p.name == 'cong':
          a, b, c, d = p_args
          if {a, b} == {c, d}:
            continue
        if p.name == 'para':
          a, b, c, d = p_args
          if {a, b} == {c, d}:
            continue

        if theorem.name in [
            'cong_cong_eqangle6_ncoll_contri*',
            'eqratio6_eqangle6_ncoll_simtri*',
        ]:
          if p.name in ['eqangle', 'eqangle6']:  # SAS or RAR
            b, a, b, c, y, x, y, z = (  # pylint: disable=redeclared-assigned-name,unused-variable
                p_args
            )
            if not nm.same_clock(a.num, b.num, c.num, x.num, y.num, z.num):
              p_args = b, a, b, c, y, z, y, x

        dep = Dependency(p.name, p_args, rule_name='', level=level)
        try:
          dep = dep.why_me_or_cache(g, level)
        except:  # pylint: disable=bare-except
          fail = True