使用 scala^z3 在 z3 中可能的配置太多

Question

我猜这主要是一个逻辑问题...

我使用这个 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 在那里？ 是否有可能只得到我期望的结果？

Answer 1

使用 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(_))，我get：

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 可以选择始终返回不关心变量的值，或者可能只是列出模型中的所有不关心变量。