Z3 Python API 中的标签约束

Question

问题 1：如何使用 Z3 Python API 来添加具有唯一标签的约束？我正在尝试类似：

... self.solver.add(self.vm[i] >= 0, 'labelIdx'+str(self.idx)) ...

其中 self.idx 是一个整数，每增加一个 i，但我得到：

z3.z3types.Z3Exception：需要 True、False 或 Z3 布尔表达式。收到labelIdx0

也就是说add的参数不能是字符串。

问题 2：函数 unsat_core() 仅适用于 Solver() 对象或也适用于 Optimize() 对象。我应该在添加约束之前设置一些选项吗？显然，这里 [1] 就是这个过程。

谢谢！

[1]https://rise4fun.com/Z3/smtc_core

Answer 1

要跟踪未饱和核心，您需要使用assert_and_track，请参见此处：https://z3prover.github.io/api/html/classz3py_1_1_solver.html#ad1255f8f9ba8926bb04e1e2ab38c8c15

不幸的是，优化和 unsat-cores 不一起工作。这是最近提出的一个问题，请参见此处：https://github.com/Z3Prover/z3/issues/1577。据我了解，这不是因为它不能被支持，而是他们还没有实现它。评论该票可以激励他们添加支持！