Cryptarithmetic Solver

Description
Cryptarithms are a kind of mathematical puzzle. Each puzzle consists of a basic equation of arithmetic (involving addition, subtraction, division, etc.) with words, where each letter represents a different digit. The goal of the puzzle is to find the correct number substitution for each letter in order to make a valid equation.

This classic example (taken from the wikipedia page) was first published in 1924:

    S E N D
+   M O R E
_______________
  M O N E Y
The solution to this puzzle is:

O = 0,
M = 1,
Y = 2,
E = 5,
N = 6,
D = 7,
R = 8,
and S = 9.

(i.e. 9567 + 1085 = 10652)

Note: Leading zeroes are not allowed in a valid solution.

Task
You will be given a cryptarithm in string form. Your task is to output the letters and corresponding numbers which make up a valid solution to the puzzle.

For the purposes of this challenge, all equations will consist only of addition.

Leading zeroes (in a multi-digit number) are not allowed in a valid solution.

The input is guaranteed to be a valid cryptarithm.

Example
Input:
"THIS + IS + HIS == CLAIM"

Output:
{"A"=>7, "C"=>1, "H"=>8, "I"=>5, "L"=>0, "M"=>6, "S"=>2, "T"=>9}

Challenge Input
"WHAT + WAS + THY == CAUSE"

"HIS + HORSE + IS == SLAIN"

"HERE + SHE == COMES"

"FOR + LACK + OF == TREAD"

"I + WILL + PAY + THE == THEFT"
Output
{"A"=>0, "C"=>1, "E"=>4, "H"=>2, "S"=>3, "T"=>6, "U"=>7, "W"=>9, "Y"=>5}

{"A"=>1, "E"=>8, "H"=>3, "I"=>5, "L"=>0, "N"=>6, "O"=>9, "R"=>7, "S"=>4}

{"A"=>6, "C"=>7, "D"=>3, "E"=>2, "F"=>5, "K"=>8, "L"=>9, "O"=>4, "R"=>0, "T"=>1}

{"A"=>2, "E"=>4, "F"=>7, "H"=>0, "I"=>8, "L"=>3, "P"=>5, "T"=>1, "W"=>9, "Y"=>6}
Bonus
A bonus solution can solve one of the longest known alphametics in a reasonable amount of time:

"TEN + HERONS + REST + NEAR + NORTH + SEA + SHORE + AS + TAN + TERNS + SOAR + TO + ENTER + THERE + AS + HERONS + NEST + ON + STONES + AT + SHORE + THREE + STARS + ARE + SEEN + TERN + SNORES + ARE + NEAR == SEVVOTH"

"SO + MANY + MORE + MEN + SEEM + TO + SAY + THAT + THEY + MAY + SOON + TRY + TO + STAY + AT + HOME +  SO + AS + TO + SEE + OR + HEAR + THE + SAME + ONE + MAN + TRY + TO + MEET + THE + TEAM + ON + THE + MOON + AS + HE + HAS + AT + THE + OTHER + TEN == TESTS"

"THIS + A + FIRE + THEREFORE + FOR + ALL + HISTORIES + I + TELL + A + TALE + THAT + FALSIFIES + ITS + TITLE + TIS + A + LIE + THE + TALE + OF + THE + LAST + FIRE + HORSES + LATE + AFTER + THE + FIRST + FATHERS + FORESEE + THE + HORRORS + THE + LAST + FREE + TROLL + TERRIFIES + THE + HORSES + OF + FIRE + THE + TROLL + RESTS + AT + THE + HOLE + OF + LOSSES + IT + IS + THERE + THAT + SHE + STORES + ROLES + OF + LEATHERS + AFTER + SHE + SATISFIES + HER + HATE + OFF + THOSE + FEARS + A + TASTE + RISES + AS + SHE + HEARS + THE + LEAST + FAR + HORSE + THOSE + FAST + HORSES + THAT + FIRST + HEAR + THE + TROLL + FLEE + OFF + TO + THE + FOREST + THE + HORSES + THAT + ALERTS + RAISE + THE + STARES + OF + THE + OTHERS + AS + THE + TROLL + ASSAILS + AT + THE + TOTAL + SHIFT + HER + TEETH + TEAR + HOOF + OFF + TORSO + AS + THE + LAST + HORSE + FORFEITS + ITS + LIFE + THE + FIRST + FATHERS + HEAR + OF + THE + HORRORS + THEIR + FEARS + THAT + THE + FIRES + FOR + THEIR + FEASTS + ARREST + AS + THE + FIRST + FATHERS + RESETTLE + THE + LAST + OF + THE + FIRE + HORSES + THE + LAST + TROLL + HARASSES + THE + FOREST + HEART + FREE + AT + LAST + OF + THE + LAST + TROLL + ALL + OFFER + THEIR + FIRE + HEAT + TO + THE + ASSISTERS + FAR + OFF + THE + TROLL + FASTS + ITS + LIFE + SHORTER + AS + STARS + RISE + THE + HORSES + REST + SAFE + AFTER + ALL + SHARE + HOT + FISH + AS + THEIR + AFFILIATES + TAILOR + A + ROOFS + FOR + THEIR + SAFE == FORTRESSES"

