<分区>
我正在处理不同大小的 Z3 bitvecs，我正在研究一种减轻工作量的方法。我将在创建 z3 表达式之前从一个对象获取信息，因此这实际上不是一个重要问题，但我想知道为什么 z3 bitvecs 不携带运行时大小信息。
<分区>
我正在处理不同大小的 Z3 bitvecs，我正在研究一种减轻工作量的方法。我将在创建 z3 表达式之前从一个对象获取信息，因此这实际上不是一个重要问题，但我想知道为什么 z3 bitvecs 不携带运行时大小信息。
最佳答案
您当然可以查询每个 z3 AST 术语的 sort，然后获取 bv 的大小；所以，是的，它们确实带有尺寸信息以及几乎所有您需要知道的信息。
相关调用是:
API 文档有无数其他要求来仔细检查术语的不同部分，请参阅 here .
关于c++ - 为什么 Z3 BitVec 对象没有运行时大小信息？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/57493819/