// ==================================================================
// N queens are to be placed on a NxN chessboard so that no queen can
// attack another queen. It is known that there are no solutions for
// chessboards with N<=6.
// ==================================================================

#ifndef N
   #define N 5
#endif

spec Queen(bool q[N][N]) {
  s:
   not(
   // -- each row contains a queen -------------
     (forall(int[sizeOf(N-1)] i=0 .. (N-1))
         exists(int[sizeOf(N-1)] j=0 .. (N-1))
            q[i][j]
     )
     &
   // -- forbid row attacks --------------------
     (forall(int[sizeOf(N-1)] i=0 .. (N-1))
         forall(int[sizeOf(N-1)] j=0 .. (N-1))
            (q[i][j] ->
               forall(int[sizeOf(N-1)] k=1 .. (N-2))
                  !q[i][(j+k)%N])
     )
     &
   // -- forbid column attacks --------------------
     (forall(int[sizeOf(N-1)] i=0 .. (N-1))
         forall(int[sizeOf(N-1)] j=0 .. (N-1))
            (q[i][j] ->
               forall(int[sizeOf(N-1)] k=1 .. (N-2))
                  !q[(i+k)%N][j])
     )
     &
   // -- forbid diagonal attacks --------------------
     (forall(int[sizeOf(N-1)] i=0 .. (N-1))
         forall(int[sizeOf(N-1)] j=0 .. (N-1))
            (q[i][j] ->
               forall(int[sizeOf(N-1)] k=1 .. (N-2))
                  !q[(i+k)%N][(j+k)%N])
     )
     &
   // -- forbid diagonal attacks --------------------
     (forall(int[sizeOf(N-1)] i=0 .. (N-1))
         forall(int[sizeOf(N-1)] j=0 .. (N-1))
            (q[i][j] ->
               forall(int[sizeOf(N-1)] k=1 .. (N-2))
                  !q[(i+k)%N][(j-k)%N])
     )
   );
}