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.