(_ 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) 是一个位向量常量，以 32 位编码值 0。

您可以在“位向量常量”下的逻辑定义中找到正式描述http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV