sig
val benchmark_to_smtstring :
Z3.context ->
string ->
string -> string -> string -> Z3.Expr.expr list -> Z3.Expr.expr -> string
val parse_smtlib_string :
Z3.context ->
string ->
Z3.Symbol.symbol list ->
Z3.Sort.sort list ->
Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> unit
val parse_smtlib_file :
Z3.context ->
string ->
Z3.Symbol.symbol list ->
Z3.Sort.sort list ->
Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> unit
val get_num_smtlib_formulas : Z3.context -> int
val get_smtlib_formulas : Z3.context -> Z3.Expr.expr list
val get_num_smtlib_assumptions : Z3.context -> int
val get_smtlib_assumptions : Z3.context -> Z3.Expr.expr list
val get_num_smtlib_decls : Z3.context -> int
val get_smtlib_decls : Z3.context -> Z3.FuncDecl.func_decl list
val get_num_smtlib_sorts : Z3.context -> int
val get_smtlib_sorts : Z3.context -> Z3.Sort.sort list
val parse_smtlib2_string :
Z3.context ->
string ->
Z3.Symbol.symbol list ->
Z3.Sort.sort list ->
Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> Z3.Expr.expr
val parse_smtlib2_file :
Z3.context ->
string ->
Z3.Symbol.symbol list ->
Z3.Sort.sort list ->
Z3.Symbol.symbol list -> Z3.FuncDecl.func_decl list -> Z3.Expr.expr
end