OCaml logo

libzipperposition

Library for Zipperposition
Overview Documentation
IN THIS PACKAGE
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
| 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

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