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 = Libzipperposition.Cover_set.case
type payload = private | Fresh | Clause_component of Logtk.Literals.t | Lemma of Libzipperposition.Cut_form.t | Case of inductive_case list

module Lit : Libzipperposition.Bool_lit_intf.S with type payload = payload

type t = Lit.t

val dummy : t
val pp_payload : payload CCFormat.printer
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 : Libzipperposition.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 -> Libzipperposition.Cut_form.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 : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_bclause : t list CCFormat.printer