z3 - 如何计算 Z3 中位向量的以 2 为底的对数？

Question

是否有任何函数可以让 z3 直接计算位向量的对数？

否则我怎样才能有效地实现对数？

Answer 1

我认为您最好的选择是将其编码为 if-then-else 链，本质上是一个查找表。假设base-2，你会有类似的东西（假设lg 0 = 0）：

(ite (< x 2) 0
     (ite (< x 4) 1
          (ite (< x 8) 2
           .... etc ...

由于对数增长缓慢，对于 32 位向量等，您只需要 32 个分支。其他基数类似。您可以轻松地自动生成此代码。