sig
  type config = Config.config
  type bound = Bound.bound
  type statistic = Statistic.statistic
  type literal = Term.literal
  type clause = Term.clause
  type choice_point = State.choice_point
  type state = State.state
  type selected = Selection_types.selected
  type context = Context.context
  type guiding_path = Jumping.guiding_path
  type selection
  exception SATISFIABLE
  val create :
    Selection.config ->
    Selection.bound ->
    Selection.statistic ->
    Selection.state ->
    Selection.context ->
    Selection.clause list ->
    Selection.clause list ->
    Selection.literal list -> Selection.guiding_path -> Selection.selection
  val add_lemma : Selection.selection -> Selection.clause -> unit
  val add : Selection.selection -> Context.element -> unit
  val select : Selection.selection -> Selection.selected
  val get_lemmas : Selection.selection -> Selection.clause list
  val in_replay : Selection.selection -> bool
  val backtrack :
    Selection.selection ->
    Selection.choice_point -> Selection.literal list -> unit
end