// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  Knight's Tour
//
//  The problem is to find a path for a Knight on a (N)x(N) chessboard,
//  such that every field is visited exactly once. It is known that
//  there is a Hamilton circuit (a Knight's Tour where start and end
//  points are identical) iff N>=6 and N is even.
//
//  A Knight's Tour can be easily obtained by divide and conquer
//  algorithms or heuristics like Warnsdorff's rule (from 1823).
//  For further references see the PDF files.
//
// **************************************************************************

macro N = 4;

module KnightsTour(
    bv{3} move,
    [N][N()]bool q,
    nat{N} x, y
) {
    x = 1;
    y = 0;
    always {
        q[x][y] = true;
        case
            (move==0b000) do {
                if(x>=2 & y>=1)
                    if(!q[x-2][y-1]) {
                        next(x) = x-2;
                        next(y) = y-1;
                    }
            }
            (move==0b001) do {
                if(x>=1 & y>=2)
                    if(!q[x-1][y-2]) {
                        next(x) = x-1;
                        next(y) = y-2;
                    }
            }
            (move==0b010) do {
                if(x<N-1 & y>=2)
                    if(!q[x+1][y-2]) {
                        next(x) = x+1;
                        next(y) = y-2;
                    }
            }
            (move==0b011) do {
                if(x<N-2 & y>=1)
                    if(!q[x+2][y-1]) {
                        next(x) = x+2;
                        next(y) = y-1;
                    }
            }
            (move==0b100) do {
                if(x<N-2 & y<N()-1)
                    if(!q[x+2][y+1]) {
                        next(x) = x+2;
                        next(y) = y+1;
                    }
            }
            (move==0b101) do {
                if(x<N-1 & y<N()-2)
                    if(!q[x+1][y+2]) {
                        next(x) = x+1;
                        next(y) = y+2;
                    }
            }
            (move==0b110) do {
                if(x>=1 & y<N-2)
                    if(!q[x-1][y+2]) {
                        next(x) = x-1;
                        next(y) = y+2;
                    }
            }
            (move==0b111) do {
                if(x>=2 & y<N-1)
                    if(!q[x-2][y+1]) {
                        next(x) = x-2;
                        next(y) = y+1;
                    }
            }
            default
                nothing;
    }
} satisfies {
    spec[DisProveA] : assert
        ! E F forall(i=0..N-1) forall(j=0..N()-1) q[i][j];
}