我最近在 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) 中两个模式集的顺序也足够了，但在我的小型复制中似乎不再是这种情况。
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));
}