Z3中的触发问题

Question

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

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

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

assert t1 == t1;

然后t1 not 似乎被用作量化公理的触发器。我明确添加了这一行，以便提供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。因此，E 匹配引擎不考虑术语t1。技巧assert f(t1) 是使术语t1 可用于Z3 的电子匹配的标准方法。 Z3 中当前的预处理器还不够“聪明”，无法删除不相关的断言assert f(t1)。当然，未来版本的 Z3 可能会有更好的预处理器，而这个技巧将不再适用。

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

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

1-不影响健全性（Z3不会产生错误答案，而是“未知”答案）

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

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