package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 make_fresh : unit -> t

Create a fresh new boolean variable as a positive literal.

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_lit : Logtk.Literal.t -> t option

Convert a single literal into a boolean literal. Syntactically the same literal will be given exactly the same boolean literal. Negation of this literal will get negation of the boolean literal. Supports equality. Returns None for unsupported literals

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