z3でBitVecでどのような値を表現できますか？

Question

私はBitVecがz3でどのように機能するのか分かりません。この範囲内と外の値があるので、私は、これは「UNSAT」であることをことを期待

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

：私は、次のコードを書かれています。しかし、私はs.check()を実行したときに、私が取得：

>>> s.check() 
sat 

これは私に混乱しているので、私は関与オーバーフローがあったと推測しました。しかし、私は試しました：

z3が32ビットBitVecを使用してこのモデルをモデル化できることを示唆しているので、私は多くを混乱させます。さらに、私は走った：それは第二の例と明確に互換性がないようなので、もっと私を混同

>>> 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を使用して、符号ビットを無視することができます。

ボトムライン：ビットベクトルは数値を表しますが、使用している演算の符号が何であるかを知る必要があります。 Python APIでは、演算子のオーバーロードはすべて符号付き演算です。