这主要是我猜的逻辑问题……
我使用这个 smtlib 公式：
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert (xor (and a (xor b c)) d))
这是这个结构的一个术语（至少在我看来）：
XOR
| |
AND d
| |
a XOR
| |
b c
我的猜测：结果集应该是这样的：
{ab, ac, d}
但它使用 scala^z3 ctx.checkAndGetAllModels():
{ab, d, ac, ad, abcd}
为什么里面有ad和abcd？ 是否有可能只得到我期望的结果？
【问题讨论】：
使用 Scala（不带 Z3）来证明实际上还有更多的约束解决方案：
val tf = Seq(true, false)
val allValid =
for(a <- tf; b <- tf; c <- tf; d <- tf;
if((a && (b ^ c)) ^ d)) yield (
(if(a) "a" else "") + (if(b) "b" else "") +
(if(c) "c" else "") + (if(d) "d" else ""))
allValid.mkString("{ ", ", ", " }")
打印：
{ abcd, ab, ac, ad, bcd, bd, cd, d }
所以除非我遗漏了什么，否则问题是，为什么它没有找到所有解决方案？现在这是那个问题的答案。 （剧透警告：“getAllModels”并没有真正获取所有模型。）首先，让我们重现您观察到的内容：
import z3.scala._
val ctx = new Z3Context("MODEL" -> true)
val a = ctx.mkFreshConst("a", ctx.mkBoolSort)
val b = ctx.mkFreshConst("b", ctx.mkBoolSort)
val c = ctx.mkFreshConst("c", ctx.mkBoolSort)
val d = ctx.mkFreshConst("d", ctx.mkBoolSort)
val cstr0 = ctx.mkXor(b, c)
val cstr1 = ctx.mkAnd(a, cstr0)
val cstr2 = ctx.mkXor(cstr1, d)
ctx.assertCnstr(cstr2)
现在，如果我运行：ctx.checkAndGetAllModels.foreach(println(_))，我会得到：
d!3 -> false
a!0 -> true
c!2 -> false
b!1 -> true
d!3 -> true // this model is problematic
a!0 -> false
d!3 -> false
a!0 -> true
c!2 -> true
b!1 -> false
d!3 -> true
a!0 -> true
c!2 -> false
b!1 -> false
d!3 -> true
a!0 -> true
c!2 -> true
b!1 -> true
现在，问题在于第二个模型是一个不完整模型。 Z3 可以返回它，因为无论b 和c 的值是什么，都满足约束（b 和c 是无关 变量）。 checkAndGetAllModels的当前实现只是简单地否定模型以防止重复；在这种情况下，它将要求另一个模型，例如 (not (and d (not a))) 成立。这将阻止返回具有这两个值的所有其他模型。从某种意义上说，不完整模型实际上代表了四个有效的、完整的模型。
顺便说一句，如果您将 ScalaZ3 的 DSL 与 findAll 函数一起使用会发生什么情况，当所有模型不完整时（以及在它们习惯于计算下一个）。在 DSL 的上下文中，我们可以这样做，因为我们知道出现在公式中的变量集。在这种情况下，很难猜测应该如何完成模型。一种选择是让 ScalaZ3 记住使用了哪些变量。更好的解决方案是 Z3 可以选择始终返回无关变量的值，或者可能只是列出模型中的所有无关变量。
【讨论】：