4

Z3 の QBVF ソルバーをいじっていて、存在するアサーションから値を抽出できるかどうか疑問に思っています。つまり、私が次のものを持っているとしましょう：

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

これは基本的に、「最小」の 16 ビット符号なし値があることを示しています。次に、私は言うことができます：

(check-sat)
(get-model)

Z3-3.0 は喜んでこう答えます。

sat
(model  (define-fun x!0 () (_ BitVec 16)
#x0000)
)

これは本当にクールです。しかし、私がやりたいのは、get-value を介してそのモデルの一部を抽出できるようにすることです。当然のことながら、次のいずれも機能していないようです

(get-value (x))
(get-value (x!0))

いずれの場合も、Z3 は当然、そのような定数はないと不平を言います。(check-sat)呼び出しへの応答によって証明されるように、Z3 がその情報を持っていることは明らかです。get-valueまたは他のメカニズムを介して、存在する値に自動的にアクセスする方法はありますか?

ありがとう..

4

1 に答える 1

4

Z3get-valueでは、ユーザーは「グローバル」宣言のみを参照できます。存在変数xはローカル宣言です。したがって、を使用してアクセスすることはできませんget-value。デフォルトでは、Z3 は「スコーレム化」と呼ばれるプロセスを使用して存在変数を排除します。アイデアは、存在する変数を新しい定数と関数シンボルに置き換えることです。たとえば、式

exists x. forall y. exists z. P(x, y, z)

に変換されます

forall y. P(x!1, y, z!1(y))

z の選択は y に依存する可能性があるため、z は関数になることに注意してください。ウィキペディアにskolem 標準形に関するエントリがあります。

そうは言っても、あなたが説明した問題に対する満足のいく解決策は見つかりませんでした。たとえば、数式には、同じ名前のさまざまな存在変数が含まれている場合があります。get-valueそのため、コマンド内の各インスタンスを明確な方法で参照する方法が明確ではありません。

この制限の可能な回避策は、スコーレム化ステップを「手動で」適用するか、少なくとも値を知りたい変数に適用することです。例えば、

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

は次のように書かれています。

(declare-const x (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y x)))
(check-sat)
(get-value x)

存在変数が次のような全称量指定子にネストされている場合:

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x))))
(check-sat)
(get-model)

新しい skolem 関数を使用して、xfor eachの値を取得できますy。上記の例は次のようになります。

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)

この例でsxは、 は fresh 関数です。Z3 によって作成されたモデルは、 の解釈を割り当てsxます。バージョン 3.0 では、解釈は恒等関数です。この関数を使用して、xfor eachの値を取得できますy。

于 2011-08-24T20:40:18.830 に答える