Module Libzipperposition.BBox

BBox (Boolean Box)

This module defines a way to encapsulate clauses and some meta-level properties into boolean literals, and maintains a bijection between encapsulated values and boolean literals

val section : Logtk.Util.Section.t
type inductive_case = Cover_set.case
type payload = private
  1. | Fresh
  2. | Clause_component of Logtk.Literals.t
  3. | Lemma of Cut_form.t
  4. | Case of inductive_case list
module Lit : Bool_lit_intf.S with type payload = payload
type t = Lit.t
val dummy : t
val pp_payload : payload CCFormat.printer
val find_boolean_lit : Logtk.Literals.t -> t option

Find a boolean literal that abstracts given clause component and the new sign of the abstracted literal. If no boolean literal exists, None will be the first component.

val inject_lits : Logtk.Literals.t -> t

Inject a clause into a boolean literal. No other clause will map to the same literal unless it is alpha-equivalent to this one. The boolean literal can be negative is the argument is a unary negative clause

val inject_lemma : Cut_form.t -> t

Make a new literal from this formula that we are going to cut on. This is generative, meaning that calling it twice with the same arguments will produce distinct literals.

val inject_case : inductive_case list -> t

Inject cst = case

val payload : t -> payload

Obtain the payload of this boolean literal, that is, what the literal represents

val is_case : t -> bool
val as_case : t -> inductive_case list option

If payload t = Case p, then return Some p, else return None

val as_lemma : t -> Cut_form.t option
val as_lits : t -> Logtk.Literals.t option
val must_be_kept : t -> bool

must_be_kept lit means that lit should survive in boolean splitting, that is, that if C <- lit, Gamma then any clause derived from C recursively will have lit in its trail.

val is_lemma : t -> bool

returns true if the bool literal represents a lemma

val to_s_form : t -> Logtk.TypedSTerm.Form.t

Printers

Those printers print the content (injection) of a boolean literal, if any

val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_bclause : t list CCFormat.printer