sig
type var = Logtk.FOTerm.var
type term = Logtk.FOTerm.t
type clause = Logtk.Literals.t
type form = Cut_form.clause list
type t = private { vars : Logtk.FOTerm.VarSet.t; cs : Cut_form.form; }
val make : Logtk.Literals.t list -> Cut_form.t
val trivial : Cut_form.t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val pp : t CCFormat.printer
val to_string : t -> string
val pp_tstp : Cut_form.t CCFormat.printer
val vars : Cut_form.t -> Logtk.FOTerm.VarSet.t
val cs : Cut_form.t -> Logtk.Literals.t list
val ind_vars : Cut_form.t -> Cut_form.var list
val subst1 : Cut_form.var -> Cut_form.term -> Cut_form.t -> Cut_form.t
val apply_subst :
renaming:Logtk.Subst.Renaming.t ->
Logtk.Subst.t -> Cut_form.t Logtk.Scoped.t -> Cut_form.t
val are_variant : Cut_form.t -> Cut_form.t -> bool
val normalize : Cut_form.t -> Cut_form.t
val to_s_form : Cut_form.t -> Logtk.TypedSTerm.Form.t
module Pos :
sig
val at : Cut_form.t -> Logtk.Position.t -> Cut_form.term
val lit_at :
Cut_form.t -> Logtk.Position.t -> Logtk.Literal.t * Logtk.Position.t
val clause_at :
Cut_form.t -> Logtk.Position.t -> Cut_form.clause * Logtk.Position.t
val replace :
Cut_form.t -> at:Logtk.Position.t -> by:Cut_form.term -> Cut_form.t
val replace_many :
Cut_form.t -> Cut_form.term Logtk.Position.Map.t -> Cut_form.t
end
module Seq :
sig
val terms : Cut_form.t -> Cut_form.term Sequence.t
val terms_with_pos :
?subterms:bool ->
Cut_form.t -> Cut_form.term Logtk.Position.With.t Sequence.t
end
end