問題タブ [bitvector]

ビットベクトルとして表されるコレクションを扱っています。最後に、M & (N-1) のようなものを見ました。M と N はどちらもコレクションであり、どちらも空ではありません。

コレクションに関して、これの結果は何を意味しますか?

これら 2 つの関数のビット ロジックを理解できません。

1. 条件 (bitVector & mask) == 0 をチェックしている理由がわかりません。

2. また、条件が満たされたときに bitVector と mask を OR し、それ以外の場合は bitVector と ~mask を AND するのはなぜですか?

3. 「整数から 1 を減算し、それを元の整数と AND することによって、正確に 1 ビットが設定されていることを確認する」ことができるようなプロパティがあるのはなぜですか?

完全なコードはこちら。

BitVecs が z3 でどのように機能するかを理解していないと思います。私は次のコードを書きました：

この範囲の内外に値があるため、これは「unsat」であると予想されます。しかし、実行するs.check()と、次のようになります。

これは私を混乱させたので、オーバーフローが関係していると推測しました。しかし、私は試しました：

z3 が 32 ビット BitVecs を使用してこの数値をモデル化できることを示唆しているため、これは私を大いに混乱させます。さらに私は走った：

2番目の例とは明らかに互換性がないように見えるため、さらに混乱しました...

z3でのビット ベクトルの整数への変換(およびその逆)に関する投稿がいくつかあります。たとえば、ここ、 ここ、ここを参照してください。

ドキュメントによると、Z3_mk_bv2intは解釈されません。

「...この関数は本質的に解釈されないものとして扱われます。そのため、この関数で制約を解決するときに、Z3 がこの関数のセマンティクスを正確に反映するとは期待できません...」

ただし、 期待されるセマンティクスを反映していない単純な例は見つかりませんでした。たとえば、次のようなクエリを使用するときはいつでも:

正しい答えが得られました(インデックスは 7 のはずですが、7 です)

z3 の bv2intやint2bvが失敗する簡単な例を教えてください。ありがとう！