sig
  type profile = ClauseQueue_intf.profile
  val profile_of_string : string -> ClauseQueue.profile
  val get_profile : unit -> ClauseQueue.profile
  val set_profile : ClauseQueue.profile -> unit
  module type S = ClauseQueue_intf.S
  module Make :
    functor (C : Clause.S->
      sig
        module C :
          sig
            module Ctx :
              sig
                val ord : unit -> Logtk.Ordering.t
                val selection_fun : unit -> Selection.t
                val set_selection_fun : Selection.t -> unit
                val set_ord : Logtk.Ordering.t -> unit
                val signature : unit -> Logtk.Signature.t
                val renaming : Logtk.Subst.Renaming.t
                val compare :
                  Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
                val select : Selection.t
                val lost_completeness : unit -> unit
                val is_completeness_preserved : unit -> bool
                val add_signature : Logtk.Signature.t -> unit
                val find_signature : Logtk.ID.t -> Logtk.Type.t option
                val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
                val declare : Logtk.ID.t -> Logtk.Type.t -> unit
                val on_new_symbol :
                  (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
                val on_signature_update : Logtk.Signature.t Logtk.Signal.t
                module Lit :
                  sig
                    val from_hooks :
                      unit -> Logtk.Literal.Conv.hook_from list
                    val add_from_hook : Logtk.Literal.Conv.hook_from -> unit
                    val to_hooks : unit -> Logtk.Literal.Conv.hook_to list
                    val add_to_hook : Logtk.Literal.Conv.hook_to -> unit
                    val of_form :
                      Logtk.Term.t Logtk.SLiteral.t -> Logtk.Literal.t
                    val to_form :
                      Logtk.Literal.t -> Logtk.Term.t Logtk.SLiteral.t
                  end
              end
            type t = C.t
            type clause = t
            type flag = SClause.flag
            val set_flag : flag -> t -> bool -> unit
            val get_flag : flag -> t -> bool
            val mark_redundant : t -> unit
            val is_redundant : t -> bool
            val mark_backward_simplified : t -> unit
            val is_backward_simplified : t -> bool
            val equal : t -> t -> bool
            val hash : t -> int
            val compare : t -> t -> int
            val id : t -> int
            val lits : t -> Logtk.Literal.t array
            val is_ground : t -> bool
            val weight : t -> int
            module Tbl :
              sig
                type key = t
                type 'a t = 'C.Tbl.t
                val create : int -> 'a t
                val clear : 'a t -> unit
                val reset : 'a t -> unit
                val copy : 'a t -> 'a t
                val add : 'a t -> key -> '-> unit
                val remove : 'a t -> key -> unit
                val find : 'a t -> key -> 'a
                val find_all : 'a t -> key -> 'a list
                val replace : 'a t -> key -> '-> unit
                val mem : 'a t -> key -> bool
                val iter : (key -> '-> unit) -> 'a t -> unit
                val filter_map_inplace :
                  (key -> '-> 'a option) -> 'a t -> unit
                val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
                val length : 'a t -> int
                val stats : 'a t -> Hashtbl.statistics
                val get : 'a t -> key -> 'a option
                val get_or : 'a t -> key -> default:'-> 'a
                val add_list : 'a list t -> key -> '-> unit
                val incr : ?by:int -> int t -> key -> unit
                val decr : ?by:int -> int t -> key -> unit
                val keys : 'a t -> key CCHashtbl.sequence
                val values : 'a t -> 'CCHashtbl.sequence
                val keys_list : 'a t -> key list
                val values_list : 'a t -> 'a list
                val map_list : (key -> '-> 'b) -> 'a t -> 'b list
                val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
                val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
                val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
                val add_seq_count : int t -> key CCHashtbl.sequence -> unit
                val of_seq_count : key CCHashtbl.sequence -> int t
                val to_list : 'a t -> (key * 'a) list
                val of_list : (key * 'a) list -> 'a t
                val update :
                  'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
                val get_or_add : 'a t -> f:(key -> 'a) -> k:key -> 'a
                val print :
                  key CCHashtbl.printer ->
                  'CCHashtbl.printer -> 'a t CCHashtbl.printer
              end
            val is_goal : t -> bool
            val distance_to_goal : t -> int option
            val comes_from_goal : t -> bool
            val pp_trail : Trail.t CCFormat.printer
            val has_trail : t -> bool
            val trail : t -> Trail.t
            val trail_l : t list -> Trail.t
            val update_trail : (Trail.t -> Trail.t) -> t -> t
            val trail_subsumes : t -> t -> bool
            val is_active : t -> v:Trail.valuation -> bool
            val create :
              penalty:int ->
              trail:Trail.t ->
              Logtk.Literal.t list -> Clause_intf.proof_step -> t
            val create_a :
              penalty:int ->
              trail:Trail.t ->
              Logtk.Literal.t array -> Clause_intf.proof_step -> t
            val of_sclause :
              ?penalty:int -> SClause.t -> Clause_intf.proof_step -> t
            val of_forms :
              ?penalty:int ->
              trail:Trail.t ->
              Logtk.Term.t Logtk.SLiteral.t list ->
              Clause_intf.proof_step -> t
            val of_forms_axiom :
              ?penalty:int ->
              file:string ->
              name:string -> Logtk.Term.t Logtk.SLiteral.t list -> t
            val of_statement : Logtk.Statement.clause_t -> t list
            val proof_step : t -> Clause_intf.proof_step
            val proof : t -> Clause_intf.proof
            val proof_parent : t -> Logtk.Proof.Parent.t
            val proof_parent_subst :
              Logtk.Subst.Renaming.t ->
              t Logtk.Scoped.t -> Logtk.Subst.t -> Logtk.Proof.Parent.t
            val update_proof :
              t -> (Clause_intf.proof_step -> Clause_intf.proof_step) -> t
            val is_empty : t -> bool
            val length : t -> int
            val maxlits : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val is_maxlit :
              t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
            val eligible_res : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val eligible_res_no_subst : t -> CCBV.t
            val eligible_param : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val is_eligible_param :
              t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
            val has_selected_lits : t -> bool
            val is_selected : t -> int -> bool
            val selected_lits : t -> (Logtk.Literal.t * int) list
            val penalty : t -> int
            val is_unit_clause : t -> bool
            val is_oriented_rule : t -> bool
            val symbols :
              ?init:Logtk.ID.Set.t -> t Sequence.t -> Logtk.ID.Set.t
            val to_sclause : t -> SClause.t
            val to_forms : t -> Logtk.Term.t Logtk.SLiteral.t list
            val to_s_form : t -> Logtk.TypedSTerm.Form.t
            module Seq :
              sig
                val lits : t -> Logtk.Literal.t Sequence.t
                val terms : t -> Logtk.Term.t Sequence.t
                val vars : t -> Logtk.Type.t Logtk.HVar.t Sequence.t
              end
            module Eligible :
              sig
                type t = int -> Logtk.Literal.t -> bool
                val res : clause -> t
                val param : clause -> t
                val eq : t
                val arith : t
                val filter : (Logtk.Literal.t -> bool) -> t
                val max : clause -> t
                val pos : t
                val neg : t
                val always : t
                val combine : t list -> t
                val ( ** ) : t -> t -> t
                val ( ++ ) : t -> t -> t
                val ( ~~ ) : t -> t
              end
            module ClauseSet :
              sig
                type elt = t
                type t = C.ClauseSet.t
                val empty : t
                val is_empty : t -> bool
                val mem : elt -> t -> bool
                val add : elt -> t -> t
                val singleton : elt -> t
                val remove : elt -> t -> t
                val union : t -> t -> t
                val inter : t -> t -> t
                val diff : t -> t -> t
                val compare : t -> t -> int
                val equal : t -> t -> bool
                val subset : t -> t -> bool
                val iter : (elt -> unit) -> t -> unit
                val map : (elt -> elt) -> t -> t
                val fold : (elt -> '-> 'a) -> t -> '-> 'a
                val for_all : (elt -> bool) -> t -> bool
                val exists : (elt -> bool) -> t -> bool
                val filter : (elt -> bool) -> t -> t
                val partition : (elt -> bool) -> t -> t * t
                val cardinal : t -> int
                val elements : t -> elt list
                val min_elt : t -> elt
                val max_elt : t -> elt
                val choose : t -> elt
                val split : elt -> t -> t * bool * t
                val find : elt -> t -> elt
                val of_seq : elt CCSet.sequence -> t
                val add_seq : t -> elt CCSet.sequence -> t
                val to_seq : t -> elt CCSet.sequence
                val of_list : elt list -> t
                val add_list : t -> elt list -> t
                val to_list : t -> elt list
                val pp :
                  ?start:string ->
                  ?stop:string ->
                  ?sep:string -> elt CCSet.printer -> t CCSet.printer
              end
            module Pos :
              sig val at : t -> Logtk.Position.t -> Logtk.Term.t end
            module WithPos :
              sig
                type t =
                  C.WithPos.t = {
                  clause : clause;
                  pos : Logtk.Position.t;
                  term : Logtk.Term.t;
                }
                val compare : t -> t -> int
                val pp : t CCFormat.printer
              end
            val pp : t CCFormat.printer
            val pp_tstp : t CCFormat.printer
            val pp_tstp_full : t CCFormat.printer
            val to_string : t -> string
            val pp_set : ClauseSet.t CCFormat.printer
            val pp_set_tstp : ClauseSet.t CCFormat.printer
          end
        module WeightFun :
          sig
            type t = C.t -> int
            val default : t
            val penalty : t
            val favor_all_neg : t
            val favor_non_all_neg : t
            val favor_ground : t
            val favor_horn : t
            val favor_goal : t
            val combine : (t * int) list -> t
          end
        type t
        val add : t -> C.t -> unit
        val add_seq : t -> C.t Sequence.t -> unit
        val length : t -> int
        val is_empty : t -> bool
        val take_first : t -> C.t
        val name : t -> string
        val make : ratio:int -> weight:(C.t -> int) -> string -> t
        val bfs : unit -> t
        val almost_bfs : unit -> t
        val explore : unit -> t
        val ground : unit -> t
        val goal_oriented : unit -> t
        val default : unit -> t
        val of_profile : ClauseQueue_intf.profile -> t
        val pp : t CCFormat.printer
        val to_string : t -> string
      end
end