sig
  type t = Logtk.Literal.t array -> CCBV.t
  val no_select : Selection.t
  val select_max_goal : strict:bool -> ord:Logtk.Ordering.t -> Selection.t
  val select_diff_neg_lit :
    strict:bool -> ord:Logtk.Ordering.t -> Selection.t
  val select_complex : strict:bool -> ord:Logtk.Ordering.t -> Selection.t
  val select_complex_except_RR_horn :
    strict:bool -> ord:Logtk.Ordering.t -> Selection.t
  val default_selection : ord:Logtk.Ordering.t -> Selection.t
  val selection_from_string : ord:Logtk.Ordering.t -> string -> Selection.t
  val available_selections : unit -> string list
  val register : string -> (ord:Logtk.Ordering.t -> Selection.t) -> unit
end