c++ - 创建一个常量位向量

Question

我对 Z3 非常陌生，并尝试使用它的位向量 C++ API。据我了解，类上下文中的方法 bv_val(int n, unsigned sz) 旨在创建一个大小为 sz 且值为 n 的位向量。但是为什么值 n 被限制为 int 类型？如果我创建一个大小为 10 且其值大于 2^64 的位向量会发生什么？

有人能给我一些建议吗？提前致谢。

Answer 1

Z3 C++ API 提供以下方法来创建位向量值。

    expr bv_val(int n, unsigned sz);
    expr bv_val(unsigned n, unsigned sz);
    expr bv_val(__int64 n, unsigned sz);
    expr bv_val(__uint64 n, unsigned sz);
    expr bv_val(char const * n, unsigned sz);

对于大小大于 UINTMAX64 的位向量值，我们必须使用字符串。例子：

    expr big = ctx.bv_val("1267650600228229401496703205376", 512);

其中ctx是 Z3 上下文对象。

Answer 2

很可能，您对这个问题的唯一答案是“因为开发人员做到了”。

我们实际上只能表示计算机科学中的有限量。在设计 API 时，有时会出现一个问题，即某事物的最大值或最小值应该是多少。在这种特殊情况下，最大值n似乎是UINT_MAX（unsigned int函数有过载）。

也许开发人员认为用例n > UINT_MAX是不切实际的。没有一个头脑正常的人会尝试它。

可能是因为执行操作n > UINT_MAX对资源的负担太重（花费了太长时间，太多的内存）。

也许是因为有一种方法可以将这种操作分成多个部分，使得无法在一个大通道中执行它不是问题。

或者也许有人只是没有考虑过，并且n > UINT_MAX确实存在通过的需要。在这种情况下，我相信您可以在他们的bug tracker上提交问题。

很可能，这只是因为有人认为：“足够好”。无论如何，这个问题无法真正回答。