Z3py:如何扩展和截断变量？

Question

我有两个不同大小的'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)"分配"布尔变量p,其值为x大小的位向量,1反之亦然.该公式p == (x == 1)只是声明p当且仅当x是的时候是真的1.这是一个例子(也可以在这里在线获得)

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)