import structure FD from "x-alice:/lib/gecode/FD"
import structure FS from "x-alice:/lib/gecode/FS"
import structure Modeling from "x-alice:/lib/gecode/Modeling"
import structure Explorer from "x-alice:/lib/tools/Explorer"

open Modeling

val inputlist2 = [(1,[8,31,43,55]),(2,[2,51,63,67]),
                  (3,[10,39,49,59,74]),(4,[19,47,69,79]),
                  (5,[23,29,42,53,64]),(6,[3,18,80]),
                  (7,[13,27,33]),(8,[7,15,75]),
                  (9,[35,40,72])]
                
val inputlist_hard2 = [(1,[17,56,76]),(2,[34,60]),
                       (3,[6,48]),(4,[43,65]),
                       (5,[22,74]),(6,[8,50]),
                       (7,[21,41]),(8,[26,39,61]),
                       (9,[20,32,62])]
                 
fun sudoku2 inputlist space = 
  let
     val numbers = Vector.tabulate(9,fn x => 
                        FS.upperBound(space,#[(1,81)]))
     val rows = List.tabulate(9,fn x =>(x*9+9-8,x*9+9)) 
     val columns = List.tabulate(9,fn y => 
                       Vector.tabulate(9,fn x =>(x*9+1+y,x*9+1+y)))
     val boxes1 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+1+y*3,x*9+3+y*3)))
     val boxes2 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+28+y*3,x*9+30+y*3)))
     val boxes3 = List.tabulate(3,fn y => 
                   Vector.tabulate(3,fn x =>(x*9+55+y*3,x*9+57+y*3)))
     val boxes = List.concat([boxes1,boxes2,boxes3])
     fun constr l = 
       List.app(fn y => 
                 let
                    val tmp1 = FS.Value.make(space,y)
                 in
                    Vector.app(fn x => 
                     let 
                        val tmp2 = FS.setvar space 
                     in
                        FS.relOp(space,x,FS.INTER,tmp1,FS.SEQ,tmp2);
                        FS.cardRange(space,1,1,tmp2)
                     end)numbers
                 end)l
     fun fsDisjoint ([]) = ()
       | fsDisjoint (x::xs) = 
            (List.app(fn y => FS.rel(space,y, FS.DISJ,x))xs;
             fsDisjoint(xs))
  in
    (* use next constraint only, if inputlist is used *)
     List.app(fn(x,y) => 
       List.app(fn z => 
                  let 
                     val tmp = FS.Value.make(space,#[(z,z)])
                  in
                     FS.rel(space,Vector.sub(numbers,x-1),FS.SUP,tmp)
                  end)y)inputlist;
     Vector.app(fn x => FS.cardRange(space,9,9,x))numbers;
     (* the domains of all numbers are pairwise distinct *)
     fsDisjoint(Vector.toList numbers);
    (* distinct numbers in rows *)
     List.app(fn(y,z)=>
       let 
          val tmp1 = FS.Value.make(space,#[(y,z)]) 
       in
          Vector.app(fn x => 
                      let 
                         val tmp2 = FS.setvar space 
                      in
                         FS.relOp(space,x,FS.INTER,tmp1,FS.SEQ,tmp2);
                         FS.cardRange(space,1,1,tmp2)
                      end)numbers
       end)rows;
    (* distinct numbers in columns *)
     constr columns;  
    (* distinct numbers in 3 x 3 boxes *)
     constr boxes;   
     FS.setvarbranch(space,numbers,FS.FSB_MIN_CARD,FS.FSB_MIN); 
     numbers
  end

(* Explorer.exploreOne(sudoku2) *)
(* Explorer.exploreAll(sudoku2 inputlist2) *)
(* Explorer.exploreAll(sudoku2 inputlist_hard2) *)