sig
val on_add_clause : C.t Logtk.Signal.t
val on_remove_clause : C.t Logtk.Signal.t
val add : C.t Sequence.t -> unit
val remove : C.t Sequence.t -> unit
val clauses : unit -> C.ClauseSet.t
val queue : ProofState_intf.S.CQueue.t
val next : unit -> C.t option
val num_clauses : unit -> int
end