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 位的位向量常量。

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