sig
  type t
  and ext = unit
  val eq : Solution.SET.t -> Solution.SET.t -> bool
  val pp : Solution.SET.t Pretty.printer
  val empty : Solution.SET.t
  val is_empty : Solution.SET.t -> bool
  val is_dependent : Solution.SET.t -> Term.t -> bool
  val is_independent : Solution.SET.t -> Term.t -> bool
  val iter : (Fact.Equal.t -> unit) -> Solution.SET.t -> unit
  val fold : (Fact.Equal.t -> 'a -> 'a) -> Solution.SET.t -> 'a -> 'a
  val for_all : (Fact.Equal.t -> bool) -> Solution.SET.t -> bool
  val exists : (Fact.Equal.t -> bool) -> Solution.SET.t -> bool
  val to_list : Solution.SET.t -> Fact.Equal.t list
  val equality : Solution.SET.t -> Term.t -> Fact.Equal.t
  val apply : Solution.SET.t -> Jst.Eqtrans.t
  val find : Solution.SET.t -> Jst.Eqtrans.t
  val inv : Solution.SET.t -> Jst.Eqtrans.t
  val dep : Solution.SET.t -> Term.t -> Term.Var.Set.t
  val ext : Solution.SET.t -> Solution.SET.ext
  module Dep :
    sig
      type eqs = t
      val iter : Solution.DEP.eqs -> (Fact.Equal.t -> unit) -> Term.t -> unit
      val fold :
        Solution.DEP.eqs -> (Fact.Equal.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
      val for_all :
        Solution.DEP.eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
      val exists :
        Solution.DEP.eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
      val choose :
        Solution.DEP.eqs -> (Fact.Equal.t -> bool) -> Term.t -> Fact.Equal.t
    end
  val restrict : Solution.SET.t -> Term.t -> unit
  type config = Partition.t * Solution.SET.t
  val update : Solution.SET.config -> Fact.Equal.t -> unit
  val diff : Solution.SET.t -> Solution.SET.t -> Solution.SET.t
  val copy : Solution.SET.t -> Solution.SET.t
end