Module Problem_literals (.ml)

module Problem_literals: sig .. end

checking of problem literals against new context literals

Contains all literals of the problem set (input clause set).

As the same literal may occur in different clauses at the same as well as different positions, it is stored paired with the index of its position. Identical combinations of literals and positions are stored only once.

Checks for each new context literal its unifiability with all problem literals, stores the information (substitution, resolved, subsumed, ...), and calls Context_unifier_search.Search.search_context_unifiers for each clause where the new context literal unifies.

Applies the Resolve and Subsume rule of the model evolution calculus. As this module contains no information about clauses, Resolve is only applied in a restricted - clause independent - way, i.e. as subsumption of the problem literal.

Types

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

Functions

Creation

val create : config ->
       bound ->
       statistic ->
       state ->
       context -> problem_literals

creation of the problem_literals data structure within a given environment.

Registration

Clauses have to register their literals in order to get notified when a relevant literal is added to the context, i.e. a context literal that unifies with one of the clause literals.

val register_literal : problem_literals ->
       literal -> int -> input_partner

register_literal problem_literals literal index retrieves (or implicitly creates) the input_partner representing the problem literal used at the index position in a clause.

val register_input_partner : problem_literals ->
       input_partner ->
       context_unifier_space -> unit

register_input_partner problem_literals input_partner context_unifier_space registers the context_unifier_space as containing the literal input_partner, so that if a context literal unifies with this literal context_unifier_space is searched for new context unifiers.

input_partner must have been previously retrieved with Problem_literals.register_literal.

val unregister_space : problem_literals ->
       context_unifier_space -> unit

undoes the effects of the calls to Problem_literals.register_input_partner with this space. also undoes the effects of Problem_literals.register_input_partner, if it has been only called with input_partners from this space.

Context Unifier Computation

val add : problem_literals ->
       Context.element -> Context_unifier.candidate_type -> unit

add problem_literals context_literal candidate_type checks the new context_literal against all stored problem literals, and calls Context_unifier_search.Search.search_context_unifiers for each match.

Based on candidate_type the computation of assert or split candidates might be deferred until computed with Problem_literals.compute_deferred. Close candidates are always computed. candidate_type must be Close, CloseAssert, or All.

val compute_deferred : problem_literals -> Context_unifier.candidate_type -> unit

compute_deferred problem_literals candidate_type computes all context unifiers with the context based on candidate_type, where candidate_type must be Assert or Split.

to be used in conjunction with Problem_literals.add, most prominently to compute first only CloseAssert and later the previously ignored Split candidates.

val compute_for_element : problem_literals ->
       Context.element -> Context_unifier.candidate_type -> unit

compute_for_element problem_literals context_element candidate_type computes all context unifiers with the context based on candidate_type, where candidate_type must be Assert or Split which are created by context_element. That is, context_element must be used in the context unifier, and no context literal younger than context_element can be used.

Subsumption

val is_space_subsumed : problem_literals ->
       context_unifier_space -> bool

is the given clause subsumed by the context?

Backtracking

val backtrack : problem_literals -> unit

removes all information based on retracted context literals.

DEPENDENCY: Context.backtrack must have been executed before.