有没有办法使用solver.unsat_core，而不使用solver.assert_and_track？

Question

有什么方法可以让下面的代码工作，并打印出一个有效的 unsat core？

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()
s.add(a == 1)
s.add(a == 2)
s.add(b == 3)

s.check()

# This prints [], and I would like it to print [a == 1, a == 2]
print(s.unsat_core())

我知道我可以这样做：

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()
s.assert_and_track(a == 1, 'p1')
s.assert_and_track(a == 2, 'p2')
s.assert_and_track(b == 3, 'p3')

s.check()
# This prints [p1, p2]
print(s.unsat_core())

但对于我正在从事的实际项目，遍历并为每个约束命名会很痛苦（由于它们的体积以及它们的生成方式。）

Answer 1

除非您自己实现，否则不会。未饱和核心提取需要标记约束，请参阅本文档第 67 页的顶部：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

话虽如此，您可以通过定义自己的add 版本来构建断言的“数据库”，该版本首先组成一个名称并插入它，然后在您的函数my_unsat_core 中进行反向查找将类似地定义。如果您要以通用方式实现此功能，Z3 人员可能也有兴趣将其合并到他们的 API 中。会是一个不错的补充。