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

Question

假设这a是一个8位值的整数254.如果a是有符号整数,则实际考虑它-2.相反,如果a是未签名的,它仍然存在254.

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

非常感谢.

Answer 1

Z3具有用于签名和未签名解释的API.例如,在C API中,Z3_mk_bvslt创建signed signed和Z3_mk_bvultunsigned.在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