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