module BBox:sig
..end
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
typeinductive_case =
Cover_set.case
type
payload = private
| |
Fresh |
| |
Clause_component of |
| |
Lemma of |
| |
Case of |
module Lit:Bool_lit_intf.S
with type payload = payload
typet =
Lit.t
val dummy : t
val pp_payload : payload CCFormat.printer
val inject_lits : Logtk.Literals.t -> t
val inject_lemma : Cut_form.t -> t
val inject_case : inductive_case list -> t
cst = case
val payload : t -> payload
val is_case : t -> bool
val as_case : t -> inductive_case list option
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
true
if the bool literal represents a lemmaval to_s_form : t -> Logtk.TypedSTerm.Form.t
val pp : t CCFormat.printer
val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val pp_bclause : t list CCFormat.printer