意義（_ BV 0 32），（_ BV1 16）......在SMT2基準測試

Question

我注意到，一些SMT2基準，符號，如(_ bv0 32)，(_ bv16 32)，...，其用途，例如在：

QF_FP/schanda /火花/ 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）是一個位矢量常量，用32位對值0進行編碼。

您可以找到邏輯定義的形式化描述，在「位向量常量」 http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV