sig
type var = Logtk.Term.var
type term = Logtk.Term.t
type clause = Logtk.Literals.t
type form = Cut_form.clause list
type t = private { vars : Logtk.Term.VarSet.t; cs : Cut_form.form; }
type cut_form = Cut_form.t
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 pp_zf : Cut_form.t CCFormat.printer
val vars : Cut_form.t -> Logtk.Term.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 :
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
module FV_tbl :
functor (X : Map.OrderedType) ->
sig
type value = X.t
type t
val create : unit -> Cut_form.FV_tbl.t
val add :
Cut_form.FV_tbl.t ->
Cut_form.cut_form -> Cut_form.FV_tbl.value -> unit
val mem : Cut_form.FV_tbl.t -> Cut_form.cut_form -> bool
val get :
Cut_form.FV_tbl.t ->
Cut_form.cut_form -> Cut_form.FV_tbl.value option
val to_seq :
Cut_form.FV_tbl.t -> (Cut_form.cut_form * X.t) Sequence.t
end
end