Z3 的位向量中所有位的总和 [英] Sum of all the bits in a Bit Vector of Z3

问题描述

给定 Z3 中的一个位向量，我想知道如何总结这个向量的每个位?

Given a bit vector in Z3, I am wondering how can I sum up each individual bit of this vector?

例如，

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

是否有任何预先实现的 API/函数支持这一点?谢谢！

Is there any pre-implemented APIs/functions that support this? Thank you!

推荐答案

它不是位向量运算的一部分.您可以按如下方式创建表达式:

It isn't part of the bit-vector operations. You can create an expression as follows:

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))

当然，如果您愿意，结果的 log(n) 位就足够了.

Of course, log(n) bits for the result will suffice if you prefer.

这篇关于Z3 的位向量中所有位的总和的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！