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 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 : 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 returnSome p
, else returnNone
val as_lemma : t -> Libzipperposition.Cut_form.t option
val as_lits : t -> Logtk.Literals.t option
val must_be_kept : t -> bool
must_be_kept lit
means thatlit
should survive in boolean splitting, that is, that ifC <- lit, Gamma
then any clause derived fromC
recursively will havelit
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