Module Context_unifier_space (.ml)

module Context_unifier_space: sig .. end

a problem clause

Stores a clause with some additional information like a unique id, shared variables, and so on, as specified in Context_unifier.context_unifier_space.

Registers all clause literals at Problem_literals, and initiates the search for new context unifiers when informed by Problem_literals that a new literal has been added to the context.

Types

type config = Config.config

type statistic = Statistic.statistic

type bound = Bound.bound

type literal = Term.literal

type clause = Term.clause

type state = State.state

type context_unifier_space = Context_unifier.context_unifier_space

type raw_context_unifier = Context_unifier.raw_context_unifier

type problem_literals = Problem_literals.problem_literals

type space_registry

used to create context_unifier_space values.

Functions

val create : config ->
       bound -> space_registry

create a space_registry

Creation

val create_space : ?register:bool ->
       space_registry ->
       problem_literals ->
       clause ->
       (raw_context_unifier -> unit) ->
       (raw_context_unifier -> bool) ->
       (raw_context_unifier -> unit) ->
       (Context.element -> bool) ->
       (Context.element -> bool) ->
       bool -> context_unifier_space

create: space_registry problem_literals clause
    process_close_candidate process_assert_candidate process_split_candidate
    is_assert_incomplete is_split_incomplete  is_lemma

creates a Context_unifier_space.context_unifier_space for a Term.clause using process_close_candidate resp. process_assert_candidate resp. process_split_candidate as callback functions to be called when assert resp. split candidates are computed. see Context_unifier.create_space for details.

and registers the literals with Problem_literals if register is true (default: true).

does call process_split_candidate if an initial candidate can be computed with v only.

val get_id : space_registry -> int

returns a unique id for a context_unifier_space. Should be used if a context_unifier_space is created manually with Context_unifier.create_space

Backtracking

val backtrack : context_unifier_space -> unit

DEPENDENCY: Problem_literals.backtrack must have been executed before, dependent on resolve information managed there.