Alphametic Solver

from z3 import *
import string

# Solve the alphametic with following pattern
#    SEND + MORE = MONEY

def create_term_sum(charmap, term):
    rev_term = list(reversed(term))
    result = charmap[rev_term[0]]

    coeff = 10
    for i in range(1, len(rev_term)):
        result = result + coeff*charmap[rev_term[i]]
        coeff *= 10
    return result

def print_term(model, charmap, term):
    line = "{} = {}"
    left = term
    right = ""
    for i in range(len(term)):
        right += "{}".format(model[charmap[term[i]]])
    print(line.format(left, right))


if __name__ == '__main__':
    sentence = input('Enter equation: ')

    while sentence != "EXIT":
        charmap = {}
        solver = Solver ()

        # Declare variables, actually map of characters and Z3 Ints
        print("*** Split the setence ***")
        sequence = "".join(filter(lambda c: c.isupper(), set(sentence)))
        for char in sequence:
            charmap[char] = Int(char)

        # Make all character disctinct
        print("*** Applying distinct ***")
        solver.add(Distinct(list(charmap.values())))

        # Make all character in correct range
        print("*** Applying range ***")
        for item in charmap.values():
            solver.add(And(0 <= item, item <= 9))

        # Create constraints
        # SEND + MORE = MONEY
        # left = [SEND, MORE]
        # right = MONEY
        left, right = sentence.replace(' ','').split('=')
        left = left.split('+')

        # But for the first in each term should not be 0
        for term in left:
            solver.add(And(0 < charmap[term[0]], charmap[term[0]] <= 9))
        solver.add(And(0 < charmap[right[0]], charmap[right[0]] <= 9))

        solver.add(sum([create_term_sum(charmap, term) for term in left]) == create_term_sum(charmap, right))

        print("*** Solving ***")
        if solver.check() == sat:
            model = solver.model()
            for term in left:
                print_term(model, charmap, term)
            print("---------------------")
            print_term(model, charmap, right)

        sentence = input('Enter equation: ')