// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  This Quartz program considers magic squares of size sizexsize(). In such a
//  square, the numbers 1,...,9 should be placed such that the sums of
//  all rows and columns is the same.
//
//  It is well known that (up to permutations) there is only one
//  solution for the 3x3 square:
//
//      -------------
//      | 4 | 8 | 3 |
//      -------------
//      | 2 | 6 | 7 |
//      -------------
//      | 9 | 1 | 5 |
//      -------------
//
//  Clearly, the sum 15 is the only possibility, since the sum of all
//  numbers is 1+2+...+9 = 45 that will be partitioned into equally
//  sized parts for the three rows or the three columns.
//
// **************************************************************************

import MagicSquare.*;

package MagicSquare;

macro size = 3;

module MagicSquare(
    [size][size()]nat{size()*size()} a,
    event !wrong_sum, no_perm
) {
    for(i=0..(size-1)) CheckRowSum (a,i,wrong_sum);
    for(i=0..(size-1)) CheckColSum (a,i,wrong_sum);
    for(i=0..(size-1)) CheckRowPerm(a,i,no_perm);
    for(i=0..(size-1)) CheckColPerm(a,i,no_perm);
} satisfies {
    notmagic [DisProveA]: assert wrong_sum | no_perm;
}