z3 - 来自未饱和核心轨道的 SMT-LIB v2 格式的命名术语列表

Question

如何使用z3 api记录或打印出带有“a_uc_1”等名称列表的术语和名称列表的数量？

Answer 1

不幸的是，没有 API 可以做你想做的事。此信息在内部可用，但未在 API 中公开。更改 Z3 代码以提取此信息并不难。在内部，以下函数用于解析 SMT-LIB v2 文件。

bool parse_smt2_commands(cmd_context & ctx, 
                         std::istream & is, 
                         bool interactive = false, 
                         params_ref const & p = params_ref());

它在文件中定义src/parsers/smt2/smt2parser.h。

对象在cmd_contextobject 中定义src/cmd_context/cmd_context.h。

它有以下方法：

ptr_vector<expr>::const_iterator begin_assertion_names() const;
ptr_vector<expr>::const_iterator end_assertion_names() const;

这两种方法可用于遍历 SMT-LIB v2 文件中用于命名断言的所有名称。每个名称在内部都表示为布尔变量。如果ctx是cmd_context，我们可以使用以下方法遍历所有名称：

ptr_vector<expr>::const_iterator it = ctx.begin_assertion_names();
for (; it != ctx.end_assertion_names(); it++) {
   expr * n = *it;
   // do something
   // here, we just print the name
   std::cout << to_app(n)->get_decl()->get_name() << "\n";
}