在Z3Py中获取布尔表达式的所有解永不结束

Question

可能是与Z3有关的一个基本问题：我正在尝试获取布尔表达式的所有解，例如对于a OR b，我想获得{(true, true),(false,true),(true,false)}

基于发现的其他回复，例如Z3: finding all satisfying models，我有以下代码：

a = Bool('a')
b = Bool('b')

f1=Or(a,b)
s=Solver()
s.add(f1)

while s.check() == sat:
  print s
  s.add(Not(And(a == s.model()[a], b == s.model()[b])))

[问题在于，它在第二次迭代时进入了无限循环：约束a == s.model()[a]的计算结果为假b / c s.model()[a]不再存在。

有人可以告诉我我在做什么错吗？

Answer 1

我建议您尝试这样编写循环：

from z3 import *

a = Bool('a')
b = Bool('b')

f1 = Or(a,b)
s = Solver()
s.add(f1)

while s.check() == sat:

    m = s.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Model:")
    print("a := " + str(v_a))
    print("b := " + str(v_b))

    bc = Or(a != v_a, b != v_b)
    s.add(bc)

输出为：

Model:
a := True
b := False
Model:
a := False
b := True
Model:
a := True
b := True

自变量model_completion=True是必需的，因为否则，m.eval(x)的行为类似于当前模型x中任何具有[[不在乎值的m布尔变量的身份关系，并且它返回x结果，而不是True/False。 （See related Q/A）

---

NOTE：因为z3友好地标记了[[on't care

布尔变量，所以另一种选择是编写自己的模型生成器，该模型生成器可以自动完成任何部分模型。这将减少呼叫s.check()的次数。此实现对性能的影响很难评估，但可能会稍快一些。