c++ - 创建常量位 vector

Question

我是 Z3 的新手，正在尝试使用它的位 vector C++ API。据我所知，类上下文中的方法 bv_val(int n, unsigned sz) 旨在创建一个大小为 sz 且值为 n 的位 vector 。但是为什么值 n 被限制为 int 类型？。如果我用一个值创建一个大小为 10 的位 vector 会发生什么，例如超过 2^64 ?

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

Answer 1

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 上下文对象。