Z3 Python乘以两个位向量

Question

我想用Python + Z3位向量做一些计算，并且我在multiply操作中遇到了一些问题。

例如：

a = BitVecVal(3, 2) 
b = BitVecVal(3, 2) 
c = a * b 
print c.size() <----- output is 2; but can I have a vector of length 2 + 2 = 4?? 

print simplify(c) <---- of course, the output is 1, not 9 

上面的例子应该是很清楚的。我真的很感激，如果任何人都可以教育我如何在位矢量上进行乘法而不削减某些最高位。

谢谢！

Answer 1

尝试乘以之前延长了位向量的长度：

from z3 import * 

    a = BitVecVal(3, 2) 
    b = BitVecVal(3, 2) 
    c = ZeroExt(2, a) * ZeroExt(2, b) 
    print c.size() 

    print simplify(c)