+ val index_unit_clause :
+ DT.t -> B.t Terms.unit_clause -> DT.t
+
+ val remove_unit_clause :
+ DT.t -> B.t Terms.unit_clause -> DT.t
+
+ val fold :
+ DT.t ->
+ (B.t Discrimination_tree.path -> ClauseSet.t -> 'a -> 'a)
+ -> 'a -> 'a
+
+ val elems : DT.t -> ClauseSet.t
+
+ type active_set = B.t Terms.unit_clause list * DT.t