z3 - (_ bv0 32)、(_ bv1 16) ... SMT2 ベンチマークでの意味

Question

いくつかの SMT2 ベンチマークでは(_ bv0 32)、 、(_ bv16 32)、 ... などの表記が次のように使用されていることに気付きました。

QF_FP/schanda/spark/zeros_consistent_2.smt2

http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev_xstrcoll_mtime.il.wp.smt2

http://rise4fun.com/Z3/e1s

ただし、これは理論宣言内のそのような記号への参照ではありません。

http://smtlib.cs.uiowa.edu/theories.shtml

それについて何かコメントはありますか？それらの意味は何ですか？

ありがとう ！

Answer 1

(_ bv0 32) は、値 0 を 32 ビットでエンコードするビットベクトル定数です。

「Bitvector Constants」の下のロジック定義で正式な説明を見つけることができますhttp://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV