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.

Returns A string representation of the benchmark.

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.

Returns A conjunction of assertions in the scope (up to push/pop) at the end of the string.

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.