问题描述
我一直在尝试列举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','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，将其替换为无限域也无济于事。进行更改：
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谓词；不再受支持。