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