sig
  type config = Partition.t * Solution.Set.t
  module type T =
    sig
      val th : Th.t
      val map : (Term.t -> Term.t) -> Term.t -> Term.t
      val sigma : Sym.t -> Term.t list -> Term.t
      val of_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
      val of_var_equal : Fact.Equal.t -> Can.config -> Fact.Equal.t list
      val of_var_diseq : Fact.Diseq.t -> Can.config -> Fact.Equal.t list
      val disjunction : Can.config -> Clause.t
    end
  module Make :
    functor (Can : 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
  module type OPS =
    sig
      val is_flat : Term.t -> bool
      val is_pure : Term.t -> bool
      val find : Partition.t * Solution.Set.t -> Jst.Eqtrans.t
      val inv : Partition.t * Solution.Set.t -> Jst.Eqtrans.t
    end
  module Ops : functor (Can : T) -> OPS
end