// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following Quartz module illustrates causality by solving Sudokus. Given//
// a Sudoku x (where the empty fields are filled by zeros), the module below  //
// copies the known values into the array y. After that, the Sudoku rules are //
// listed to make further assignments to the single fields y[i][j]. Note that //
// the entire computation is done within a single macro step, where y[i][j]   //
// may already have its final value or the unknown value ⊥. This way, known   //
// values, i.e., the "must" information propagate themselves. The "can/may"   //
// information, i.e., which values are forbidden in particular fields y[i][j] //
// is maintained in the local array p: p[i][j][v] holds if value v is possible//
// in field y[i][j].                                                          //
// ************************************************************************** //


module Sudoku([9][9]nat{10} ?x,[9][9]nat{9} y) {
    [9][9][9]bool p;
    
    // retrieve initial values
    for(i=0..8)
        for(j=0..8)
            if(x[i][j]>0)
                let(v = x[i][j]-1) {
                    y[i][j] = v;
                    p[i][j][v] = true;
                }

    // no value must appear twice in a group
    for(i=0..8)
        for(j=0..8) {
            // row constraint
            for(k=0..8)
                if(k!=j)
                    p[i][k][y[i][j]] = false;
            // column constraint
            for(k=0..8)
                if(k!=i)
                    p[k][j][y[i][j]] = false;
            // square constraint
            let(i0=3*(i/3))
            let(j0=3*(j/3))
            for(i1=0..2)
                for(j1=0..2)
                    if((i0+i1!=i) | (j0+j1!=j))
                        p[i0+i1][j0+j1][y[i][j]] = false;
        }

    // assign value if this is the only possible place in a group
    for(i=0..8)
        for(j=0..8) 
            for(v=0..8) {
                // unique possibility
                if(!exists(k=0..8) (k!=v & p[i][j][k])) {
                    y[i][j] = v;
                    p[i][j][v] = true;
                }
                // row constraint
                if(!exists(k=0..8) (k!=j & p[i][k][v])) {
                    y[i][j] = v;
                    p[i][j][v] = true;
                }
                // column constraint
                if(!exists(k=0..8) (k!=i & p[k][j][v])) {
                    y[i][j] = v;
                    p[i][j][v] = true;
                }
                // square constraint
                let(i0=3*(i/3))
                let(j0=3*(j/3))
                if(!exists(i1=0..2) exists(j1=0..2) ((i0+i1!=i | j0+j1!=j) & p[i0+i1][j0+j1][v])) {
                    y[i][j] = v;
                    p[i][j][v] = true;
                }
            }
}
drivenby {
    [9][9]nat{10} solution;
    x = [[0,0,3,0,0,6,0,0,5],
         [0,2,1,0,8,0,4,3,0],
         [0,4,0,0,0,1,0,0,7],
         [0,0,0,3,6,9,0,0,1],
         [9,0,7,1,0,8,6,0,4],
         [8,0,0,2,7,4,0,0,0],
         [3,0,0,8,0,0,0,5,0],
         [0,8,5,0,9,0,7,4,0],
         [2,0,0,7,0,0,3,0,0] ];
    solution = 
        [[7,9,3,4,2,6,1,8,5],
         [6,2,1,5,8,7,4,3,9],
         [5,4,8,9,3,1,2,6,7],
         [4,5,2,3,6,9,8,7,1],
         [9,3,7,1,5,8,6,2,4],
         [8,1,6,2,7,4,5,9,3],
         [3,7,4,8,1,2,9,5,6],
         [1,8,5,6,9,3,7,4,2],
         [2,6,9,7,4,5,3,1,8] ];
    for(i=0..8)
        for(j=0..8)
            assert(y[i][j] == solution[i][j]-1);
}