z3 - Z3中的触发问题

Question

我最近在 Z3 中观察到了一些关于触发的行为，我不明白。不幸的是，这些示例来自大型 Boogie 文件，所以我想我现在应该抽象地描述它们，只是为了看看是否有明显的答案。但是，如果具体文件会更好，我可以附上它们。

基本上有三个问题，尽管第三个问题很可能是第二个问题的特例。就我的理解而言，没有任何行为是预期的，但也许我错过了一些东西。任何帮助将不胜感激!

首先 :就触发而言，我的程序中的琐碎等式似乎被忽略了。例如，如果 t1是一个术语，它应该匹配量化公理的模式，如果我在我的 Boogie 程序中添加一行

assert t1 == t1;

然后 t1似乎没有被用作量化公理的触发器。我明确添加了该行以提供 t1作为证明者的触发器，我经常在 Boogie 程序中做/做。

如果相反我引入了一个额外的功能，说

function f(x : same_type_as_t1) : bool
{ true }

现在改为添加一行

assert f(t1);

到我的程序，然后 t1似乎确实被 Z3 用作触发器。我检查了前一个程序的 Z3 翻译，以及 t1 上的(微不足道的)等式。确实在 Boogie 翻译中幸存下来(即，Boogie 并没有试图做一些聪明的事情)。

第二个:次要模式似乎对我不起作用。例如，我有一个程序，其中一个公理的形式为

axiom (forall ... :: {t1,t2} {t3,t4,t5} ..... );

以及t3, t4的情况和 t5都发生了。程序无法验证，显然是因为公理没有被实例化。但是，如果我将公理重写为

axiom (forall ... :: {t3,t4,t5} {t1,t2} ..... );

然后程序验证。在这两种情况下，运行 Boogie 的时间大约为 3 秒，并且模式保留到 Z3 输出。

第三:这很可能是第二个问题的症状，但我对以下行为感到惊讶:

我写了以下形式的公理

axiom (forall .. :: {t1,t2} .... );

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );

并且在 t2 的情况下和 t3已经发生，第一个公理没有被实例化(我预计它会，因为在第二个公理实例化之后，t1 发生)。但是，如果我改写为

axiom (forall .. ::  {t2,t3} {t1,t2} .... );

axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );

然后第一个公理被实例化。但是，如果出于某种原因，一般没有使用次要模式，那么这也可以解释这种行为。

如果明确的例子有用，我当然可以附上长的，并且可以尝试将它们减少一点(但当然触发问题有点微妙，所以如果我让例子太小，我很可能会失去行为)。

非常感谢您提供任何建议!

亚历克斯·萨默斯

编辑:这是一个示例，部分说明了上述第二和第三种行为。我附上了 Boogie 代码，以便在这里阅读更容易，但如果 Z3 输入更有用，我也可以复制或通过电子邮件发送。我已经删掉了几乎所有的原始 Boogie 代码，但似乎很难在不完全失去行为的情况下使它更简单。

下面的代码与我的原始示例的行为已经略有不同，但我认为它已经足够接近了。基本上，下面标记为 (1) 的公理无法使其第二个模式集匹配。如果我将公理 (1) 注释掉，而是用(当前已注释的)公理 (2) 和 (3) 替换它，它们只是带有两个模式集的原始副本，然后程序会验证。实际上，在这种特殊情况下有公理(2)就足够了。在我的原始代码中(在我削减它之前)，翻转公理 (1) 中两个模式集的顺序也足够了，但在我的较小的repro 中似乎不再是这种情况。

type ref;
type HeapType;

function vals1(HeapType, ref) returns (ref);
function vals2(HeapType, ref) returns (ref);
function vals3(HeapType, ref) returns (ref);

function heap_trigger(HeapType) returns (bool);

function trigger1(ref) returns (bool);
function trigger2(ref) returns (bool);

axiom (forall Heap: HeapType, this: ref ::  {vals1(Heap, this)}  (vals1(Heap, this) == vals3(Heap,this)));

axiom (forall Heap: HeapType, this: ref :: {vals2(Heap, this)}  trigger2(this));

// (1)
axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this)));

// (2)
// axiom (forall Heap: HeapType, this: ref :: {trigger1(this), heap_trigger(Heap), trigger2(this)}  (vals1(Heap, this) == vals2(Heap, this)));
// (3)    
// axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals2(Heap, this)));

procedure test(Heap:HeapType, this:ref)
{
  assume trigger1(this); assume heap_trigger(Heap);

  assert (vals2(Heap, this) == vals3(Heap,this));
}

Answer 1

第一个问题:

在预处理步骤中，Z3 简化了琐碎的断言。断言assert t1 == t1简化为 assert true .因此，术语 t1 E 匹配引擎不考虑。绝招assert f(t1)是制作术语的标准之一 t1可用于 Z3 的 E 匹配。
Z3 中当前的预处理器“不够聪明”，无法删除不相关的断言 assert f(t1) .当然， future 版本的 Z3 可能会有更好的预处理器，这个技巧将不再适用。

对于第二个问题和第三个问题，最好有(小)Z3 脚本产生所描述的行为。

编辑。
我分析了你问题中的例子。事实证明这是Z3中的一个错误。我修复了该错误，该修复将在 Z3 4.1 中可用。
感谢您花时间缩小示例的大小。对此，我真的非常感激。在更大的实例中找到这个错误需要“永远”。
E 匹配引擎缺少一些实例。
该问题会影响包含多模式的 Z3 脚本，这些多模式使用不会出现在任何一元模式中的函数符号 f。
多模式也应该发生在地面 f 应用之前。
此外，必须禁用 MBQI 引擎。默认情况下，Boogie 禁用 MBQI 引擎。
在这种情况下，可能会错过多模式的实例。
这个错误在 E 匹配引擎中存在了很长时间。我认为它从未被发现有两个原因:

1- 不影响稳健性(Z3 不会产生错误答案，但会产生“未知”答案)

2- MBQI 引擎“补偿”任何丢失的实例。

关于为e-matching提供附加条件的额外命令，我们可以通过以下方式进行模拟。
命令 add_term(t)只是 (assert (add_term t)) 的语法糖.
即使我们实现了一个预处理器来消除只出现正(或负)的谓词符号，它也不会消除保留的谓词符号 add_term .因此，即使我们添加了这个预处理器，这个技巧也会继续工作。