Сумма всех битов в битовом векторе 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))

Конечно, журнал (п) бит результата будет достаточно, если вы предпочитаете.

Answer 2

Страница:

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

имеет различные алгоритмы для подсчета битов; который, я полагаю, может быть переведен на Z3/Python с относительной легкостью.

Мой любимый: https://graphics.stanford.edu/~seander/bithacks.html#CountBitsSetKernighan

который имеет приятное свойство, что она закругляется столько раз, сколько там установлены биты на входе. (Но вы не должны экстраполировать его на любую значимую метрику сложности, так как вы выполняете арифметику в каждом цикле, что может быть дорогостоящим. То же самое верно для всех этих алгоритмов.)

Сказав это, если ваш ввод полностью символический, вы не можете обыграть простой итеративный алгоритм, так как вы не можете сократить количество итераций. Вышеуказанные методы могут работать быстрее, если вход имеет конкретные биты.