【发布时间】：2014-04-23 13:48:52
【问题描述】：
使用 C++ API，如何从模型中提取位向量常量的十进制值。
【问题讨论】：
标签： z3
【发布时间】：2014-04-23 13:48:52
【问题描述】：
有几个 C-Function 允许您提取不同类型的值，具体取决于数字的预期大小：Z3_get_numeral_int、Z3_get_numeral_uint、Z3_get_numeral_uint64、Z3_get_numeral_int64。对于不适合这些基本类型的数字，我们可以使用Z3_get_numeral_string 函数来获取可以解析为您喜欢的大整数表示的字符串表示形式。
请注意，这些函数是 C 函数，而不是 C++ 函数，但是这两个 API 可以很好地混合。 （参见例如z3 C++ API & ite）。
【讨论】：
-
感谢您的建议。写
int val; Z3_get_numeral_int(bv.ctx(), bv, &val);之类的东西就可以了。