specmanでuintの設定ビット数をカウントするにはどうすればよいですか？

Question

Specmanのuintの設定ビット数をカウントしたい：

var x: uint;
gen x;
var x_set_bits: uint;
x_set_bits = ?;

これを行う最良の方法は何ですか？

Answer 1

Specmanはわかりませんが、これを確認した別の方法は少し安っぽく見えますが、効率的な傾向があります。256要素の配列を保持します。配列の各要素は、その値に対応するビット数で構成されます。例（擬似コード）：

bit_count = [0, 1, 1, 2, 1, ...]

したがって、bit_count 2 ==1。これは、バイナリの値2に単一の「1」があるためです。ビット。同様に、bit_count [255] == 8。

次に、uintをバイトに分割し、バイト値を使用してbit_count配列にインデックスを付け、結果を追加します。擬似コード：

total = 0
for byte in list_of_bytes
    total = total + bit_count[byte]

編集

この問題は、 Beautiful Code の本に記載されています。ヘンリー・S・ウォーレンによる章。また、Matt Howellsは、ビット数を効率的に計算するC言語の実装を示しています。 こちらをご覧ください回答。

Answer 2

私が見た方法の1つは次のとおりです。

x_set_bits = pack(NULL, x).count(it == 1);

pack（NULL、x）は、 x をビットのリストに変換します。
count はリストに作用し、条件が満たされるすべての要素をカウントします。この場合、条件は、要素が1に等しいことです。これは、設定ビット数になります。