我有两个不同大小的变量“a”和“b”，见下文。我有几个问题：
（1）如何将'a'的值复制到'b'？（即扩展操作）
（2）如何将'b'的值复制到'a'？（即截断操作）
谢谢。
a = BitVec('a', 1)
b = BitVec('b', 32)
问问题
1892 次
1 回答
9
对于扩展，我们使用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)
于 2013-01-29T15:05:25.600 回答