sig
type config = Config.config
type bound = Bound.bound
type statistic = Statistic.statistic
type literal = Term.literal
type subst = Subst.subst
type choice_point = State.choice_point
type state = State.state
type context = Context.context
type context_partner = Context_unifier.context_partner
type input_partner = Context_unifier.input_partner
type context_unifier_space = Context_unifier.context_unifier_space
type problem_literals
val create :
Problem_literals.config ->
Problem_literals.bound ->
Problem_literals.statistic ->
Problem_literals.state ->
Problem_literals.context -> Problem_literals.problem_literals
val register_literal :
Problem_literals.problem_literals ->
Problem_literals.literal -> int -> Problem_literals.input_partner
val register_input_partner :
Problem_literals.problem_literals ->
Problem_literals.input_partner ->
Problem_literals.context_unifier_space -> unit
val unregister_space :
Problem_literals.problem_literals ->
Problem_literals.context_unifier_space -> unit
val add :
Problem_literals.problem_literals ->
Context.element -> Context_unifier.candidate_type -> unit
val compute_deferred :
Problem_literals.problem_literals ->
Context_unifier.candidate_type -> unit
val compute_for_element :
Problem_literals.problem_literals ->
Context.element -> Context_unifier.candidate_type -> unit
val is_space_subsumed :
Problem_literals.problem_literals ->
Problem_literals.context_unifier_space -> bool
val backtrack : Problem_literals.problem_literals -> unit
end