z3 - Z3py: 変数を拡張して切り詰める方法は?

Question

サイズの異なる 2 つの変数 'a' と 'b' があります。以下を参照してください。いくつか質問があります:

(1) 'a' の値を 'b' にコピーするにはどうすればよいですか? (すなわち拡張操作)

(2) 'b' の値を 'a' にコピーするにはどうすればよいですか? (すなわち切り捨て操作)

ありがとう。

a = BitVec('a', 1)
b = BitVec('b', 32)

Answer 1

拡張には、ZeroExtまたはを使用しますSignExt。はZeroExt「ゼロ」を追加SignExtし、符号ビット（つまり最上位ビット）を「コピー」します。を使用する切り捨てではExtract、ビットの任意のサブシーケンスを抽出できます。これは小さな例です（rise4funでもオンラインで入手できます）。

a = BitVec('a', 1)
b = BitVec('b', 32)
solve(ZeroExt(31, a) == b)
solve(b > 10, Extract(0,0,b) == a)

編集：サイズのビットベクトルの値を使用p == (x == 1)してブール変数を「割り当てる」ために使用できます。その逆も可能です。公式は、がである場合にのみ、それが真であると述べているだけです。ここに例があります（ここからオンラインでも入手できます）px1p == (x == 1)px1

x = BitVec('x', 1)
p = Bool('p')

solve(p == (x == 1), x == 0)
solve(p == (x == 1), x == 1)
solve(p == (x == 1), Not(p))
solve(p == (x == 1), p)