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?
相关问题
- How to compute with Quaternion numbers in Z3?
- Z3 real arithmetics and data types theories integr
- Timeout for Z3 Optimize
- Adjusting `simplify` tactic in Z3
- How to setup a Java development environment for Z3
相关文章
- retrieve the matched model in Z3py?
- Simplex in z3 via for-all
- How do I get Z3 to return minimal model?
- How to get z3 to return multiple unsat cores, mult
- ld linking error while compiling z3
- Horn clauses in Z3
- Getting a “good” unsat-core with z3 (logic QF_BV)
- how to get multiple solutions for z3 solver in smt
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:
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:
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.
Again x <= 0 (unsigned) is uninterpreted. Signed bitvectors are similar:
Alive does have a log2(foo) function btw. It uses a linear encoding similar to the one given by Tim.