CODEWITHSUNDEEP
z3smt
Robert
Robert

Reputation: 211

How to calculate logarithm base 2 to Bitvectors in Z3?

Is there any function in which z3 calculate directly the logarithm to Bitvectors?

Otherwise how can I implement the logarithm efficiently?

Upvotes: 0

Views: 295

Answers (1)

alias
alias

Reputation: 30450

I think your best bet is to code it up as an if-then-else chain as essentially a look-up table. Assuming base-2, you'd have something like (assuming lg 0 = 0):

(ite (< x 2) 0
     (ite (< x 4) 1
          (ite (< x 8) 2
           .... etc ...

Since logarithm grows slowly, you'd only need 32 branches for 32-bit vectors, etc. Other bases would be similar. You can easily generate this code automatically.

Upvotes: 1

Related Questions