 ```{                     N x N Queens
By asking the query "all Queens(n)" all solutions to the n x n queens
are computed and displayed.

The basic data structure is a dynamically allocated symbolic array 'pos' of
the type Board. The relation
pos(r) = c
means that the queen in the row r is in the column c.

The array pos is allocated in the predicate Queens to be of the
size specified by the argument by specifying the constraint:
Len(pos,size)

Some solutions:

Queens(8)  :     92 solutions (     914 backtracks)
...
Queens(11) :   2680 solutions (   89393 backtracks)
Queens(12) :  14200 solutions (  467802 backtracks)
Queens(13) :  73712 solutions ( 2600469 backtracks)
Queens(14) : 365596 solutions (15419300 backtracks)
Queens(15) :2279184 solutions (96699767 backtracks)
...

}

Nl :<S = '\n'
Board = [0..]->[0..]                        {flexible array of col. positions}

pred Queens(size:<[1..]) iff
pos::Board & Len(pos,size) &             {symbolic flexible array pos}
Queens1(pos,0)                           {find a solution into pos}
& Present(0,pos)                         {display the solution in pos}

pred Queens1(pos::Board,row:<I)  iff
{ the partial solution [0..row-1] in pos can be extended to [0..Len(pos] }
if row < Len(pos) then                    {row r is not set}
pos(row) < Len(pos) &                   {constraint on the max column}
NoAttack(row,pos,row - 1) &             {queen r does not attack [0..r-1]}
Queens1(pos,row + 1)                    {set the remaining queens}
end

pred NoAttack(r:<I,pos::Board,i:<I) iff
{ the queen in the row r does not attack queens in [0..i] }
if i >= 0 then
pos(r) <> pos(i) &                      {r and i not in the same column}
pos(r)+r <> pos(i)+i &                  {r and i not in same \ diagonal }
pos(r)+i <> pos(i)+r &                  {r and i not in same / diagonal }
NoAttack(r,pos,i - 1)                   {r does not attack [0..i-1] }
end

proc Present(row:<I,pos:< Board) iff        {display a solution}
if row < Len(pos) then
Print('\n      ') &
Onerow(0,pos(row),Len(pos)) &
Present(row+1,pos)                     {tail recursion: compiled as loop}
end

proc Onerow(c:<I,qpos:<I,size:<I) iff       {display one row of a solution}
if c < size then
if c <> qpos then Print('.') else Print('*') end &
Print(' ') &
Onerow(c+1,qpos,size)
end

```