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