z3 - 在 Z3Py 中获取布尔表达式的所有解决方案永远不会结束

Question

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

根据找到的其他响应，例如Z3:finding all compatible 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/cs.model()[a]不再存在。

有人能告诉我我做错了什么吗？

标签： z3z3py

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)的恒等关系，并且它作为结果返回而不是. （见相关问答）xmxTrue/False

---

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