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