【发布时间】：2017-02-01 01:45:01
【问题描述】：
我注意到这是一些 SMT2 基准测试，(_ bv0 32)、(_ bv16 32)、... 等符号的使用如下：
QF_FP/schanda/spark/zeros_consistent_2.smt2
但是，这并不是在理论声明中引用此类符号：
http://smtlib.cs.uiowa.edu/theories.shtml
对此有何评论？它们的含义是什么？
谢谢！
【问题讨论】：
【发布时间】：2017-02-01 01:45:01
【问题描述】：
(_ bv0 32) 是将值 0 编码为 32 位的位向量常量。
您可以在“位向量常量”http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV下的逻辑定义中找到正式的描述
【讨论】：
-
谢谢。在逻辑中存在这些结构很奇怪，但在理论中却没有