Module Libzipperposition.Cut_form

Universally Quantified Conjunction of Clauses

type var = Logtk.Term.var
type term = Logtk.Term.t
type clause = Logtk.Literals.t
type form = clause list
type t = private {
  1. vars : Logtk.Term.VarSet.t;
  2. cs : form;
}

A formula of the form forall vars. \bigand_i C_i. The C_i are clauses with free variables in vars

type cut_form = t
val make : Logtk.Literals.t list -> t
val trivial : t
include Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
val compare : t -> t -> int
include Logtk.Interfaces.PRINT with type t := t
val to_string : t -> string
val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val vars : t -> Logtk.Term.VarSet.t
val cs : t -> Logtk.Literals.t list
val ind_vars : t -> var list

subset of vars that have an inductive type

val subst1 : var -> term -> t -> t

Substitution of one variable

val are_variant : t -> t -> bool

Are these two cut formulas alpha-equivalent?

val normalize_form : form -> form
val normalize : t -> t

Use rewriting to normalize the formula

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

Convert to input formula

module Pos : sig ... end
module Seq : sig ... end
module FV_tbl (X : Map.OrderedType) : sig ... end