// **************************************************************************
//
//    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
//
// **************************************************************************
//
// 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.
//
// **************************************************************************

macro N = 6;

module Queens( [N][N]bool q ) {
    nothing;
} satisfies {
    s [ProveA]: assert
    !(
        // -- each row contains a queen -------------
        ( forall(i=0..N-1) exists(j=0..N-1) q[i][j] )
     &
        // -- forbid row attacks --------------------
        ( forall(i=0..N-1) forall(j=0..N-1)
            (q[i][j] -> forall(k=1..N-1) !q[i][(j+k)%N])
        )
     &
        // -- forbid column attacks --------------------
        ( forall(i=0..N-1) forall(j=0..N-1)
            (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][j])
        )
     &
        // -- forbid diagonal attacks --------------------
        ( forall(i=0..N-1) forall(j=0..N-1)
            (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(j+k)%N])
        )
     &
        // -- forbid diagonal attacks --------------------
        (forall(i=0..N-1) forall(j=0..N-1)
            (q[i][j] -> forall(k=1..N-1) !q[(i+k)%N][(N+j-k)%N])
        )
    );
}