在 z3 的交叉点上使用集合和 SetHasSize

Question

我一直在尝试列举following problem 的解决方案。我先从简单的方法开始。

下面我有两组大小k，它们之间的交集大小为1，我想看看集合A和B的样子：

Els, elems = EnumSort('Els',['a1', 'a2', 'a3'])
A, B = Consts('A B', SetSort(Els))
k, c = Ints('k c')
s = Solver()
s.add(SetHasSize(A, k))
s.add(SetHasSize(B, k))
s.add(k == 2, c == 1)
s.add(SetHasSize(SetIntersect(A, B), c))
s.check()
s.model()

这里，解决方案应该是A == ['a1', 'a2'] 和B == ['a2', 'a3']，但没有达到可满足性。

即使是像下面这样的简单任务也会导致执行永无止境：

V, _ = EnumSort('Els',['a1', 'a2', 'a3'])
A = Const('A', SetSort(V))
k = Int('k')
s = SimpleSolver()
s.add(SetHasSize(A, k))
s.add(k == IntVal(2))
s.check()
s.model()

将k == IntVal(2) 更改为k <= IntVal(2) 可以解决问题并返回[A = ∃k!0 : k!0 = a1 ∨ k!0 = a2, k = 2] 作为集合的模型。我不确定是否有更快的方法。

Answer 1

如果我运行你的程序，我会得到：

WARNING: correct handling of finite domains is TBD
WARNING: correct handling of finite domains is TBD
WARNING: correct handling of finite domains is TBD

在它开始循环之前。这是实现中的一个已知问题：Z3 无法真正处理具有有限域的集合。

唉，用无限域替换它也无济于事。进行此更改：

A, B = Consts('A B', SetSort(IntSort()))

你得到：

unsat

这显然是假的。我强烈怀疑这与以下问题有关：https://github.com/Z3Prover/z3/issues/3854（简而言之，SMTLib 前端不支持set-has-size。无论出于何种原因，他们将其留在了 Python 和 C/C++ 接口中，但显然它并不是真正的功能.)

所以，严格来说，这是一个错误。但更现实的答案是 z3 不再支持set-has-size。您应该在https://github.com/Z3Prover/z3/issues 提出问题，以便作者意识到这个问题，如果它永远不受支持，可能会从 API 中完全删除它。

更新：

截至commit，z3 不再接受set-has-size 谓词；它不再受支持。