2

Z3 で muZ を使用していますが、この新しい一般化された PDR があります。PDR アルゴリズムに関するデータを取得するにはどうすればよいか考えています。PDR アルゴリズムの不変条件は次のとおりです。

I => F_0
F_i => F_{i+1} for 0 <= i < k
F_i => P for 0 <= i <= k
F_i /\ T => F'_{i + 1}

終了時の k の値に非常に興味があります。この統計は何らかの方法で入手できますか? クエリで :print-statistics true を有効にすると表示されません。

(query (p x) :print-statistics true)
4

1 に答える 1

5

統計機能は現在、PDR についてあまり詳しく説明していません (これを指摘してくれてありがとう)。この時点で、冗長モードで実行することにより、追加情報を取得できます。反復カウントを stderr ストリームに出力します。

例えば：

z3.exe bakery.smt2 /v:1
Entering level 1
Entering level 2
Entering level 3
Entering level 4
Entering level 5
Entering level 6
.... followed by inductive assertions ...
于 2012-09-27T03:17:04.257 に答える