z3 - Z3py：如何扩展和截断变量？

Question

我有两个不同大小的变量“a”和“b”，见下文。我有几个问题：

（1）如何将'a'的值复制到'b'？（即扩展操作）

（2）如何将'b'的值复制到'a'？（即截断操作）

谢谢。

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

Answer 1

对于扩展，我们使用ZeroExtor 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)“分配”一个布尔变量，其值为sizep的位向量，反之亦然。该公式只是说明当且仅当is时为真。这是一个示例（也可在此处在线获得）x1p == (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)