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