parse_smtlib2_string method

Z3_ast_vector parse_smtlib2_string(
  1. Z3_context c,
  2. Z3_string str,
  3. int num_sorts,
  4. Pointer<Z3_symbol> sort_names,
  5. Pointer<Z3_sort> sorts,
  6. int num_decls,
  7. Pointer<Z3_symbol> decl_names,
  8. Pointer<Z3_func_decl> decls,
)

@name Parser interface / /**@{/ /** \brief 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.

def_API('Z3_parse_smtlib2_string', AST_VECTOR, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL)))

Implementation

Z3_ast_vector parse_smtlib2_string(
  Z3_context c,
  Z3_string str,
  int num_sorts,
  ffi.Pointer<Z3_symbol> sort_names,
  ffi.Pointer<Z3_sort> sorts,
  int num_decls,
  ffi.Pointer<Z3_symbol> decl_names,
  ffi.Pointer<Z3_func_decl> decls,
) {
  return _parse_smtlib2_string(
    c,
    str,
    num_sorts,
    sort_names,
    sorts,
    num_decls,
    decl_names,
    decls,
  );
}