functor (Sh : T) ->
  sig
    type e = Solution.Set.t
    val current : unit -> e
    val initialize : e -> unit
    val finalize : unit -> e
    val abstract : Term.t -> unit
    val merge : Fact.Equal.t -> unit
    val propagate : Fact.Equal.t -> unit
    val dismerge : Fact.Diseq.t -> unit
    val propagate_diseq : Fact.Diseq.t -> unit
    val branch : unit -> unit
    val normalize : unit -> unit
  end