ビットベクトルZ3の全ビットの和

Question

Z3のビットベクトルが与えられた場合、どのようにしてこのベクトルの各ビットを集計できますか？

例えば、

a = BitVecVal(3, 2) 
sum_all_bit(a) = 2 

は、これをサポートする任意の事前実装されたAPI /機能はありますか？ありがとうございました！

Answer 1

ビットベクトル演算の一部ではありません。次のように あなたは式を作成することができます：あなたが好む場合

もちろん

def sub(b): n = b.size() bits = [ Extract(i, i, b) for i in range(n) ] bvs = [ Concat(BitVecVal(0, n - 1), b) for b in bits ] nb = reduce(lambda a, b: a + b, bvs) return nb

print sub(BitVecVal(4,7))

、結果のログ（n）ビットで十分です。

Answer 2

ページ：

https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetNaive

のビットをカウントするための様々なアルゴリズムを有します。比較的簡単にZ3/Pythonに変換することができます。

私のお気に入りです：入力のビットが設定されているとして、それが何回ループの素敵な性質を持っているhttps://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetKernighan

。 （ただし、各ループで算術演算を行うのと同じように、それを意味のある複雑さのメトリックに外挿する必要はありません。これらのアルゴリズムはすべて同じです）。

あなたの入力が完全な象徴的なものであれば、反復回数を短縮できないので、単純な反復アルゴリズムを打ち破ることはできません。上記のメソッドは、入力に具体的なビットがある場合、より高速に動作する可能性があります。