Module Selection_lookahead (.ml)

module Selection_lookahead: sig .. end

Close lookahead for candidates

Used to store assert and unit split candidates in a lookahead set. Other assert (and unit split) candidates can be checked for contradiction with the lookahead set.

The intention is that if there exist two contradictory candidates, then this will be detected early and Close can be applied. Otherwise - depending on the selection heuristic and bad luck -- those contradictory candidates might not be chosen at all in a reasonable amount of time.

Types

type literal = Term.literal

type raw_context_unifier = Context_unifier.raw_context_unifier

type selection_lookahead

Functions

val create : int -> selection_lookahead

create limit database creates a lookahead where at most limit candidates are stored in the index.

val is_full : selection_lookahead -> bool

is the index full, i.e. limit candidates are stored?

val add : no_duplicates:bool ->
       selection_lookahead ->
       literal ->
       raw_context_unifier -> unit

add no_duplicates candidate_literal candidate_context_unifier adds a candidate_literal with its context unifier to the lookahead set.

stores each candidate_literal only once, if no_duplicates is given, duplicates are ignored (see Term_indexing).

val check : selection_lookahead ->
       literal -> bool

check literal returns true, if the literal is contradictory with the lookahead set.

val backtrack : selection_lookahead -> unit

removes invalid candidates.

DEPENDENCY: State_backtrack must have been executed before.