sig
  type t = Logtk.Literal.t array -> CCBV.t
  type parametrized = strict:bool -> ord:Logtk.Ordering.t -> Selection.t
  val no_select : Selection.t
  val max_goal : Selection.parametrized
  val except_RR_horn : Selection.parametrized -> Selection.parametrized
  val default : ord:Logtk.Ordering.t -> Selection.t
  val from_string : ord:Logtk.Ordering.t -> string -> Selection.t
  val all : unit -> string list
end