如何显示特定的未饱和约束，而不是整个核心（Z3，Python）

Question

如何仅列出来自我的未饱和核心的特定约束结果？我有很多条件，打印整个核心并不能全部打印。我读到可以使用 assert_and_track 和 unsat_core 命令来完成。我找到了一些例子，但它们不起作用。有这方面的经验吗？

s.assert_and_track(A > B, 'p1')
s.assert_and_track(B > C, 'p2')
if s.check() == sat:
  print('ok')
else:
  c = s.unsat_core
  print(c) <- this print all core

那么如何只打印 p1 或 p2（只是真/假结果）？例如p2 = false，或者它可以以 print(c) 模式中显示的方式显示 - 但仅适用于 p1。

Answer 1

实现这一点的最简单方法是简单地将标签映射保存到约束，对于这个示例，我们可以这样做

M = {}
M['p1'] = (A > B)
M['p2'] = (B > C)
M['p3'] = (C > A)

以便稍后我们可以根据这些约束打印核心，例如如下

core = s.unsat_core()
for e in core:
    print(M[str(e)])

当然，如果您只想打印一些条目而不是所有条目，这也可以。