Z3 파이썬 두 비트 벡터 곱하기

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)