sig
  type t
  type id
  type term
  type location
  val annot :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.term -> Stmt_intf.Logic.term list -> Stmt_intf.Logic.term
  val include_ :
    ?loc:Stmt_intf.Logic.location ->
    string -> Stmt_intf.Logic.id list -> Stmt_intf.Logic.t
  val p_cnf :
    ?loc:Stmt_intf.Logic.location -> int -> int -> Stmt_intf.Logic.t
  val clause :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.term list -> Stmt_intf.Logic.t
  val assumption :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.term list -> Stmt_intf.Logic.t
  val pop : ?loc:Stmt_intf.Logic.location -> int -> Stmt_intf.Logic.t
  val push : ?loc:Stmt_intf.Logic.location -> int -> Stmt_intf.Logic.t
  val assert_ :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val check_sat : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val set_logic :
    ?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
  val get_info : ?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
  val set_info :
    ?loc:Stmt_intf.Logic.location ->
    string * Stmt_intf.Logic.term option -> Stmt_intf.Logic.t
  val get_option :
    ?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
  val set_option :
    ?loc:Stmt_intf.Logic.location ->
    string * Stmt_intf.Logic.term option -> Stmt_intf.Logic.t
  val type_decl :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id -> int -> Stmt_intf.Logic.t
  val type_def :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id ->
    Stmt_intf.Logic.id list -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val fun_decl :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id ->
    Stmt_intf.Logic.term list -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val fun_def :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id ->
    Stmt_intf.Logic.term list ->
    Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val get_proof : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val get_unsat_core :
    ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val get_value :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.term list -> Stmt_intf.Logic.t
  val get_assignment :
    ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val get_assertions :
    ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val exit : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
  val tpi :
    ?loc:Stmt_intf.Logic.location ->
    ?annot:Stmt_intf.Logic.term ->
    Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val thf :
    ?loc:Stmt_intf.Logic.location ->
    ?annot:Stmt_intf.Logic.term ->
    Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val tff :
    ?loc:Stmt_intf.Logic.location ->
    ?annot:Stmt_intf.Logic.term ->
    Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val fof :
    ?loc:Stmt_intf.Logic.location ->
    ?annot:Stmt_intf.Logic.term ->
    Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val cnf :
    ?loc:Stmt_intf.Logic.location ->
    ?annot:Stmt_intf.Logic.term ->
    Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val inductive :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id ->
    Stmt_intf.Logic.term list ->
    (Stmt_intf.Logic.id * Stmt_intf.Logic.term list) list ->
    Stmt_intf.Logic.t
  val data :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.t list -> Stmt_intf.Logic.t
  val decl :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val definition :
    ?loc:Stmt_intf.Logic.location ->
    Stmt_intf.Logic.id ->
    Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val goal :
    ?loc:Stmt_intf.Logic.location ->
    ?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val assume :
    ?loc:Stmt_intf.Logic.location ->
    ?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
  val rewrite :
    ?loc:Stmt_intf.Logic.location ->
    ?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
end