如果是这种情况，如何强制 z3py 显示多个答案？

Question

from z3 import *

p = Int('p')
q = Int('q')

solve(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

给我 [p = 2, q = 1]，但 p 可能是 2 或 3。所以答案应该是 {2,3}。我如何让 z3 通知我多个答案？

Answer 1

这个问题经常出现，有几点需要注意。本质上，您必须编写一个循环来“拒绝”早期模型并继续查询可满足性。对于您的特定问题，您可以这样编码：

from z3 import *

p = Int('p')
q = Int('q')

s = Solver()
s.add(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

res = s.check()
while (res == sat):
  m = s.model()
  print(m)
  block = []
  for var in m:
      block.append(var() != m[var])
  s.add(Or(block))
  res = s.check()

当我运行这个时，我得到：

[p = 2, q = 1]
[p = 3, q = 1]

请注意，z3 并不总是生成“完整”模型：一旦确定问题是 sat，它就会停止生成分配。因此，您可能必须跟踪变量并明确使用 model-completion。有关如何执行此操作的详细信息，请参阅。

如果是这种情况，如何强制 z3py 显示多个答案？

How to force z3py to show multiple answers if that the case?

z3py