Solution
in C

#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include <string.h>

#define DELIM " \n\r"

enum op {OP_RET, OP_PUSH, OP_ADD, OP_MUL, OP_EQ};

static long
execute(const char *ops, const long *constants)
{
    long stack[8];
    long *top = stack;
    long a, b;
    for (;; ops++) {
        switch ((enum op)*ops) {
            case OP_RET:
                assert(top - stack == 1);
                return top[-1];
            case OP_PUSH:
                *top++ = constants[(int)*++ops];
                break;
            case OP_ADD:
                a = *--top;
                b = *--top;
                *top++ = a + b;
                break;
            case OP_MUL:
                a = *--top;
                b = *--top;
                *top++ = a * b;
                break;
            case OP_EQ:
                a = *--top;
                b = *--top;
                *top++ = a == b;
                break;
            default:
                abort();
        }
    }
    abort();
}

static char *
compile_word(char *ops, const char *word)
{
    int len = strlen(word);
    *ops++ = OP_PUSH;
    *ops++ = 9 + word[len - 1] - 'A';
    for (int i = 0; len > 1; i++) {
        *ops++ = OP_PUSH;
        *ops++ = word[i] - 'A' + 9;
        *ops++ = OP_PUSH;
        *ops++ = --len - 1;
        *ops++ = OP_MUL;
        *ops++ = OP_ADD;
    }
    return ops;
}

void
disassemble(char *ops)
{
    int i;
    for (;; ops++) {
        switch ((enum op)*ops) {
            case OP_RET:
                puts("ret");
                return;
            case OP_PUSH:
                i = *++ops;
                if (i >= 9)
                    printf("push %c\n", i + 'A' - 9);
                else
                    printf("push 10^%d\n", i + 1);
                break;
            case OP_ADD:
                puts("add");
                break;
            case OP_MUL:
                puts("mul");
                break;
            case OP_EQ:
                puts("eq");
                break;
            default:
                printf("INVALID:%d\n", *ops);
        }
    }
}

static long
solve(const char *vars, const char *ops, long *constants, unsigned avail)
{
    int v = *vars;
    if (!v) {
        return execute(ops, constants);
    } else {
        for (int i = 0; i < 10; i++) {
            unsigned bit = 1u << i;
            if (avail & bit) {
                constants[v - 'A' + 9] = i;
                long r = solve(vars + 1, ops, constants, avail & ~bit);
                if (r)
                    return r;
            }
        }
    }
    return 0;
}

int
main(void)
{
    char line[4096];
    fgets(line, sizeof(line), stdin);

    /* Compiled representation of the puzzle */
    char vars[11] = {0};
    int nvars = 0;
    static char program[1024UL * 1024];

    /* Compile puzzle into a program */
    enum op last = 0;
    char seen[26] = {0};
    char *ops = program;
    for (char *tok = strtok(line, DELIM); tok; tok = strtok(0, DELIM)) {
        switch (tok[0]) {
            case '+':
                last = OP_ADD;
                break;
            case '=':
                last = OP_EQ;
                break;
            default:
                for (char *c = tok; *c; c++) {
                    int i = *c - 'A';
                    if (!seen[i]) {
                        seen[i] = 1;
                        vars[nvars++] = *c;
                    }
                }
                ops = compile_word(ops, tok);
                if (last)
                    *ops++ = last;
                break;
        }
    }
    *ops = OP_RET;

    long constants[35] = {
        10, 100, 1000, 10000, 100000,
        1000000, 10000000, 100000000, 1000000000
    };
    if (solve(vars, program, constants, -1U))
        for (char *v = vars; *v; v++)
            printf("%c = %ld\n", *v, constants[*v - 'A' + 9]);
}