sig
  type config = Config.config
  type literal = Term.literal
  type clause = Term.clause
  type subst = Subst.subst
  type choice_point
  type explanation = State.choice_point list
  type literal_type = Propagation | SplitLeft | SplitRight
  type literal_info = private {
    li_literal : State.literal;
    li_type : State.literal_type;
    li_choice_point : State.choice_point;
    li_context_unifier : State.subst;
    li_clause : State.clause;
    li_clause_vars : Subst.var list;
    li_context_literals : State.literal array;
    li_clause_index : int;
    li_clause_utility : unit -> unit;
    mutable li_explanation : State.explanation option;
  }
  type state
  val valid_choice_point : State.choice_point
  val invalid_choice_point : State.choice_point
  val create_literal_info :
    State.literal ->
    State.literal_type ->
    State.choice_point ->
    State.subst ->
    State.clause ->
    Subst.var list ->
    State.literal array ->
    int -> (unit -> unit) -> State.explanation option -> State.literal_info
  val root_choice_point : State.state -> State.choice_point
  val active_choice_point : State.state -> State.choice_point
  val left_split_literal : State.choice_point -> State.literal
  val right_split_literals : State.choice_point -> State.literal list
  val get_branch : State.state -> State.choice_point list
  val get_literal_info : State.state -> State.literal -> State.literal_info
  val create : State.config -> State.state
  val apply_split_left :
    State.state ->
    State.literal ->
    State.subst ->
    State.clause ->
    Subst.var list -> int -> (unit -> unit) -> State.choice_point
  val apply_split_right :
    State.state ->
    State.literal ->
    State.subst ->
    State.clause ->
    Subst.var list -> int -> (unit -> unit) -> State.literal array -> unit
  val apply_propagation :
    State.state ->
    State.literal ->
    State.subst ->
    State.clause ->
    Subst.var list -> int -> (unit -> unit) -> State.literal array -> unit
  val invalidate_choice_point : State.choice_point -> unit
  val set_branch : State.state -> State.choice_point list -> unit
  val backtrack_literal_info : State.state -> unit
  val id_of_choice_point : State.choice_point -> int
  val is_choice_point_valid : State.choice_point -> bool
  val is_choice_point_invalid : State.choice_point -> bool
  val get_explanation :
    State.state -> State.literal array -> State.choice_point list
  val choice_point_equal : State.choice_point -> State.choice_point -> bool
  val compare_age : State.choice_point -> State.choice_point -> int
  val backtracking_depends_on :
    State.choice_point -> State.choice_point -> bool
  val choice_point_to_string : State.choice_point -> string
  val explanation_to_string : State.explanation -> string
  val id_to_string : int -> string
  val active_choice_point_to_string : State.state -> string
  val branch_to_string : State.state -> string
end