package libzipperposition

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libzipperposition.BBoxSource

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

Sourcetype inductive_case = Cover_set.case
Sourcetype payload = private
  1. | Fresh
  2. | Clause_component of Logtk.Literals.t
  3. | Lemma of Cut_form.t
  4. | Case of inductive_case list
Sourcetype t = Lit.t
Sourceval dummy : t
Sourceval 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

Sourceval 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.

Sourceval inject_case : inductive_case list -> t

Inject cst = case

Sourceval payload : t -> payload

Obtain the payload of this boolean literal, that is, what the literal represents

Sourceval is_case : t -> bool
Sourceval as_case : t -> inductive_case list option

If payload t = Case p, then return Some p, else return None

Sourceval as_lemma : t -> Cut_form.t option
Sourceval 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.

Sourceval is_lemma : t -> bool

returns true if the bool literal represents a lemma

Sourceval to_s_form : t -> Logtk.TypedSTerm.Form.t

Printers

Those printers print the content (injection) of a boolean literal, if any

Sourceval pp_bclause : t list CCFormat.printer
OCaml

Innovation. Community. Security.