sig
  module Make :
    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
end