bitvectorに負の数を表示するにはどうすればよいですか？

Question

タイトルはそれをすべて言っています。私は次のように-1を提示しようとします：(_ bv-1 32)、そしてz3が文句を言う。

3x - 5y <= 10などの制約をビットベクトルにどのように表示するのですか？何らかの理由で、私は線形整数を使いたくない。

Answer 1

これは通常two's complement encodingによって行われます。ショートバージョンは、flip(x)は単にxのすべてのビットを反転

-x = flip(x) + 1 

あります。