Module Lemma_propositional (.ml)


module Lemma_propositional: sig .. end
propositional 'lemma' generation

treats a conflict set, i.e. the negation of a set of splits leading to a conflict, as a lemma and performs propagations and closures on it.

See Lemma for details.



Types

type config = Config.config 
type bound = Bound.bound 
type literal = Term.literal 
type clause = Term.clause 
type state = State.state 
type context = Context.context 
type choice_point = State.choice_point 
type explanation = State.explanation 
type propositional_lemmas 
type raw_context_unifier = Context_unifier.raw_context_unifier 
type candidates = Selection_assert.candidates 
type selected = Selection_types.selected 
type space_registry = Context_unifier_space.space_registry 
type lemmas_propositional 

Functions

val create : config ->
state ->
context ->
candidates ->
(raw_context_unifier -> unit) ->
(raw_context_unifier -> bool) ->
space_registry ->
lemmas_propositional
create config state context candidates process_close_candidate process_assert_candidate space_registry creates a lemmas_propositional structure. process_close_candidate and process_split_candidate correspond to the elements of the same name in Context_unifier.context_unifier_space, and are used by Lemma_propositional.extend_context to propagate candidates.
val add_lemma : lemmas_propositional ->
clause -> bool -> unit
add_lemma lemmas_propositional lemma global adds the lemma.

if global then the lemma is independent of the current derivation and can be reused after a restart.

val extend_context : lemmas_propositional -> Context.element -> unit
compute assert and close candidates for the new context element and propagate them
val get_lemmas : lemmas_propositional -> clause list
returns all global (see ) clauses.
val backtrack : lemmas_propositional -> unit
backtracks to the most recent valid choice point