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

Why doesn't Z3 BitVec object have runtime size info?

本文关键字：信息 运行时 Z3 BitVec 对象 为什么      更新时间：2023-10-16

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

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

相关电话是：

  • get_sort
  • bv_size

API 文档有无数其他调用来仔细检查术语的不同部分，请参阅此处。

相关文章：