sig
  type t
  type exp
  val empty : Explanation.t
  val singleton : Solver_types.atom -> Explanation.t
  val union : Explanation.t -> Explanation.t -> Explanation.t
  val merge : Explanation.t -> Explanation.t -> Explanation.t
  val iter_atoms : (Solver_types.atom -> unit) -> Explanation.t -> unit
  val fold_atoms :
    (Solver_types.atom -> 'a -> 'a) -> Explanation.t -> 'a -> 'a
  val fresh_exp : unit -> int
  val remove_fresh : int -> Explanation.t -> Explanation.t option
  val add_fresh : int -> Explanation.t -> Explanation.t
  val print : Format.formatter -> Explanation.t -> unit
end