z3py：Pythonの数学関数でbitvecをキャストする方法は？

Question

私はbitvecの実際に使用されている長さを計算したいと思います。例えば、我々は00101100のようなbitvecを持っており、次のように実際に使用長さはとにかく、私はz3pyのコードを最も右側の1の位置の点では6を持っている：

from z3 import * 
import math 
def length(t): 
return int(math.ceil(math.log(t,2))) 

をよく私ならば、整数を入力として使用してください。実際には純粋なPythonコードなので、問題はありません。私はその後、

x = BitVecVal(31,8) 
print length(x) 

を使用する場合は、インスタンスが何の属性フロートを持っていないとして、私は問題を抱えて。私はz3_mk_bv2int、またはToInt（）を試しました。しかし、誰も働いていませんでした。

私はそれを並べ替えることができますか、それはz3pyでは許可されていません。

Answer 1

私は、これが「公式」の方法であるわからないんだけど、あなたは文字列表現を取得し、整数にそれを解析することができます

x = BitVecVal(42, 8) 
value = int(str(x)) 
print value, type(value) 

42 <type 'int'>