创建一个常量位向量

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

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

来源

2013-06-26 Ta Thanh Dinh

从什么时候开始超过2^64？ –

我不知道'Z3'，但我猜测并说“不要填充超过容量的东西”。问题是“你想达到什么？”。我们可能会帮助你 – stefan

关于是否以位或字节（或其他）指定大小有困惑？ –

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

来源

2013-06-26 19:32:37

非常感谢您的回答。我不知道还有'expr bv_val（char const * n，unsigned sz）'''方法。 –

很可能，你会得到这个问题的唯一答案是“因为开发人员这么做”。

我们真的只能表示计算机科学中的有限量。在设计API时，有时候会出现问题，应该是什么东西的最大值或最小值。在这种情况下，n的最大值似乎为UINT_MAX（该函数有一个unsigned int过载）。

也许开发人员认为n > UINT_MAX是不现实的用例。没有人在他们的正确思想中会尝试。

也许是因为执行n > UINT_MAX的操作对资源过于重要（耗时太长，内存太多）。

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

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

最有可能的，这是因为有人认为：“够好”。无论如何，这个问题不能真正回答。

来源

2013-06-26 18:23:30

创建一个常量位向量

回答

相关问题