sig
  module type T =
    sig
      val th : Th.t
      val map : (Term.t -> Term.t) -> Term.t -> Term.t
      val solve : Fact.Equal.t -> Fact.Equal.t list
      val disjunction : Fact.Equal.t -> Clause.t
    end
  module Make :
    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
end