Module Selection_assert (.ml)

module Selection_assert: sig .. end

type config = Config.config 

type bound = Bound.bound 

type statistic = Statistic.statistic 

type literal = Term.literal 

type state = State.state 

type raw_context_unifier = Context_unifier.raw_context_unifier 

type problem_literals = Problem_literals.problem_literals 

type selected = Selection_types.selected 

type context = Context.context 

type candidates 

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

creates an empty candidate repository.

val has_closing_candidate : candidates -> bool

the next candidate to be chosen will lead to the computation of a closing context unifier (Selection_lookahead). imperfect, might return false although the candidate leads to a Close.

val size : candidates -> int

the number of candidates to chose from. not all of these may be actually eligible, some candidates may be subsumed by the context, and other candidates may be invalidated by backtracking, but not yet removed (done lazily).

val add : candidates -> raw_context_unifier -> bool

adds an assert candidate to the repository. returns true if a lookahead closing candidate is known (Selection_assert.has_closing_candidate).

val select : candidates -> selected option

selects (priority based) an assert literal from the repository, and blocks it from further selection (until backtracking).

Does not choose candidates subsumed by the context.

Returns None, if no further assert candidate exists.

val check_exceeding : candidates -> unit

registers all candidates which exceed the depth bound and are currently applicable Bound.

to be called only when select returns None, based on the semantics of Flags.opt_restart, when a branch has to be checked for being exhausted.

val is_element_incomplete : candidates -> Context.element -> bool

is_element_incomplete candidates context_element returns true if applicable exceeding candidates computed by this context_element have been dropped when the restart mode Config.restart is Flags.opt_restart.RS_Delayed.

Then, when a branch has been found that is saturated wrt. to the candidates within the current depth bound, all candidates for incomplete context elements are recomputed and checked if they are satisfied in the branch, and registered in Bound otherwise.

val backtrack : candidates -> unit

returns the candidate store to the one associated to the current active state.

DEPENDENCY: State_backtrack must have been executed before.