#!/usr/bin/env python3
from z3 import *

LENGHT=4

def try_NHASH(NHASH):
    ch=[BitVec('ch%d' % c, 32) for c in range(LENGHT)]
    h=[BitVec('h%d' % c, 32) for c in range(LENGHT)]

    MULTIPLIER=31

    s=Solver()

    for i in range(LENGHT):
        s.add(And(ch[i]>=0x20, ch[i]<=0x7E))

    s.add(h[0]==ch[0])
    for i in range(LENGHT-1):
        s.add(h[i+1]==MULTIPLIER*h[i]+ch[i+1])

    # BUG, because this is signed modulo:
    #s.add((h[LENGHT-1] % NHASH)==0)
    # this is unsigned modulo:
    s.add(URem(h[LENGHT-1], NHASH)==0)

    assert s.check()

    # enumerate all solutions:
    results=[]
    while s.check() == sat:
        m = s.model()

        t=[chr(m[ch[i]].as_long()) for i in range(LENGHT)]
        print ("".join(t))
        #for i in range(LENGHT):
        #    print ("0x%08x" % m[h[i]].as_long())

        results.append(m)
        block = []
        for d in m:
            t=d()
            block.append(t != m[d])
        s.add(Or(block))

    print ("solutions total", len(results))
    return len(results)

try_NHASH(65521)