def get_rule_unifiers(rule_a, rule_b, config):
  """Returns `rule_c` that can be combined with `rule_b` to equal `rule_a`.

  Here we interpret rules as functions over strings, with arity equal to the
  number of uniquely indexed non-terminals.
  Our task can be viewed as a restricted form of higher-order unification.
  We are looking for a function `c` that can be applied to an argument of `b`
  that `unifies` `b` and `a`, or vice versa.

  For example, if `a` has arity 2 and `b` has arity 2, we are looking for `c`
  such that one of the following holds:
    - a(x, y) = b(c(x), y)
    - a(x, y) = b(x, c(y))
    - a(x, y) = c(b(x, y))

  More concretely, consider the following rules:
    - `rule_a` is `foo bar ### FOO BAR`
    - `rule_b` is `foo NT_1 ### FOO NT_1`
    - The function should return {`bar ### BAR`}.

  Args:
    rule_a: QCFGRule.
    rule_b: QCFGRule.
    config: Config dict.

  Returns:
    Set of QCFGRule candidates for `rule_c`.
  """
  candidates = set()

  # First, consider applying `c` to an argument of `b`.
  # For example:
  # `a` could be `foo bar ### FOO BAR`
  # `b` could be `foo NT_1 ### FOO NT_1`
  # `c` could be `bar ### BAR`
  # Therefore, our strategy is to find some substitution for the non-terminals
  # in `b` that matches `a`.
  candidates_c_b = _get_candidates_c_b(rule_a, rule_b, config)
  candidates |= candidates_c_b

  # Second, consider applying `b` to an argument of `c`.
  # For example:
  # `a` could be `foo bar ### FOO BAR`
  # `b` could be `bar ### BAR`
  # `c` could be `foo NT_1 ### FOO NT_1`
  candidates_b_c = _get_candidates_b_c(rule_a, rule_b, config)
  candidates |= candidates_b_c

  return candidates
Returns `rule_c` that can be combined with `rule_b` to equal `rule_a`.

  Here we interpret rules as functions over strings, with arity equal to the
  number of uniquely indexed non-terminals.
  Our task can be viewed as a restricted form of higher-order unification.
  We are looking for a function `c` that can be applied to an argument of `b`
  that `unifies` `b` and `a`, or vice versa.

  For example, if `a` has arity 2 and `b` has arity 2, we are looking for `c`
  such that one of the following holds:
    - a(x, y) = b(c(x), y)
    - a(x, y) = b(x, c(y))
    - a(x, y) = c(b(x, y))

  More concretely, consider the following rules:
    - `rule_a` is `foo bar ### FOO BAR`
    - `rule_b` is `foo NT_1 ### FOO NT_1`
    - The function should return {`bar ### BAR`}.

  Args:
    rule_a: QCFGRule.
    rule_b: QCFGRule.
    config: Config dict.

  Returns:
    Set of QCFGRule candidates for `rule_c`.
  
language/compgen/csl/induction/unification_utils.py