1

我试图养成使用 Dafny 作为一些简单公式的友好 SAT-QBF 求解器的习惯，因为在 Z3 中这样做太不舒服了。

上下文是我已经实现了 Cooper 的量词消除算法，当所有变量都有界时，它可以用作决策过程：因此，我想知道在执行它之前应该得到哪个结果。

但是，我在 Dafny 中遇到了一个问题。

例如，让我们提出这个公式（用 Dafny 编写）：

  assert forall x_1: int :: exists y_1: int :: forall x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

在我的 Cooper 中，它返回False，而 Dafny 返回assertion violation（以及典型的triggers警告），我False也将其解释为。好的，所以这没有问题。

但如果我提出：

  assert exists x_1: int :: exists y_1: int :: exists x_2: int :: exists y_2 : int
    :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);

在我的 Cooper 中，它返回True，而 Dafny 也返回assertion violation。我已经完成了手动 Cooper 执行（铅笔和纸），我认为这True是正确的。

知道发生了什么吗？

PS：我还没有在Z3中尝试过，因为我在做其他理论的第一次尝试。

编辑

使用一个简单的技巧来实例化量化变量可以避免触发警告：创建一个未解释的函数。


method Main() {
 assert exists x_1 : int {:trigger P(x_1)} :: exists y_1: int {:trigger P(y_1)} 
    :: exists x_2: int {:trigger P(x_2)} :: exists y_2 : int {:trigger P(y_2)}
        :: (y_2<y_1) && (x_2<y_2) && (x_1<x_2);
}


predicate P(a: int)
{
   true
}
4

1 回答 1

2

你不能用 Dafny 做到这一点。虽然 Dafny 支持量词、布尔值、算术和许多其他东西（递归函数、集合、序列、对象和引用、多维数组、归纳、归纳和协归纳数据类型、位向量、单调函数的最大和最小固定点等） ，它不适用于 SAT-QBF（或 QBF + artihmetic）基准。

Dafny 的错误，包括assertion violation，告诉您验证者无法进行证明。可能该财产仍然存在，但您需要自己提供更多证明。换句话说，您应该将其解释assertion violation为“不知道”的答案。换句话说，你不能用 Dafny决定（只是半决定）公式。

Dafny 通过匹配模式（即触发器）在 SMT 求解器中使用量词。当量词没有好的触发器时，这就是 Dafny 的“无触发器”警告告诉您的，您可能会看到性能不佳、验证不稳定和所谓的蝴蝶效应（程序中看似无关的小部分会导致更改）在其他证明的自动构造中）。触发器由未解释的函数符号驱动，您的示例根本没有。

如果你想要一个可读的语法，你可以通过 Boogie 做你正在尝试的事情。我没有尝试过，但是您可以尝试将 Boogie 置于其单态模式，然后提供证明者选项来请求 SAT-QBF 或类似的东西（请参阅 Boogie's /help）。否则，如果您有兴趣决定这些问题，那么直接使用 SMT 求解器是您的最佳选择。

于 2021-05-25T17:29:29.743 回答