0

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

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

4

1 回答 1

3

使用 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 可以返回它，因为无论 and 的值是什么，b都c满足约束（b并且c是无关变量）。当前的实现checkAndGetAllModels只是简单地否定模型以防止重复；在这种情况下，它会要求另一个模型这样(not (and d (not a)))成立。这将阻止返回具有这两个值的所有其他模型。从某种意义上说，不完整模型实际上代表了四个有效的、完整的模型。

顺便说一句，如果您将 ScalaZ3 的 DSL 与该函数一起使用，那么当所有模型不完整时（以及在用于计算下一个findAll模型之前），所有模型都将使用默认值完成。在 DSL 的上下文中，我们可以这样做，因为我们知道出现在公式中的变量集。在这种情况下，很难猜测应该如何完成模型。一种选择是让 ScalaZ3 记住使用了哪些变量。更好的解决方案是 Z3 可以选择始终返回无关变量的值，或者可能只是列出模型中的所有无关变量。

于 2011-12-09T18:51:38.367 回答