0

I think I don't understand how BitVecs work in z3. I have written the following code:

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

I'd expect that this to be "unsat", because there are values inside and outside this range. But when I run s.check(), I get:

>>> s.check()
sat

This was confusing to me, so I guessed there was overflow involved. But then I tried:

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

Which confuses me a lot, because it suggests that z3 can model this number using 32 bit BitVecs. Additionally I ran:

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

Which confused me even more, because it seems clearly incompatible with the second example...

4

1 回答 1

4

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

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

于 2017-07-12T21:29:25.927 回答