z3 - ビットベクトルに負の数を表示するには?

Question

タイトルがすべてを物語っています。-1 を次のように提示しようとします: (_ bv-1 32)、および z3 は文句を言います。

3x - 5y <= 10ビットベクトルなどの制約を提示するにはどうすればよいですか? 何らかの理由で、線形整数を使用したくありません。

Answer 1

これは通常、2 の補数エンコーディングによって行われます。ショートバージョンは、

-x = flip(x) + 1

whereflip(x)は のすべてのビットを単純に反転しますx。