5

假设它a是一个 8 位的整数 value 254。如果a是有符号整数，则实际上被认为是-2。相反，如果a是无符号的，它仍然是254。

我试图用 Z3 用 BitVector 理论来模拟这个有符号/无符号整数问题，但似乎 BitVector 不允许这样做。这是真的？那么关于如何在 Z3py 中建模的任何想法？

非常感谢。

4

2 回答 2

10

Z3 具有用于有符号和无符号解释的 API。例如，在 C API 中，Z3_mk_bvslt创建有符号的小于和Z3_mk_bvult无符号的小于。在 Z3Py 中，我们重载了<, <=, ... 使用有符号的。为了创建 unsigned a < b，我们必须使用ULT(a,b). 以下是无符号运算符的列表：( ULE) <=、ULT( <)、UGE( >=)、UGT( >)、UDiv(无符号除法)、URem(无符号余数)。您可以在这里找到更多信息：

http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html

于 2013-07-24T16:09:28.760 回答
5

您正确地观察到位向量值不带符号。另一方面，有符号版本的位向量操作和关系。因此，您可以将相同的位向量实体视为有符号或无符号数，方法是将它们传递给有符号或无符号比较（有符号少/无符号少）或有符号或无符号运算（有符号除法/无符号除法）。其他算术运算在有符号和无符号实体上的工作方式相同。例如，无论您想将它们解释为有符号还是无符号，加法都会以相同的方式移动位。

Z3 遵循 SMT-LIB2 理论的约定，您可以在以下网址找到大量文档：http ://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2

于 2013-07-24T16:09:09.453 回答