私は最近、Z3 でトリガーに関していくつかの動作を観察しましたが、これは理解できません。残念ながら、これらの例は大きな Boogie ファイルからのものであるため、ここでは抽象的に説明して、明白な答えがあるかどうかを確認したいと思います。ただし、具体的なファイルの方がよい場合は、添付できます。
基本的に 3 つの問題がありますが、3 番目の問題は 2 番目の問題の特殊なケースかもしれません。私の理解では、どの動作も期待されていませんが、何かが欠けている可能性があります。どんな助けでも大歓迎です！
まず、トリガーに関する限り、私のプログラムの些細な等式は無視されるようです。たとえば、t1が量化された公理のパターンに一致する項である場合、Boogie プログラムに次の形式の行を追加すると、
assert t1 == t1;
thent1は、定量化された公理のトリガーとして使用されないようです。証明者にトリガーとして提供するために、明示的に行を追加しましたt1。これは、Boogie プログラムでよく実行します。
代わりに、追加の機能を導入すると、
function f(x : same_type_as_t1) : bool
{ true }
代わりに行を追加します
assert f(t1);
私のプログラムでは、t1 Z3によってトリガーとして使用されているようです。私は以前のプログラムの Z3 翻訳をチェックしましたが、(些細な) 等価性t1は Boogie 翻訳を生き延びました (つまり、Boogie が巧妙なことをしようとしているわけではありません)。
第二に、二次パターンがうまく機能していないようです。たとえば、1 つの公理が次の形式を持つプログラムがあります。
axiom (forall ... :: {t1,t2} {t3,t4,t5} ..... );
t3, t4そして、t5すべてが発生した状況。明らかに公理がインスタンス化されていないため、プログラムは検証に失敗します。ただし、公理を次のように書き直すと、
axiom (forall ... :: {t3,t4,t5} {t1,t2} ..... );
次に、プログラムが検証します。どちらの場合も、Boogie を実行する時間は約 3 秒で、パターンは Z3 出力まで存続します。
3 番目:これは 2 番目の問題の症状である可能性がありますが、次の動作に驚きました。
私は次の形式の公理を書きました
axiom (forall .. :: {t1,t2} .... );
axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );
t2とが発生した状況ではt3、最初の公理はインスタンス化されませんでした (2 番目の公理のインスタンス化後に発生するので、そうなると予想していましたt1)。ただし、次のように書き直すと、
axiom (forall .. :: {t2,t3} {t1,t2} .... );
axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving t1... );
次に、最初の公理がインスタンス化されました。ただし、何らかの理由で二次パターンが一般的に使用されていない場合は、この動作も説明できます。
明示的な例が役立つ場合は、確かに長いものを添付して、それらを少し削減することができます (ただし、もちろん、トリガーの問題は少しデリケートなので、例を小さくしすぎると動作が失われる可能性があります)。
アドバイスをよろしくお願いします！
アレックス・サマーズ
編集:上記の 2 番目と 3 番目の動作を部分的に示す例を次に示します。ここでは読みやすくするために Boogie コードを添付しましたが、Z3 入力をコピーするかメールで送信することもできます。元の Boogie コードのほとんどすべてを削除しましたが、動作を完全に失わずに単純化するのは難しいようです。
以下のコードは、すでに元の例とは微妙に異なる動作をしていますが、十分に近いと思います。基本的に、以下の (1) とラベル付けされた公理は、2 番目のパターン セットを一致させることができません。公理 (1) をコメントアウトし、代わりに (現在コメントされている) 公理 (2) と (3) に置き換えると、これらは 2 つのパターン セットのそれぞれを含む元のコピーにすぎません。プログラムは検証します。実際、この特定のケースでは、公理 (2) があれば十分です。元のコード (切り詰める前) では、公理 (1) の 2 つのパターン セットの順序を反転するだけで十分でしたが、私の小さな再現コードではそうではないようです。
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));
}