我在 python 中有一个这样的整数列表：
myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]
我想让 Z3 输出各种数字集或数字列表，它们都是 myList 的所有成员...本质上，我想使用 Z3 来获取其他数字列表，这些数字都存在于 myList 中，但顺序不同。换句话说，我想从 Z3 获得各种输出，其中包含上面集合 myList 中的数字。
我在使用 Z3py 时遇到问题，因为我不知道如何让 z3 在调用 s.model() 时返回一个列表或一个集合作为模型，假设为 s = Solver()。
【问题讨论】：
from z3 import *
myList = [97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57]
s = Solver ()
pick = []
for (i, v) in enumerate(myList):
b = Bool ('pick_%d' % i)
s.add(b == b)
pick += [(b, v)]
while (s.check() == sat):
m = s.model()
chosen = []
block = []
for (p, v) in pick:
if m.eval(p, model_completion=True):
chosen += [v]
block.append(Not(p))
else:
block.append(p)
print chosen
s.add(Or(block))
请注意，这将打印2^n 解决方案，其中n 是列表中元素的数量；所以如果n 很大，需要一段时间才能完成！
【讨论】：
s.add(b==b)，要么将model_completion=True 参数传递给eval。 （我两个都做了；但你实际上只需要其中一个。两者都没有伤害。）否则求解器对布尔值一无所知，因为它一开始就没有限制。 s.add(b==b) 是告诉求解器的一种廉价方式：“嘿，我有这个变量，没有任何限制。”请注意，调用Bool 对Solver 实例没有任何作用，因此您需要以某种方式使其意识到这一点。这是一种方法。