Подсчитайте их в BitVec в Z3 с форматом ввода данных

Question

Существует ли компактный способ подсчета количества битов, которые установлены в 1 в BitVec в Z3, с использованием формата ввода данных?

$ z3 -h  # most of the lines below omited for clarity
Input format:
  -dl         use parser for Datalog input format.

В настоящее время принятый ответ на этот вопрос: Подсчитать ответы в BitVec в Z3 с форматом ввода SMT 2 утверждает, что нет хорошего способа сделать это в формате ввода SMT 2.

В настоящее время принятый ответ на этот вопрос: Сумма всех битов в битовом векторе Z3 показывает, как это сделать в Python.

Answer 1

Для векторов 32 bit вы можете попытаться перевести следующий псевдокод в SMT:

v = v - ((v >> 1) & 0x55555555);                    // reuse input as temporary
v = (v & 0x33333333) + ((v >> 2) & 0x33333333);     // temp
c = ((v + (v >> 4) & 0xF0F0F0F) * 0x1010101) >> 24; // count

Это называется Bit Twiddling Hack и также было размещено здесь .