Module Selection (.ml)

module Selection: sig .. end

selection of a split or assert literal

manages the computation of candidates for Assert and Split after each change of the context with Selection_assert, Selection_split.

manages the original problem clause set, plus derived lemmas.

Types

type config = Config.config

type bound = Bound.bound

type statistic = Statistic.statistic

type literal = Term.literal

type clause = Term.clause

type choice_point = State.choice_point

type state = State.state

type selected = Selection_types.selected

type context = Context.context

type guiding_path = Jumping.guiding_path

type selection

the Selection data structure

exception SATISFIABLE

no further applicable candidate available - satisfiability of the problem detected

Functions

Creation

val create : config ->
       bound ->
       statistic ->
       state ->
       context ->
       clause list ->
       clause list ->
       literal list -> guiding_path -> selection

create ... input_clauses lemmas initial_interpretation guiding_path creates a new selection over the given input clauses and lemmas.

if a guiding_path is given, only the search space specified by it is searched. that is, first the candidate literals are selected so that the guiding_path is recreated, then the search continues as usual.

lemmas are lemmas kept over a restart.

initial_interpretation is a set of literals which is asserted to the initial context.

val add_lemma : selection -> clause -> unit

add a lemma to the current clause set.

this does not compute any context unifiers, so Context_unifier.CLOSE may not be raised.

also ok to store local lemmas, i.e. lemmas learnt after an incomplete branch has been discovered.

Creation

val add : selection -> Context.element -> unit

to be called when a new element is added to the context. Updates the set of assert and split candidate literals. May raise Context_unifier.CLOSE.

val select : selection -> selected

selects a literal to be added to the context. Raises Selection.SATISFIABLE if no applicable candidate literal exists.

Misc

val get_lemmas : selection -> clause list

get all stored (non-local) lemmas.

val in_replay : selection -> bool

is the derivation still replaying the initial guiding path?

Backtracking

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

backtrack selection retracted_split explanation removes candidates based on invalid states.

takes the retracted left split and its explanation.

DEPENDENCY: State_backtrack must have been executed before.