Z3/cvc4中是否有任何函数可用于计算底数2的对数？

Question

我想证明一个简化，涉及计算日志到基地2.是否有任何可用于z3/cvc4计算它的功能？

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

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

对于有界整数，即x in [a，b]其中a和b是数字，没有解算器特定的支持，但可以对此进行建模。首先创建一个Integer类型的Skolem常量。然后，您使用断言力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. 
) 

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

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

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

再次x < = 0（无符号）未被解释。签名的位向量类似：

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

Answer 2

Alive确实有btw的log2（foo）函数。 它使用类似于Tim提供的线性编码。