Module Z3.SMT

module SMT: sig .. end

Functions for handling SMT and SMT2 expressions and files


val benchmark_to_smtstring : context ->
string ->
string -> string -> string -> Expr.expr list -> Expr.expr -> string

Convert a benchmark into an SMT-LIB formatted string.

val parse_smtlib2_string : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list ->
FuncDecl.func_decl list -> AST.ASTVector.ast_vector

Parse the given string using the SMT-LIB2 parser.

val parse_smtlib2_file : context ->
string ->
Symbol.symbol list ->
Sort.sort list ->
Symbol.symbol list ->
FuncDecl.func_decl list -> AST.ASTVector.ast_vector

Parse the given file using the SMT-LIB2 parser.