Module Lemma_lifted (.ml)

module Lemma_lifted: sig .. end

lifted lemma learning

computes a lemma, i.e. a clause entailed by the problem clause set, from a closing context unifier. See Lemma for details.

Types

type state = State.state

type context = Context.context

type choice_point = State.choice_point

type literal = Term.literal

type clause = Term.clause

type subst = Subst.subst

Functions

val get_lemma : uip:bool ->
       state ->
       context ->
       subst ->
       clause ->
       literal array ->
       choice_point -> clause option

get_lemma uip state context closing_context_unifier closing_clause context_literals retracted_choice_point

computes a lemma from the closing_context_unifier between the closing_clause and the used context_literals using lifted regression.

stops the regression at the retracted_choice_point, or earlier, when the uip is reached, if uip is given.