 ```{

The Problem of the Tanks

one of Clif Pickover's Extreme Challenges

You are a tank traveling (up, down, left, right and diagonally) through electric fields.
If you travel through two - signs in a row, your battery is drained and you are stuck.
If you travel through two + signs in a row, your battery overcharges and explodes.
How can you travel from Start to End through every cell once and survive?

- + - + -
+ + - - +
- + + + S
- + E - -
- + + - +

Run the query

all TankTour()

}

local Symbol = P | M | B | E  //"Plus","Minus","Beginning","End"

local Map :<[0..4]->[0..4]->Symbol =
[[M,P,M,P,M],
[P,P,M,M,P],
[M,P,P,P,B],
[M,P,E,M,M],
[M,P,P,M,P]]

local Board = [0..4]->[0..4]->I

pred TankTour() iff
pos:.Board & Dupl(5,Dupl(5,0),pos) &      //Intialize all position as 0 (not visited)
pos (2,4) := 1 &                          //First step is placing the tank at the beginning
TankTour1(pos,2,4,2) &                    //Calculate the rest of the steps (starting at step 2)
PrintFormattedSolution(pos,0)             //Simple formatted printout of the solution
// (starting at row 0)

local pred TankTour1(pos:.Board,row:<I,col:<I,step:<I)  iff
if step <= Len(pos)*Len(pos(0)) then        // there are as many moves as board elements
MoveTank(row,col,newrow,newcol) &
// If the position is not visited yet, we'll assign the step number to it.
// (Otherwise the test for position = 0 fails and forces a backtrack)
// If the newcol, newrow are outside the arena, we'll get a backtrack as well.
pos(newrow,newcol) = 0 &

// We make sure that we landed on a different square then the last one
Map(newrow,newcol) <> Map(row,col) &

// Only the very last step can land on the End position
if step = Len(pos)*Len(pos(0)) then
Map(newrow,newcol) = E
else
Map(newrow,newcol) <> E
end &

// If we got here, then the newcol,newrow are on the board and were never visited.
// So we mark the place as visited and continue with trying to find the next move
pos(newrow,newcol) := step &
TankTour1(pos,newrow,newcol,step+1)
end

local pred MoveTank(row:<I,col:<I,newrow:>I,newcol:>I) iff

//  Given a tank at position row,col (marked 't'), the tank can
//  move to eight different places:
//
//  +---+---+---+---+
//  |   |   |   |   |
//  +---+---+---+---+
//  | 1 | 2 | 3 |   |
//  +---+---+---+---+
//  | 8 | T | 4 |   |
//  +---+---+---+---+
//  | 7 | 6 | 5 |   |
//  +---+---+---+---+
//  |   |   |   |   |
//  +---+---+---+---+

newcol =  col - 1 & newrow = row - 1 | // 1
newcol =  col     & newrow = row - 1 | // 2
newcol =  col + 1 & newrow = row - 1 | // 3
newcol =  col + 1 & newrow = row     | // 4
newcol =  col + 1 & newrow = row + 1 | // 5
newcol =  col     & newrow = row + 1 | // 6
newcol =  col - 1 & newrow = row + 1 | // 7
newcol =  col - 1 & newrow = row       // 8

// Print the double array "pos" as a matrix of M rows by N columns, with each position
// formatted to two digits (no leading zeros)

local proc PrintFormattedSolution(pos:<Board,row:<I) iff
if row < Len(pos) then
Print('\n') & PrintOneRow(pos(row),0) & PrintFormattedSolution(pos,row+1)
end

local proc PrintOneRow(r:<[0..]->I,col:<I) iff
if col < Len(r) then
if r(col) < 10 then
Print(' ')
end &
Print(r(col),' ') & PrintOneRow(r,col+1)
end

```