Is there any function readily available for calcul

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?

回答1:

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.

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.
)

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.

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))

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

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

回答2:

Alive does have a log2(foo) function btw. It uses a linear encoding similar to the one given by Tim.