from z3 import *

def ascii_printable(x):
    return And(65<= x, x <= 122)

def generate_ascii_printable_string(base_name, size, solver):
    bytes = [BitVec('%s%d' % (base_name, i), 8) for i in range(size)]
    solver.add(And(map(ascii_printable, bytes)))
    return bytes

def str_to_BitVecVals8(s):
    return map(lambda x: BitVecVal(ord(x), 8),list(s))

def voyelleInterdit(solver,username,interdit):
    for i in range (0,len(username)):
        for j in range (0,len(interdit)):
            s.add(username[i]!=interdit[j])

def doublonInterdit(solver,username):
    for i in range (0,len(username)):
        for j in range (0,len(username)):
            if i != j:
                s.add(username[i]!=username[j])

def fixVoyelleInterdit(string, solver):
    username = generate_ascii_printable_string(string, len(string), s)
    for i in range(len(string)):
        s.add(username[i] == ord(string[i]))
    return username

def differentChar(solver,password,username):
    for i in range (0,len(password)):
        for j in range (0,len(username)):
            s.add(password[i] != username[j])

def croissant(solver,username):
    for i in range (0,len(username)-1):
        s.add(username[i] < username[i+1])

def decroissant(solver,password):
    for i in range (0,len(password)-1):
        s.add(password[i] > password[i+1])

def sameSizeBin(solver,username,password):
    s.add(sum([ord(i) for i in username]) == sum([ord(i) for i in password]))


for i in range (8,15):
    s = Solver()
    username = generate_ascii_printable_string("username",i,s)
    password = generate_ascii_printable_string("password",i,s)
    # s.add(len(username)!=len(password))

    interdit = fixVoyelleInterdit("aeiuoy",s)
    voyelleInterdit(s,username,interdit)
    voyelleInterdit(s,password,interdit)
    doublonInterdit(s,username)
    doublonInterdit(s,password)
    differentChar(s,password,username)
    croissant(s,username)
    decroissant(s,password)
    sameSizeBin(s,username,password)

    while s.check() == sat:
        m = s.model()
        s.add(([sym() != m[sym] for sym in m.decls()]))
        print 'username:' + ''.join(chr(m[i].as_long()) for i in username)
        print 'password:' + ''.join(chr(m[i].as_long()) for i in password)