如何使用BitVector建模带符号整数？

Question

假设a是值为254的8位整数。如果a是一个有符号的整数，那么它实际上被认为是-2。相反，如果a未签名，它仍然是254。

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

非常感谢。

Answer 1

Z3具有的符号和无符号的解释的API。 例如，在C API中，Z3_mk_bvslt创建的是带符号的小于Z3_mk_bvult的未经签名的。在Z3Py中，我们使用签名的方式重载了<,<= ...。为了创建，未签名的a < b，我们必须使用ULT(a,b)。这里是无符号运算符的列表：ULE（<=），ULT（<），UGE（>=），UGT（>），UDiv（无符号除法），URem（无符号的剩余部分）。你可以在这里找到更多的信息：

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

Answer 2

你是正确的观察位矢量值不带符号。另一方面，有位矢量操作和关系的签名版本。 因此，您可以将相同的位矢量实体作为有符号或无符号数字对待，只要将它们传递给有符号或无符号的比较（带符号或无符号的符号）或带符号或无符号的运算符号。其他算术运算在签名和未签名实体上的工作方式相同。例如，无论您想将它们解释为有符号还是无符号，添加都会以相同方式移动位。

Z3遵循SMT-LIB2理论的约定，你可以对这些发现大量文件：http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2