sig
  type config = Config.config
  type choice_point = State.choice_point
  type bound = Bound.bound
  type statistic = Statistic.statistic
  type literal = Term.literal
  type state = State.state
  type raw_context_unifier = Context_unifier.raw_context_unifier
  type problem_literals = Problem_literals.problem_literals
  type space_registry = Context_unifier_space.space_registry
  type selected = Selection_types.selected
  type context = Context.context
  type candidates
  val create :
    Selection_split.config ->
    Selection_split.bound ->
    Selection_split.statistic ->
    Selection_split.state ->
    Selection_split.context ->
    Selection_split.problem_literals ->
    Selection_split.space_registry -> Selection_split.candidates
  val size : Selection_split.candidates -> int
  val add :
    Selection_split.candidates -> Selection_split.raw_context_unifier -> unit
  val select :
    Selection_split.candidates ->
    Jumping.guiding_step option -> Selection_split.selected option
  val select_right_split :
    Selection_split.candidates -> Selection_split.selected option
  val check_exceeding : Selection_split.candidates -> unit
  val is_element_incomplete :
    Selection_split.candidates -> Context.element -> bool
  val remainder_literals_to_string :
    Selection_split.config ->
    Selection_split.context -> Selection_split.raw_context_unifier -> string
  val backtrack :
    Selection_split.candidates ->
    Selection_split.choice_point -> Selection_split.literal list -> unit
end