是否有现成的函数计算Z3/cvc4 4中基数2的对数？

Question

我想证明一个简化，包括计算日志到基2。z3/cvc4 4中是否有任何函数可用于计算它？

Answer 1

简单地说，这两个工具中的整数都无法直接获得支持。对于无界整数，存在由一个固定常数进行普氏汉堡指数的判定过程。由此可以构造对数函数(反之亦然)。我不是一个专家，但我的理解是，这些是相当复杂的。有关详细信息，请参阅：

• 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(我认为这是合理的)，这就没有解释。这是非常不能令人满意的，但它是线性的。(如果有人知道更好的编码，我很想知道！)您还可以使用有界或无界整数的量词对上述公理进行编码。首先使用量词将函数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确实有一个log2(foo)函数。它使用类似于Tim给出的线性编码。