我想证明一种简化方法，其中涉及计算以2为底的对数。z3 / cvc4中是否有任何函数可用于计算它？
简短的答案是，两种工具都不直接支持整数。对于无界整数，存在通过固定常数进行Presburger求幂的决策程序。由此可以构造对数函数（反之亦然）。我不是专家，但我的理解是这些非常复杂。欲获得更多信息：
我不知道这些算法的任何现有实现。
对于有界整数，即[a，b]中的x，其中a和b是数字，没有求解器特定的支持，但是您可以对此建模。首先，您创建一个整数类型的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.
)
如果x <= 0（我认为是合理的），这将使s无法解释。这是非常不令人满意的，但是它是线性的。（如果有人知道更好的编码，我很想知道！）您还可以使用有界或无界整数的量词对上述公理进行编码。首先使用量词将函数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))
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句