from z3 import *

# hash functions
def rot_hash(s):
  h = 0
  for i in range(0,len(s)):
    h = (h << 4) ^ (h >> 28) ^ ord(s[i])
  return h

def shift_add_xor_hash(s):
  h = 0
  for i in range(0,len(s)):
    h = h ^ ((h << 5) + (h >> 2) + ord(s[i]))
  return h

# encoding stuff
def Iff(a,b):
  return And(Implies(a,b),Implies(b,a))

def zext(bits, num_bits):
  for i in range(0,num_bits - len(bits)):
    bits.insert(0,False)
  return bits

# character as bit vector of 32 bits
def mk_char(pre):
  vars = []
  for i in range(0, 7):
    vars.insert(0, FreshBool(pre + str(i)))
  return zext(vars,32)

# string of length n as bit vector of n * 32 bits
def mk_string(pre,l):
  s = []
  for i in range(0,l):
    s.append(mk_char(pre))
  return s

# define some strings
a = mk_string("a",4)
b = mk_string("b",4)