在Z3触发问题

Question

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

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

首先：在我的程序琐碎的等式似乎就触发关切地被忽略。例如，如果t1是应该匹配的模式进行量化公理，如果我加一条线的形式我的不羁程序

​​

然后t1不不似乎习惯作为触发一个术语用于量化的公理。我明确添加了该行，以便提供t1作为证明者的触发器，我经常在Boogie程序中执行此操作。

如果不是我引入一个额外的功能，说

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

和现在，而不是添加一行

assert f(t1); 

到我的程序，然后t1确实似乎被用来作为触发Z3。我已经检查过前一个程序的Z3翻译，并且t1上的（平凡的）等式确实存在于布吉翻译中（即，这不是布吉试图做一些聪明的事情）。

其次：辅助模式似乎不能正常工作。例如，我有一个计划，其中一个公理的形式

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

和一种情况，即t3, t4和t5都发生了。该程序未能验证，显然是因为该公理没有实例化。但是，如果我将公理改写为

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

然后程序验证。在这两种情况下，运行Boogie的时间大约是3秒，模式生存到Z3输出。

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

我写形式的公理

​​

，并在发生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）和（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)); 
} 

Answer 1

第一个问题：

琐碎的断言通过Z3中的预处理步骤简化。断言assert t1 == t1简化为assert true。因此，术语t1不被E匹配引擎考虑。技巧assert f(t1)是使术语t1可用于Z3的电子匹配的标准技巧。 Z3中的当前预处理器不够“足够聪明”以去除不相关的断言assert f(t1)。当然，Z3的未来版本可能会有更好的预处理器，而且这个技巧不再适用。

对于第二个和第三个问题，这将是不错的产生描述的行为（小）Z3脚本。

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

1，不影响稳健（Z3不会产生一个错误的答案，但“未知”的答案）

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

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