Module BBox

module BBox: sig .. end

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 = 
type payload = private 
| Fresh
| Clause_component of Logtk.Literals.t
| Lemma of Cut_form.t
| 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 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 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


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