sig
module C : Clause.S
module WeightFun :
sig
type t = C.t -> int
val default : ClauseQueue_intf.S.WeightFun.t
val age : ClauseQueue_intf.S.WeightFun.t
val favor_all_neg : ClauseQueue_intf.S.WeightFun.t
val favor_non_all_neg : ClauseQueue_intf.S.WeightFun.t
val favor_ground : ClauseQueue_intf.S.WeightFun.t
val favor_horn : ClauseQueue_intf.S.WeightFun.t
val favor_goal : ClauseQueue_intf.S.WeightFun.t
val combine :
(ClauseQueue_intf.S.WeightFun.t * int) list ->
ClauseQueue_intf.S.WeightFun.t
end
type t
val add : ClauseQueue_intf.S.t -> C.t -> ClauseQueue_intf.S.t
val adds : ClauseQueue_intf.S.t -> C.t Sequence.t -> ClauseQueue_intf.S.t
val is_empty : ClauseQueue_intf.S.t -> bool
val take_first : ClauseQueue_intf.S.t -> ClauseQueue_intf.S.t * C.t
val name : ClauseQueue_intf.S.t -> string
val make : weight:(C.t -> int) -> string -> ClauseQueue_intf.S.t
val bfs : ClauseQueue_intf.S.t
val explore : ClauseQueue_intf.S.t
val ground : ClauseQueue_intf.S.t
val goal_oriented : ClauseQueue_intf.S.t
val default : ClauseQueue_intf.S.t
val of_profile : ClauseQueue_intf.profile -> ClauseQueue_intf.S.t
val pp : ClauseQueue_intf.S.t CCFormat.printer
val to_string : ClauseQueue_intf.S.t -> string
end