Statement (docs.other.smtml.Smtml.Smtlib.Statement)

type t = Ast.t

val reset : ?loc:'a -> unit -> Ast.t

val exit : ?loc:'a -> unit -> Ast.t

val push : ?loc:'a -> int -> Ast.t

val pop : ?loc:'a -> int -> Ast.t

val reset_assertions : ?loc:'a -> unit -> Ast.t

val type_decl : ?loc:'a -> 'b

val type_def : ?loc:'a -> Symbol.t -> 'b -> Expr.t -> Ast.t

val datatypes : ?loc:'a -> 'b

val fun_decl : 
  ?loc:Loc.t ->
  Symbol.t ->
  Expr.t list ->
  Expr.t list ->
  Expr.t ->
  Ast.t

val fun_def : ?loc:'a -> 'b

val funs_def_rec : ?loc:'a -> 'b -> 'c

val assert_ : ?loc:'a -> Expr.t -> Ast.t

val get_assertions : ?loc:'a -> unit -> Ast.t

val check_sat : ?loc:'a -> Expr.t list -> Ast.t

val get_model : ?loc:'a -> unit -> Ast.t

val get_value : ?loc:'a -> Expr.t list -> Ast.t

val get_assignment : ?loc:'a -> unit -> Ast.t

val get_proof : ?loc:'a -> unit -> 'b

val get_unsat_core : ?loc:'a -> unit -> 'b

val get_unsat_assumptions : ?loc:'a -> unit -> 'b

val get_info : ?loc:'a -> string -> Ast.t

val get_option : ?loc:'a -> string -> Ast.t

val echo : ?loc:'a -> string -> Ast.t

val set_info : ?loc:'a -> Expr.t -> Ast.t

val set_option : ?loc:'a -> Expr.t -> Ast.t

val set_logic : ?loc:Loc.t -> string -> Ast.t