在 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] 被评估为 false 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)

---

注意：因为z3 善意标记不关心布尔变量，另一种选择是编写您自己的模型生成器来自动完成任何部分模型.这将减少对s.check() 的调用次数。这种实现的性能影响很难衡量，但它可能会稍微快一些。