是否有任何函数可用于计算 Z3/cvc4 中以 2 为底的对数? [英] Is there any function readily available for calculating logarithm to the base 2 in Z3/cvc4?

问题描述

我想证明一个简化，它涉及计算以 2 为底的对数.z3/cvc4 中是否有任何函数可用于计算它?

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?

推荐答案

简而言之，这两种工具都无法直接支持整数.对于无界整数，存在通过固定常数对 Presburger 取幂的决策程序.由此您可以构造对数函数(反之亦然).我不是专家，但我的理解是这些非常复杂.欲了解更多信息:

The short answer is that support is unavailable directly for integers in either tool. For unbounded integers, decision procedures for Presburger exponentiation by a fixed constant exist. From this you can construct the logarithm function (or vice versa). I am not an expert but my understanding is that these are quite complicated. For more information:

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

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

I am unaware of any existing implementation of these algorithms.

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

For bounded integers, i.e. x in [a,b] where a and b are numerals, there is not solver specific support, but you can model this. First you create a skolem constant s of sort Integer. You then force the interpretation of s using an assertion:

(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 函数指定 log 函数.这很可能会导致求解器返回未知数，如果您沿着这条路走下去，您可能需要为量词模块使用求解器选项.

This leaves s uninterpreted if x <= 0 (which I think is reasonable). This is very unsatisfactory, but it is linear. (If someone knows a better encoding, I'd love to know about it!) You can also encode the above axioms using quantifiers for bounded or unbounded integers. You first encode the function 2^i as an uninterpreted function using quantifiers. You then specify the log function using the 2^i function. This is likely to result in the solver returning unknown, and you while likely need to play with solver options for quantifier modules if you go down this path.

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

For bitvectors, you need to decide if the numbers are signed or unsigned. For unsigned values of length k, you can simulate this using right shift.

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

再次 x <= 0(无符号)是未解释的.有符号位向量是类似的:

Again x <= 0 (unsigned) is uninterpreted. Signed bitvectors are similar:

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

这篇关于是否有任何函数可用于计算 Z3/cvc4 中以 2 为底的对数?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！