Module Cut_form

module Cut_form: sig .. end

Universally Quantified Conjunction of Clauses



type var = Logtk.FOTerm.var 
type term = Logtk.FOTerm.t 
type clause = Logtk.Literals.t 
type form = clause list 
type t = private {
   vars : Logtk.FOTerm.VarSet.t;
   cs : form;
}
A formula of the form forall vars. \bigand_i C_i. The C_i are clauses with free variables in vars
val make : Logtk.Literals.t list -> t
val trivial : t
include Interfaces.HASH
include Interfaces.ORD
include Interfaces.PRINT
val pp_tstp : t CCFormat.printer
val vars : t -> Logtk.FOTerm.VarSet.t
val cs : t -> Logtk.Literals.t list
val ind_vars : t -> var list
subset of Cut_form.vars that have an inductive type
val subst1 : var -> term -> t -> t
Substitution of one variable
val apply_subst : renaming:Logtk.Subst.Renaming.t ->
Logtk.Subst.t -> t Logtk.Scoped.t -> t
val are_variant : t -> t -> bool
Are these two cut formulas alpha-equivalent?
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