c++ - 为什么 Z3 BitVec 对象没有运行时大小信息？

Question

我正在使用不同大小的 Z3 bitvecs，并且正在研究一种减轻工作量的方法。我将在创建 z3 表达式之前从对象中获取信息，所以这实际上不是一个重要问题，但我想知道为什么 z3 bitvecs 不携带运行时大小信息。

Answer 1

您当然可以查询sort每个 z3 AST 术语的 ，然后获取bvs 的大小；所以，是的，它们确实带有尺寸信息以及您需要知道的几乎所有信息。

相关的电话是：

• 获取排序
• bv_size

API 文档有无数其他要求仔细检查术语的不同部分，请参见此处。