z3 中的 BitVecs 可以表示哪些值？

Question

我想我不明白 BitVecs 在 z3 中是如何工作的。我写了下面的代码：

>>> import z3
>>> s = z3.Solver()
>>> a = z3.BitVec("a", 32)
>>> s.add(z3.ForAll(a, z3.Not(z3.And(a > 2147483647, a < 2147484671))))

我希望它是 "unsat"，因为这个运行ge 内外都有值。但是当我运行 s.check() 时，我得到：

>>> s.check()
sat

这让我感到困惑，所以我猜测其中涉及溢出。但后来我尝试了：

>>> b = z3.BitVec("b", 32)
>>> s = z3.Solver()
>>> s.add(b == 2147484671)
>>> s.check()
sat
>>> s.model()
[b = 2147484671]

这让我很困惑，因为它表明 z3 可以使用 32 位 BitVecs 为这个数字建模。另外我运行:

>>> s = z3.Solver()
>>> c = z3.BitVec("c", 32)
>>> s.add(z3.And(c > 2147483647, c < 2147484671))
>>> s.check()
unsat

这让我更加困惑，因为它似乎与第二个示例明显不兼容...

Answer 1

运算符 > 和 < 已签名。 2147484671 在解释为 32 位数字时是一个负数。这就是你的约束不满足的原因。您可以使用 UGT/ULT 而不是 >/< 来忽略符号位。

底线：位向量表示数字，但您需要知道您正在使用的操作的符号是什么。在PythonAPI中，所有运算符重载都是有符号运算。

What values can be represented with BitVecs in z3?