parse_smtlib2_file method

Z3_ast_vector parse_smtlib2_file(
  1. Z3_context c,
  2. Z3_string file_name,
  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,
)

\brief Similar to #Z3_parse_smtlib2_string, but reads the benchmark from a file.

def_API('Z3_parse_smtlib2_file', 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_file(
  Z3_context c,
  Z3_string file_name,
  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_file(
    c,
    file_name,
    num_sorts,
    sort_names,
    sorts,
    num_decls,
    decl_names,
    decls,
  );
}