Function z3_sys::Z3_parse_smtlib2_string [−][src]
pub unsafe extern "C" fn Z3_parse_smtlib2_string(
c: Z3_context,
str: Z3_string,
num_sorts: c_uint,
sort_names: *const Z3_symbol,
sorts: *const Z3_sort,
num_decls: c_uint,
decl_names: *const Z3_symbol,
decls: *const Z3_func_decl
) -> Z3_ast
Expand description
Parse the given string using the SMT-LIB2 parser.
It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string.