functor (Q : Common.QUEUE) ->
  sig
    val equiv :
      ?tracer:([ `CE | `OK | `Skip ] -> 's -> 's -> unit) ->
      ('s, 'k) Bdd.unifier ->
      ('s, 'v, 'k, 'o) Automata.sdfa ->
      's -> 's -> ('s * 's * ('v, 'k) Common.gstring_) option
    val equiv_c :
      ?tracer:([ `CE | `OK | `Skip ] ->
               Common.int_set -> Common.int_set -> unit) ->
      (Common.int_set, 'k) Bdd.unifier ->
      (Common.int_set, 'v, 'k, 'o) Automata.sdfa ->
      Common.int_set ->
      Common.int_set ->
      (Common.int_set * Common.int_set * ('v, 'k) Common.gstring_) option
  end