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