sig
  type t
  type id
  type term
  type location
  val pop :
    ?loc:Ast_smtlib.Statement.location -> int -> Ast_smtlib.Statement.t
  val push :
    ?loc:Ast_smtlib.Statement.location -> int -> Ast_smtlib.Statement.t
  val assert_ :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.term -> Ast_smtlib.Statement.t
  val check_sat :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
  val set_logic :
    ?loc:Ast_smtlib.Statement.location -> string -> Ast_smtlib.Statement.t
  val get_info :
    ?loc:Ast_smtlib.Statement.location -> string -> Ast_smtlib.Statement.t
  val set_info :
    ?loc:Ast_smtlib.Statement.location ->
    string * Ast_smtlib.Statement.term option -> Ast_smtlib.Statement.t
  val get_option :
    ?loc:Ast_smtlib.Statement.location -> string -> Ast_smtlib.Statement.t
  val set_option :
    ?loc:Ast_smtlib.Statement.location ->
    string * Ast_smtlib.Statement.term option -> Ast_smtlib.Statement.t
  val type_decl :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.id -> int -> Ast_smtlib.Statement.t
  val type_def :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.id ->
    Ast_smtlib.Statement.id list ->
    Ast_smtlib.Statement.term -> Ast_smtlib.Statement.t
  val fun_decl :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.id ->
    Ast_smtlib.Statement.term list ->
    Ast_smtlib.Statement.term -> Ast_smtlib.Statement.t
  val fun_def :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.id ->
    Ast_smtlib.Statement.term list ->
    Ast_smtlib.Statement.term ->
    Ast_smtlib.Statement.term -> Ast_smtlib.Statement.t
  val get_proof :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
  val get_unsat_core :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
  val get_value :
    ?loc:Ast_smtlib.Statement.location ->
    Ast_smtlib.Statement.term list -> Ast_smtlib.Statement.t
  val get_assignment :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
  val get_assertions :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
  val exit :
    ?loc:Ast_smtlib.Statement.location -> unit -> Ast_smtlib.Statement.t
end