SatContainer.Make
exception Sat of t
exception Unsat of Explanation.t
exception I_dont_know of t
val empty : unit -> t
val assume : t -> Expr.gformula -> Explanation.t -> t
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t
val unsat : t -> Expr.gformula -> Explanation.t
val print_model : header:bool -> Stdlib.Format.formatter -> t -> unit