Module Selection_split (.ml)

module Selection_split: sig .. end

type config = Config.config 

type choice_point = State.choice_point 

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 space_registry = Context_unifier_space.space_registry 

type selected = Selection_types.selected 

type context = Context.context 

type candidates 

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

creates an empty candidate repository.

val size : candidates -> int

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

val add : candidates -> raw_context_unifier -> unit

adds a split candidate to the repository.

val select : candidates ->
       Jumping.guiding_step option -> selected option

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

Does not choose non-applicable candidates, i.e candidates subsumed by, contradictory with, or not productive with the current context.

Returns None, if no further split candidate exists.

val select_right_split : candidates -> selected option

selects a right split literal and blocks it from further selection (until backtracking).

upon backtracking a left split with Selection_split.backtrack the corresponding right split is remembered as long as it is implied.

DEPENDENCY: these have to be applied exhaustively after backtracking before any split or assert to ensure completeness/soundness.

Returns None, if no further right split candidate exists.

raise CLOSE, if right split is inconsistent with context.

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

see Selection_assert.is_element_incomplete.

val remainder_literals_to_string : config ->
       context -> raw_context_unifier -> string

textual representation of (the remainder of) the context unifier as a clause.

val backtrack : candidates ->
       choice_point -> literal list -> unit

backtrack candidates retracted explanation returns the candidate store to the one associated to the current active state.

retracted is the choice point corresponding to the retracted left split, explanation are the choice points which implie this conflict. that is, explanation is the explanation of the corresponding right split, which is stored for further usage (Selection_split.select_right_split).

DEPENDENCY: State_backtrack must have been executed before.