触发Z3中的问题

Question

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

基本上有三个问题,尽管第三个可能是第二个问题的特例.据我所知,没有任何行为是预期的,但也许我错过了一些东西.任何帮助将不胜感激!

首先:就触发而言,我的程序中的琐碎平等似乎被忽略了.例如,if 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)的公理不能使其第二个模式集匹配.如果我注释掉axiom(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));
}

Answer 1

第一个问题：

\n\n

Z3 在预处理步骤中简化了琐碎的断言。该断言assert t1 == t1被简化为assert true。t1因此， E 匹配引擎不考虑该术语。技巧assert f(t1)是为 Z3 提供可用于电子匹配的术语的标准技巧t1。\nZ3 中当前的预处理器“不够智能”，无法删除不相关的断言assert f(t1)。当然，未来版本的 Z3 可能会有更好的预处理器，这个技巧就不再起作用了。

\n\n

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

\n\n

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

\n\n

1-它不会影响健全性（Z3不会产生错误的答案，但会产生\xe2\x80\x9cunknown\xe2\x80\x9d答案）

\n\n

2-MBQI 引擎\xe2\x80\x9c 补偿\xe2\x80\x9d 任何丢失的实例。

\n\n

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

\n