```///////////////////////////////////////////////////////////////////////////////
//
// Alphametics are word arithmetic problems where each letter is replaced
// by a unique digit 0-9.  This means that no two letters are assigned the
// same values and no two digits are assigned to the same letter. Additionally,
// the initial letter of the word cannot be 0. Sometimes an additional
// requirement of a single solution is specified.
//
// Some popular alphametics are:
//      send + more = money
//      donald + gerald = robert
//      cross + roads = danger
//      who + is + this = idiot
//      this + isa + great + time = waster
//
// The predicate Alphametic in the code below can find all solutions for any
// alphametic. The predicate accepts two arguments:
//
//       list of strings to be added, for example ('send','more',Nil)
//       resulting string ('money')
//
// The strings themselves can be in upper or lower case, deep down in the bowels
// of the predicate they are all converted to lower case.
//
// Some examples:
//
// all Alphametic(('send','more',Nil),'money')
// all Alphametic(('who','is','this',Nil),'idiot')
// all Alphametic(('Winter', 'is', 'windier', 'summer', 'is',Nil), 'sunnier')
// all Alphametic(('Romans','also','more', 'or', 'less', 'added',Nil), 'letters')
// all Alphametic(('donald','gerald',Nil),'robert')
// all Alphametic(('this','isa','great','time',Nil),'waster')
//
// The code for the predicate Alphametic is quite straightforward. It was created
// as a generalization of a code for a single hardcoded alphametic
//
//     and + to + all + a + good = night
//
// The code for the above problem is in the predicate GoodNight and it is
// also present in this file for reference purposes, possibly clarifying some
// points of the predicate Alphametic.
//
///////////////////////////////////////////////////////////////////////////////

// Define some local types

local Digit09 = L[0..9]                     // number between 0..9
local WordVars = [0..]->Digit09             // array of numbers between 0..9
local Map = arr:[0..25]->I,lettersused:I    // structure used to count letters

pred Alphametic(strings:<list S,sum:<S) iff

// Map has 26 values, one for each letter of alphabet. -1 neans letter not used,
// otherwise it is an index of the letter in the order of appearance.

map :.Map & map :=
([-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1,-1],0) &

// Having initialized the map, count the number of different letters used
// in all strings.

CountVars(strings,sum,map) &

// Define an array of variables, one for each letter used.

v::[0..]->>Digit09 & Len(v,map.lettersused) &

maxlen = Len(sum) & // the length of the longest string
wall::[0..]->WordVars & Len(wall,Len(strings)) &

// Using the map, convert strings to arrays, assign a variable for each letter and
// pad the arrays to the same lengths (maxlen)

ListToVars(strings,wall,v,map,maxlen,0) &
StringToVars(res,sum,v,map,maxlen) &

// Define some additional variables (remainders and carries)

r1::[0..]->L[0..] & Len(r1,maxlen) &
c1::[0..]->L[0..] & Len(c1,maxlen+1) & c1(0) = 0 & c1(maxlen) = 0 &

// Set up constraints between the variables

SumAllColumns(wall,res,r1,c1,0) &

// Print one result

PrintResult(wall,res,0)

///////////////////////////////////////////////////////////////////////////////
//
// Helper routines
//
///////////////////////////////////////////////////////////////////////////////

// Sum all columns af all arrays.
local pred SumAllColumns(wall::[0..]->WordVars,res::WordVars,r1::[0..]->L[0..],
c1::[0..]->L[0..],ix:<I) iff
if ix < Len(res) then
SumColumns2(wall,res,r1,c1,ix) & SumAllColumns(wall,res,r1,c1,ix+1)
end

local pred SumColumns2(wall::[0..]->WordVars,res::WordVars,r1::[0..]->L[0..],
c1::[0..]->L[0..],column:<I) iff
SumOneColumn(wall,0,sumout,column,0) &
sumout + c1(column) = r1(column) &
res(column) = r1(column) mod 10 & c1(column+1) = r1(column) / 10

// sumout = wall(i,column) + wall(i+1,column) +...wall(Len(wall)-1,column)
local pred SumOneColumn(wall::[0..]->WordVars,sumin::L,sumout::L, column:<I,i:<I) iff
if i < Len(wall) then
SumOneColumn(wall,sumin + wall(i,column),sumout,column,i+1)
else
sumout = sumin
end

///////////////////////////////////////////////////////////////////////////////
//
// Routines for a formatted output of results.
//
///////////////////////////////////////////////////////////////////////////////
local proc PrintResult(w:<[0..]->WordVars,res:<WordVars,i:<I) iff
if i < Len(w) then
PrintNumString(w(i)) & PrintResult(w,res,i+1)
else
Print('\n -------') &
PrintNumString(res) &
Print('\n')
end

local proc PrintNumString(w:<WordVars) iff
Print('\n ') & PrintNumString1(RtlReverse(w),1,0)

local proc PrintNumString1(w:<WordVars,blank:<I,i:<I) iff
if i < Len(w) then
if w(i) = 0 & blank = 1 then
Print(' ') & PrintNumString1(w,1,i+1) {don't print leading zeros}
else
Print(w(i)) & PrintNumString1(w,0,i+1)
end
end

///////////////////////////////////////////////////////////////////////////////
// Go thru all strings and count all letters used. Update the letter map
// accordingly.
///////////////////////////////////////////////////////////////////////////////
local pred CountVars(strings:<list S,sum:<S,map:.Map) iff
if strings = h,t then
CountVarsInOneString(RtlToLowerString(h),map,0) & CountVars(t,sum,map)
end &
CountVarsInOneString(RtlToLowerString(sum),map,0)

///////////////////////////////////////////////////////////////////////////////
// Given a string and a map of characters, mark all used characters in the map.
//
///////////////////////////////////////////////////////////////////////////////
local pred CountVarsInOneString(s:<S, map:.Map,i:<I) iff
if i < Len(s) then
if map.arr(s(i)-"a") = -1 then {if character not encountered yet}
map.arr(s(i)-"a") := map.lettersused & map.lettersused := map.lettersused+1
end & CountVarsInOneString(s,map,i+1)
end

///////////////////////////////////////////////////////////////////////////////
//
// Having a map of used letters and an array of variables, assign a variable
// for each letter (same letters will use the same variable).
// Convert strings to lower case.
// Create arrays of variables based on the string letters.
// Assure the first character of the string is never 0.
// Pad unused array of variable entries with zeros.
//
///////////////////////////////////////////////////////////////////////////////
local pred ListToVars(strings:<list S,wall::[0..]->WordVars,v::[0..]->>Digit09,map:.Map,maxlen:<I,i:<I) iff
if strings = h,t then
StringToVars(wall(i),h,v,map,maxlen) & ListToVars(t,wall,v,map,maxlen,i+1)
end

local pred StringToVars(w::WordVars,s:<S,v::[0..]->>Digit09,map:.Map,maxlen:<I) iff
Len(w,maxlen) & StringToVars1(w,RtlToLowerString(RtlReverse(s)),v,map,maxlen,0)

local pred StringToVars1(w::WordVars,s:<S,v::[0..]->>Digit09,map:.Map,maxlen:<I,i:<I) iff
if i < maxlen then      // for all array elements
if i < Len(s) then
w(i) = v(map.arr(s(i)-"a")) &
if i = Len(s) -1 then w(i) <> 0 end // first string character cannot represent zeros
else
w(i) = 0        // pad with zeros if array longer than the string
end & StringToVars1(w,s,v,map,maxlen,i+1)
end

///////////////////////////////////////////////////////////////////////////////
// The following code solves a hardwired alphametic:
//
//      AND
//  +    TO
//  +   ALL
//  +     A
//  +  GOOD
//    -----
//    NIGHT
//
// The code is here for illustration purposes, as it is quite easy to follow
// the steps used to solve the problem.
//
// By generalizing the specialized code we would eventually derive all the
// above code for the predicate Alphametic and all supporting routines.
//
// To execute this code, issue the query
//
//      all GoodNight()
//
///////////////////////////////////////////////////////////////////////////////

pred GoodNight() iff

// Nine variables used, corresponding to nine letters used : a,n,d,t,o,l,g,i,h
// They must be all different.

v::[0..]->>Digit09 & Len(v,9) & v = [a,n,d,t,o,l,g,i,h] &
wall::[0..]->[0..4]->Digit09 & Len(wall,5) & // five strings added

// Break individual strings into letters. Reverse them and pad them all with zeros
// up to the length of the longest (i.e.resulting) string, in our case 'night'.
// Note we don't want any leading zeroes, therefore the letters "a","t","g","n"
// are explicitely declared as non-zero

wall(0) = [d,n,a,0,0] & a <> 0 &
wall(1) = [o,t,0,0,0] & t <> 0 &
wall(2) = [l,l,a,0,0] & a <> 0 &
wall(3) = [a,0,0,0,0] & a <> 0 &
wall(4) = [d,o,o,g,0] & g <> 0 &

// Break down the "result" string into letters, same procedure as for the previous
// strings:

res ::[0..]->Digit09 & res = [t,h,g,i,n] & n <> 0 &

// The above steps are generalized for a list of strings in the routine
//  ListToVars(strings,wall,v,map,maxlen,0) &

r1::[0..]->L[0..] & Len(r1,Len(res)) &  {array of remainders, one for each column}

// Array of carries, one for each column. The first one is guaranteed to be zero.
// This way we can treat all columns eaqually

c1::[0..]->L[0..] & Len(c1,Len(res)+1) & c1(0) = 0 &

// Set up the constraints by specifying the relations between individual variables:
//
//     d + o + l + a + d      = t1 & t = t1 mod 10 & c1 = t1 / 10 &
//     n + t + l     + o + c1 = h1 & h = h1 mod 10 & c2 = h1 / 10 &
//     a     + a     + o + c2 = g1 & g = g1 mod 10 & c3 = g1 / 10 &
//                     g + c3 = i1 & i = i1 mod 10 & c4 = i1 / 10 &
//                         c4 = n  &

// By renaming the variables the above relations can be expressed as follows:

wall = [w0,w1,w2,w3,w4] &

w0(0) + w1(0) + w2(0) + w3(0) + w4(0) + c1(0) = r1(0) & res(0) = r1(0) mod 10 & c1(0+1) = r1(0) / 10 &
w0(1) + w1(1) + w2(1) + w3(1) + w4(1) + c1(1) = r1(1) & res(1) = r1(1) mod 10 & c1(1+1) = r1(1) / 10 &
w0(2) + w1(2) + w2(2) + w3(2) + w4(2) + c1(2) = r1(2) & res(2) = r1(2) mod 10 & c1(2+1) = r1(2) / 10 &
w0(3) + w1(3) + w2(3) + w3(3) + w4(3) + c1(3) = r1(3) & res(3) = r1(3) mod 10 & c1(3+1) = r1(3) / 10 &
w0(4) + w1(4) + w2(4) + w3(4) + w4(4) + c1(4) = r1(4) & res(4) = r1(4) mod 10 & c1(4+1) = r1(4) / 10 &

// All the above columns adding can be replaced by a single call "SumAllColumns(wall,res,r1,c1,0)",

// We are done, print the result:

Print('\n')     &
Print('   ',  a,n,d, '\n') &
Print('    ',   t,o, '\n') &
Print('   ',  a,l,l, '\n') &
Print('     ',    a, '\n') &
Print('  ', g,o,o,d, '\n') &
Print(' -----\n') &
Print(' ',n,i,g,h,t, '\n')

```