Z3 : z3接口支持的命名

Question

我的问题是，我没有看到unsat_core使用api跟踪在整个块中提供的任何断言。

f = Z3_parse_smtlib2_string(c, "unsat_core_example1.smt2",0,0,0,0,0,0);
params p(c);
p.set(":unsat-core", true);
s.set(p);
// enabling unsat core tracking
expr r = to_expr(c, f);

unsat_core_example1.smt2：

(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(assert (! (or p q) :named a1))
(assert (! (implies r s) :named a2))
(assert (! (implies s (iff q r)) :named a3))
(assert (! (or r p) :named a4))
(assert (! (or r s) :named a5))
(assert (! (not (and r q)) :named a6))
(assert (! (not (and s p)) :named a7))

似乎没有处理注释:named，因为返回的unsat_core向量始终为空。

但是，如果我使用z3.exe并在中输入文件，情况就不是这样了。

知道原因是什么吗？

Answer 1

Z3_parse_smtlib2_file函数并不支持所有的SMTLIB2，它实际上只是一个方便的函数；它的输出不能保证完全覆盖所有的语言(例如，它不能执行像check-sat或一些set-option命令这样的命令)。它也是作为以前的SMTLIB1解析器的扩展编写的，该解析器是在引入目标/战术/求解器架构之前很久编写的，因此并不是所有的信息都被带到这个新的架构中。

在这种情况下，断言名称确实保存在上下文中，但是Z3_parse_smtlib2_file不返回一组断言和名称；它返回一个未命名的表达式。为了准确地表示SMTLIB2基准，函数的签名必须进行重大更改。

在给定的示例中，被断言到求解器中的表达式是r，也就是说，我们的表达式类似于

s.add(r);

这实际上要求求解器断言未命名的断言名称，但是r中的表达式不支持“子名”。但是，我们仍然可以命名r本身，例如，通过调用

s.add(r, "top")

这导致了正确的unsat核心。