sig
val cc_active : bool Pervasives.ref
module type S =
sig
type t
module TimerCC : Timer.S
val empty : unit -> Cc.S.t
val assume :
cs:bool ->
Literal.LT.t -> Explanation.t -> Cc.S.t -> Cc.S.t * Term.Set.t * int
val query : Literal.LT.t -> Cc.S.t -> Sig.answer
val class_of : Cc.S.t -> Term.t -> Term.t list
end
module Make : functor (X : Sig.X) -> S
end