z3 - how to get the number of declare-funs in smt2 instance in z3(api)

Question

I used the *Z3_parse_smtlib2_file(c,Z3_string,0,0,0,num_decl,&decl_names,&decls)* to try to get the variables and the quantity of variables. But the value of *num_decl* still be zero. What I consider the value will be become as the different smt2 files. Thanks

Answer 1

参数num_decls,decl_names和decls是输入参数。它们用于使用 C API 创建的声明初始化 SMT 2.0 解析器符号表。当前的 Z3 API 不提供用于提取在 SMT 2.0 格式的文件/字符串中声明的排序和函数的过程。此信息在内部可用。请参阅 Z3 发行版中以下目录中的文件src/parsers/smt2和src/cmd_context/cmd_context.*.