package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct