我一直在尝试列举以下问题的解决方案。我先从简单的方法开始。
下面我有两个大小为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]作为集合的模型。我不确定是否有更快的方法。
如果我运行你的程序，我会得到：
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++接口中，但很明显，它并没有真正起作用。(
所以，严格地说，这是一个bug。但更现实的答案是，z3不再支持set-has-size。您应该在https://github.com/Z3Prover/z3/issues因此，作者已经意识到了这个问题，如果API永远不受支持，可能会将其完全从API中删除。
更新：
从该提交起，z3不再接受set-has-size谓词；不再支持它。