I have a system of equations to solve in which there is some equations of hamming weight. Hamming weight is generally the number of 1's in binary representation of a number. I tried to solve in Z3 SMT Solver, but it outputs an error stating " b'there is no current model". I am trying to find a 32-bit number with a given hamming weight and some equations.
In examples below, I am trying to find a number(0 to 2^5-1) with hamming weight equal to 3.
from z3 import *
s = Solver()
K = [BitVec('k%d'%i,5) for i in range(3)]
Eq = [K[0]&0x1 + K[0]&0x2 + K[0]&0x4 + K[0]&0x8 + K[0]&0x10 == 3] #
s.add(Eq)
s.check()
print(s.model())
This gives error "b'there is no current model".
Can anyone help me regarding this problem?
Edit: I put the hamming equation wrong; It will be
Eq = [(K[0]&0x1) + ((K[0]&0x2)>>1) + ((K[0]&0x4)>>2) + ((K[0]&0x8)>>3) + ((K[0]&0x10)>>4) == 3 ]
Thanks
It's the operator precedence in Python. This works:
Eq = [(K[0]&0x1) + (K[0]&0x2) + (K[0]&0x4) + (K[0]&0x8) + (K[0]&0x10) == 3]
However, you're not actually computing the hamming weight this way. Each of the terms needs to be shifted. E.g. K[0]&0x8 is not zero or one, but 0x8 or 0x0.