如何用BitVector对有符号整数进行建模？

Question

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

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

非常感谢。

Answer 1

Z3有用于签署和未签署解释的API。例如，在C中，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 2理论的惯例，您可以在：http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2上找到关于这些理论的详细文档。