2

前の議論のフォローアップ：Z3：実存的なモデル値の抽出

違いはありますか？

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

と

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

Z3に関する限り？つまり、後者のQBVFソルバーを自動的に取得できますか？

また、実験の結果、私が発行した場合、次のことがわかりました。

(eval (sx #x8000))

電話の後(check-sat)、それはうまくいきます（これは素晴らしいです）。私も言うことができればもっと良いでしょう：

(eval (sx (get-value (y))))

残念ながら、そのクエリに対して、Z3はそれがであると文句を言いますinvalid function application。evalそのように機能を使う方法はありますか？

ありがとう！

4

1 に答える 1

2

スクリプト

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

と

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

同等ではありません。2番目は実際には

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y))))

コマンドに関しては、eval解釈されていない定数と関数記号を参照できます。したがって、次のように書くことができます。

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))
(check-sat)
(eval (sx y))

はユニバーサル変数であるため、このコマンド(eval (sx y))は最初のスクリプトでは機能しません。y

于 2011-09-09T14:08:09.223 に答える