module Cut_form: sig
.. end
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 {
|
vars : Logtk.Term.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
type
cut_form = t
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 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
val subst1 : var -> term -> t -> t
Substitution of one variable
val apply_subst : 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
module FV_tbl: functor (
X
:
Map.OrderedType
) ->
sig
.. end
Structure for Sets of cut forms, indexed modulo α-eq