sig
  type term = Term.t
  type location = ParseLocation.t
  type inductive = {
    id : Id.t;
    vars : Statement.term list;
    cstrs : (Id.t * Statement.term list) list;
    loc : Statement.location option;
  }
  type descr =
      Pack of Statement.t list
    | Pop of int
    | Push of int
    | Prove
    | Antecedent of Statement.term
    | Consequent of Statement.term
    | Include of string
    | Set_logic of string
    | Get_info of string
    | Set_info of string * Statement.term option
    | Get_option of string
    | Set_option of string * Statement.term option
    | Def of Id.t * Statement.term
    | Decl of Id.t * Statement.term
    | Inductive of Statement.inductive
    | Get_proof
    | Get_unsat_core
    | Get_value of Statement.term list
    | Get_assignment
    | Get_assertions
    | Exit
  and t = {
    id : Id.t;
    descr : Statement.descr;
    attr : Statement.term option;
    loc : Statement.location option;
  }
  val annot : ?loc:location -> term -> term list -> term
  val include_ : ?loc:location -> string -> Id.t list -> t
  val p_cnf : ?loc:location -> int -> int -> t
  val clause : ?loc:location -> term list -> t
  val assumption : ?loc:location -> term list -> t
  val pop : ?loc:location -> int -> t
  val push : ?loc:location -> int -> t
  val assert_ : ?loc:location -> term -> t
  val check_sat : ?loc:location -> unit -> t
  val set_logic : ?loc:location -> string -> t
  val get_info : ?loc:location -> string -> t
  val set_info : ?loc:location -> string * term option -> t
  val get_option : ?loc:location -> string -> t
  val set_option : ?loc:location -> string * term option -> t
  val type_decl : ?loc:location -> Id.t -> int -> t
  val type_def : ?loc:location -> Id.t -> Id.t list -> term -> t
  val fun_decl : ?loc:location -> Id.t -> term list -> term -> t
  val fun_def : ?loc:location -> Id.t -> term list -> term -> term -> t
  val get_proof : ?loc:location -> unit -> t
  val get_unsat_core : ?loc:location -> unit -> t
  val get_value : ?loc:location -> term list -> t
  val get_assignment : ?loc:location -> unit -> t
  val get_assertions : ?loc:location -> unit -> t
  val exit : ?loc:location -> unit -> t
  val tpi : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
  val thf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
  val tff : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
  val fof : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
  val cnf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
  val inductive :
    ?loc:location -> Id.t -> term list -> (Id.t * term list) list -> t
  val data : ?loc:location -> t list -> t
  val decl : ?loc:location -> Id.t -> term -> t
  val definition : ?loc:location -> Id.t -> term -> term -> t
  val goal : ?loc:location -> ?attr:term -> term -> t
  val assume : ?loc:location -> ?attr:term -> term -> t
  val rewrite : ?loc:location -> ?attr:term -> term -> t
  val pp : Buffer.t -> Statement.t -> unit
  val print : Format.formatter -> Statement.t -> unit
end