c++ - 创建一个恒定的位 vector

我是Z3的新手，并尝试使用其位 vector C++ API。据我了解，类上下文中的方法bv_val(int n，unsigned sz)旨在创建大小为sz且值为n的位 vector 。
但是为什么将值n限制为int类型呢？如果我创建一个大小为10的带有值的位 vector 会怎样？大于2 ^ 64吗？

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

最佳答案

Z3 C++ API提供了以下用于创建位 vector 值的方法。

    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的位 vector 值，必须使用字符串。例:

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

其中ctx是Z3上下文对象。

关于c++ - 创建一个恒定的位 vector ，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/17326910/