z3 - Is there any function readily available for calculating logarithm to the base 2 in Z3/cvc4?

Question

I want to prove a simplification which involves calculating log to the base 2. Is there any function available in z3/cvc4 for calculating it?

Answer 1

简短的回答是，这两种工具都不能直接支持整数。对于无界整数，存在通过固定常数进行 Presburger 取幂的决策过程。由此您可以构造对数函数（反之亦然）。我不是专家，但我的理解是这些都相当复杂。了解更多信息：

• http://www.logique.jussieu.fr/~point/papiers/Pres.pdf
• http://dx.doi.org/10.2307/2586704
• https://mathoverflow.net/questions/103896/beyond-presburger-arithmetic

我不知道这些算法的任何现有实现。

对于有界整数，即 [a,b] 中的 x，其中 a 和 b 是数字，没有求解器特定的支持，但您可以对此建模。首先，您创建一个整数排序的 skolem 常量 s。然后，您使用断言强制解释 s：

(and (=> (2^0 <= x < 2^1)  (= s 0))
     (=> (2^1 <= x < 2^2)  (= s 1))
     ...
     (=> (2^i <= x < 2^{i+1}) (s = i)) ; for all 2^i in [a,b] and i >= 0.
)

如果 x <= 0（我认为这是合理的），这会使 s 无法解释。这是非常不令人满意的，但它是线性的。（如果有人知道更好的编码，我很想知道！）您还可以使用有界或无界整数的量词对上述公理进行编码。您首先使用量词将函数 2^i 编码为未解释的函数。然后使用 2^i 函数指定日志函数。这可能会导致求解器返回未知数，如果您沿着这条路走，您可能需要使用量词模块的求解器选项。

对于位向量，您需要确定数字是有符号还是无符号。对于长度为 k 的无符号值，您可以使用右移进行模拟。

(=> (bvugt x (_ bv0 k)))  (= (bvlshr x s) (_ bv1 k))

同样 x <= 0 (unsigned) 未被解释。有符号位向量类似：

(=> (bvsgt x (_ bv0 k)))  (= (bvlshr x s) (_ bv1 k))

Answer 2

顺便说一句，Alive 确实有一个 log2(foo) 函数。它使用类似于 Tim 给出的线性编码。