sig
module C : Clause_intf.S
module WeightFun :
sig
type t = C.t -> int
val default : ClauseQueue_intf.S.WeightFun.t
val penalty : 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 -> unit
val add_seq : ClauseQueue_intf.S.t -> C.t Sequence.t -> unit
val length : ClauseQueue_intf.S.t -> int
val is_empty : ClauseQueue_intf.S.t -> bool
val take_first : ClauseQueue_intf.S.t -> C.t
val name : ClauseQueue_intf.S.t -> string
val make :
ratio:int -> weight:(C.t -> int) -> string -> ClauseQueue_intf.S.t
val bfs : unit -> ClauseQueue_intf.S.t
val almost_bfs : unit -> ClauseQueue_intf.S.t
val explore : unit -> ClauseQueue_intf.S.t
val ground : unit -> ClauseQueue_intf.S.t
val goal_oriented : unit -> ClauseQueue_intf.S.t
val default : unit -> 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