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

【问题标题】：a list of named terms from SMT-LIB v2 format of unsat core track来自未饱和核心轨道的 SMT-LIB v2 格式的命名术语列表
【发布时间】：2013-03-13 09:39:23
【问题描述】：

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

【问题讨论】：

不清楚你想做什么。您能否改进问题并提供一个小例子？
例如，找出未饱和的核心，它们是 (a__uc__1 a__uc__2 a__uc__3 a__uc__4 a__uc__5 a__uc__6 a__uc__7)，大小为 7。有用吗？
对不起，我还是不明白你想要什么。
作为解决实例 SMT-LIB v2 格式， (set-option: generate unsat cores true) (assert ! (let ((?def0 x1)) (let ((?def1(a__uc__1并统计列表的数量？希望可以有帮助。谢谢。

标签： z3

【解决方案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_context 对象在对象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";
}

【讨论】：