0

次のクエリがあります（SMT-LIB v1.0標準を使用して記述されています）。

(benchmark gametime
:status unknown
:logic QF_AUFBV
:extrafuns ((x  BitVec[32]))
:extrafuns ((a  Array[32:32]))
:extrapreds ((constraint1 ))
:extrapreds ((constraint0 ))
:formula
(flet ($x37 (and (iff constraint0 (= (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32]))))
(and $x37 (and constraint0 constraint1)))
)

（クエリは少し冗長ですが、自動的に生成されます。）

これをZ3で実行し、モデルを要求すると、次のようになります。

a -> as-array[k!0]
constraint1 -> true
x -> bv1[32]
constraint0 -> true
k!0 -> {
  bv0[32] -> bv0[32]
  else -> bv0[32]
}

必要に応じて「a」と「x」の値があるので、これは素晴らしいことです。ただし、1つの小さな変更を除いて、別のクエリも同様です。

(benchmark gametime
:status unknown
:logic QF_AUFBV
:extrafuns ((x  BitVec[32]))
:extrafuns ((a  Array[32:32]))
:extrapreds ((constraint1 ))
:extrapreds ((constraint0 ))
:formula
(flet ($x37 (and (iff constraint0 (**bvuge** (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32]))))
(and $x37 (and constraint0 constraint1)))
)

変更点が強調表示されます。同等であったものが「bvuge」チェックになりました。Z3から次のモデルを受け取ります。

constraint1 -> true
x -> bv1[32]
constraint0 -> true

「a」の割り当てはもうありません。これは意図的なものでしたか？モデルに存在しない場合に想定すべき変数の「デフォルト」値はありますか？（たとえば、ここでのデフォルト値は、配列「a」がどこでもゼロであるということです。）

価値のあることとして、この問題は、操作が「bvuge」である場合にのみ発生します。その他（「bvsge」、「bvugt」、「bvsgt」、「bvult」、「bvslt」、「bvule」、「bvsle」）は機能しているようです。

4

1 に答える 1

1

「a」の割り当てはもうありません。これは意図的なものでしたか？

はい、これは意図的なものです。配列の任意の値が式を満たします。これは、constraint0が原因です。

   (bvuge (select a bv0[32]) bv0[32]))

trueと同等です。符号なし比較では、ビットベクトル値は0以上です。したがって、「a」の値は関係ありません。

于 2013-01-24T20:26:04.413 に答える