"""sudosolver.py: Sudoku puzzle solver

  For documentation, see:
    http://www.nmt.edu/tcc/help/lang/python/examples/sudoku/
"""
#================================================================
# Manifest constants
#----------------------------------------------------------------
SUBMAT_L  =  3
MAT_L  =  SUBMAT_L ** 2
BOARD_L  =  MAT_L ** 2
EMPTY  =  0
# - - - - -   c l a s s   S u d o k u S o l v e r   - - - - -

class SudokuSolver:
    """Represents one sudoku puzzle.
      Exports:
        SudokuSolver ( givenPuzzle, solutionObserver=None,
                       changeObserver=None ):
          [ (givenPuzzle is a sudoku puzzle as a string) and
            (solutionObserver is a procedure or None) and
            (changeObserver is a procedure or None) ->
              if givenPuzzle is a valid sudoku puzzle ->
                return a SudokuSolver object representing that
                puzzle in its initial state
              else ->
                raise ValueError ]
        .givenPuzzle:       [ as passed to constructor, read-only ]
        .solutionObserver:  [ as passed to constructor, read-only ]
        .changeObserver:    [ as passed to constructor, read-only ]
        .solve()
          [ call self.changeObserver (if any) for every change
            to a cell value and call self.solutionObserver for
            every solution of self ]
        .get(r, c):
          [ r and c are integers ->
              if (0<=r<MAT_L) and (0<=c<MAT_L) ->
                return the state of the cell at row r and column c
                as 0 for empty, or an integer in [1,9] if set
              else -> raise KeyError ]
        .write(outFile):
          [ outFile is a writeable file ->
              outFile  +:=  a representation of self's state in
                  input-file format ]
      State/Invariants:
        .nStateChanges:     [ number of cell state changes so far ]
        .nSolutions:        [ number of solutions seen so far ]
        .__given:
          [ the initial state of the puzzle as a list of integers,
            0 for empty, or in [1,9] if set ]
        .__board:
          [ the current state of the puzzle as a list of integers,
            0 for empty, or in [1,9] if set ]
    """
# - - -   S u d o k u S o l v e r . _ _ i n i t _ _   - - -

    def __init__ ( self, givenPuzzle, solutionObserver=None,
                   changeObserver=None ):
        """Constructor for SudokuSolver."""
        #-- 1 --
        self.givenPuzzle       =  givenPuzzle
        self.solutionObserver  =  solutionObserver
        self.changeObserver    =  changeObserver
        self.nStateChanges     =  0
        self.nSolutions        =  0
        #-- 2 --
        # [ self.givenPuzzle is a string ->
        #     if self.givenPuzzle is a valid sudoku puzzle as a string ->
        #       self.__board  :=  a list of BOARD_L integers
        #                         representing that puzzle
        #     else -> raise ValueError ]
        self.__board  =  self.__readPuzzle()
        #-- 3 --
        # [ self.__given  :=  a copy of self.__board ]
        self.__given  =  self.__board[:]
# - - -   S u d o k u S o l v e r . _ _ r e a d P u z z l e   - - -

    def __readPuzzle ( self ):
        """Translate the puzzle from external to internal form.

          [ self.givenPuzzle is a string ->
              if self.givenPuzzle is a valid sudoku puzzle ->
                return a list of BOARD_L integers representing
                that puzzle
              else -> raise ValueError ]
        """
        #-- 1 --
        # [ charList  :=  a list whose elements are the
        #       non-whitespace characters of self.givenPuzzle in
        #       the same order ]
        charList  =  [ c
                       for c in list(self.givenPuzzle)
                       if not c.isspace() ]
        #-- 2 --
        if  len(charList) != BOARD_L:
            print("Puzzle has %d nonblank characters; it should have exactly" \
                   " %d." % (len(charList), BOARD_L))
            raise ValueError
        #-- 3 --
        # [ if each element of charList is either "." or in
        #   the interval ["1", "9"] ->
        #     result  :=  a list of integers corresponding to the
        #         elements of charList consisting of integer 0
        #         where the value is "." and an integer in [1,9]
        #         where the value is a digit
        #   else ->
        #     raise ValueError ]
        result  =  [ self.__readChar ( c )
                     for c in charList ]

        #-- 4 --
        return result
# - - -   S u d o k u S o l v e r . _ _ r e a d C h a r   - - -

    def __readChar ( self, c ):
        """Translate one input character.

          [ c is a one-character string ->
              if c is "." ->
                return 0
              else if c is a digit in ["1", "9"] ->
                return int(c)
              else -> raise ValueError ]
        """
        if  c == ".":
            return 0
        elif "1" <= c <= "9":
            return int(c)
        else:
            print("Invalid sudoku character: '%s'" % c)
            raise ValueError
# - - -   S u d o k u S o l v e r . g e t   - - -

    def get ( self, r, c ):
        """Get the cell at row r, column c.
        """
        #-- 1 --
        # [ if r is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]
        
        if  not ( 0 <= r < MAT_L ):
            print( "SudokuSolver.get(): Bad row index, %d." % r )
            raise KeyError

        #-- 2 --
        # [ if c is in [0,MAT_L) ->
        #     I
        #   else -> raise KeyError ]
        if  not ( 0 <= c < MAT_L ):
            print( "SudokuSolver.get(): Bad column index, %d." % c )
            raise KeyError
        #-- 3 --
        # [ x  :=  index in self.__board corresponding to row r,
        #          column c ]
        x  =  self.__rowColToX ( r, c )
        #-- 4 --
        return  self.__board[x]
# - - -   S u d o k u S o l v e r . _ _ r o w C o l T o X   - - -

    def __rowColToX ( self, r, c ):
        """Convert row/column indices to board index.

          [ r and c are integers in [0,8] ->
              return the index in self.__board corresponding to
              that row and column ]
        """
        return  ( r * MAT_L ) + c
# - - -   S u d o k u S o l v e r . w r i t e   - - -

    def write ( self, outFile ):
        """Write the puzzle state as plain text.

          Output format (minus the enclosing box):
            +---------------------+
            |7 2 .   . . 5   1 . .|
            |. 1 5   9 8 .   4 . .|
            |. 8 .   . . 1   . . 6|
            |                     |
            |. 4 .   . 3 .   6 . 5|
            |3 . .   6 . 2   . . 7|
            |9 . 1   . 7 .   . 2 .|
            |                     |
            |5 . .   7 . .   . 9 .|
            |. . 2   . 9 6   3 5 .|
            |. . 4   2 . .   . 6 8|
            +---------------------+
        """
        #-- 1 --
        for rowx in range(MAT_L):
            #-- 1 body --
            # [ rowx is in [0,MAT_L) ->
            #     outFile  +:=  a representation of row rowx of self ]

            #-- 1.1 --
            # [ if ( ( rowx > 0 ) and
            #        ( rowx % SUBMAT_L ) == 0 ) ) ->
            #     outFile  +:=  an empty line
            #   else -> I ]
            if  ( ( rowx > 0 ) and
                  ( ( rowx % SUBMAT_L ) == 0 ) ):
                print >> outFile

            #-- 1.2 --
            # [ outFile  +:=  a representation of row rowx of self ]
            self.writeRow ( outFile, rowx )
# - - -   S u d o k u S o l v e r . w r i t e R o w   - - -

    def writeRow ( self, outFile, rowx ):
        """Display one row in plain text.

          [ (outFile is a writeable file) and
            (rowx is in [0,MAT_L) ->
              outFile  +:=  a representation of row rowx of self ]
        """

        #-- 1 --
        for  colx in range(MAT_L):
            #-- 1 body --
            # [ sys.stdout  +:=  a representation of the cell at
            #       row rowx and column colx ]

            #-- 1.1 --
            # [ c  :=  self's cell at (rowx,colx) in character
            #          form ]
            cell  =  self.get ( rowx, colx )
            if  cell == 0:  c = '.'
            else:           c = chr ( ord ( '0' ) + cell )

            #-- 1.2 --
            # [ sys.stdout  +:=  c ]
            if  ( ( colx > 0 ) and
                  ( ( colx % SUBMAT_L ) == 0 ) ):
                print >>outFile, " ",
            print >>outFile, c,
        #-- 2 --
        print >>outFile
# - - -   S u d o k u S o l v e r . s o l v e   - - -

    def solve ( self ):
        """Find all solutions to the puzzle.
        """
        #-- 1 --
        # [ call self.solutionObserver for all solutions of
        #   self.__board and call self.changeObserver (if any)
        #   for all state changes in finding those solutions ]
        self.__reSolve ( 0 )
# - - -   S u d o k u S o l v e r . _ _ r e S o l v e   - - -

    def __reSolve ( self, x ):
        """Recursively solve the puzzle.

          [ (self.__board has no blank cells before position x) and
            (x is an integer) ->
              if x >= BOARD_L ->
                call self.solutionObserver for the current state
                of self.__board
              else if x is in [0,BOARD_L) ->
                call self.solutionObserver for all solutions of
                self.__board starting at position x, and call
                self.changeObserver (if any) for all state changes
                in finding those solutions ]
        """
        #-- 1 --
        # [ if x >= BOARD_L ->
        #     call self.solutionObserver
        #     return
        #   else -> I ]
        if  x >= BOARD_L:
            self.__solution()
            return
        #-- 2 --
        # [ if self.__given[x] != EMPTY ->
        #     call self.solutionObserver for all solutions of
        #     self.__board starting at position x+1, and call
        #     self.changeObserver (if any) for all state changes
        #     in finding those solutions
        #     return
        #   else -> I ]
        if  self.__given[x] != EMPTY:
          self.__reSolve ( x + 1 )
          return
        #-- 3 --
        # [ possibles  :=  list of all digits that are not
        #       duplicate in the same row, column, or submatrix
        #       as cell x ]
        possibles  =  self.__findPossibles ( x )
        #-- 4 --
        # [ call self.solutionObserver for all solutions of
        #   self.__board starting at position x+1 with cell x
        #   set to each member of possibles, and call
        #   self.changeObserver (if any) for all state changes
        #   in finding those solutions ]
        for  trial in possibles:
            #-- 4 body --
            # [ call self.solutionObserver for all solutions of
            #   self.__board starting at position x+1 with cell
            #   x set to trial, and call self.changeObserver
            #   (if any) for all state changes in finding those
            #   solutions ]
            self.__set ( x, trial )
            self.__reSolve ( x + 1 )

        #-- 5 --
        self.__set ( x, EMPTY )
# - - -   S u d o k u S o l v e r . _ _ s o l u t i o n   - - -

    def __solution ( self ):
        """A solution has been found.

          [ if self.solutionObserver is not None ->
              call self.solutionObserver(self)
            in any case ->
              self.nSolutions  +:=  1 ]
        """

        #-- 1 --
        self.nSolutions  +=  1

        #-- 2 --
        if  self.solutionObserver is not None:
            self.solutionObserver(self)
# - - -   S u d o k u S o l v e r . _ _ f i n d P o s s i b l e s

    def __findPossibles ( self, x ):
        """What digits are legal at position x on the board?

          [ x is an integer in [0,BOARD_L) ->
              return a list of digits not found in the row,
              column, or submatrix containing position x ]
        """
        #-- 2 --
        # [ rowElim  :=  a bitmap of the digits that occur
        #       elsewhere in the same row as position x ]
        rowElim  =  self.__usedInRow ( x )

        #-- 3 --
        # [ colElim  :=  a bitmap of the digits that occur
        #       elsewhere in the same column as position x ]
        colElim  =  self.__usedInColumn ( x )

        #-- 4 --
        # [ subElim  :=  a bitmap of the digits that occur
        #       elsewhere in the same submatrix as position x ]
        subElim  =  self.__usedInSubmat ( x )
        #-- 5 --
        # [ elim  :=  (rowElim | colElim | subElim) ]
        elim  =  [ rowElim[x] | colElim[x] | subElim[x]
                   for x in range(MAT_L) ]
        #-- 6 --
        # [ return a list containing digits in [1,9]
        #   corresponding to zero elements of elim ]
        result  =  [ i+1
                     for i in range(0,MAT_L)
                     if elim[i]==0 ]

        #-- 7 --
        return result
# - - -   S u d o k u S o l v e r . _ _ u s e d I n R o w   - - -

    def __usedInRow ( self, x ):
        """What digits are used elsewhere in the row containing x?

          [ x is an integer in [0,BOARD_L) ->
              return a 9-element bitmap whose elements are true
              iff the corresponding digit is used elsewhere in
              the row containing board position x ]
        """

        #-- 1 --
        # [ rx      :=  the row index of board position x
        #   cx      :=  the column index of board position x
        #   result  :=  a list of MAT_L zeroes ]
        rx, cx  =  self.__xToRowCol ( x )
        result  =  [0] * MAT_L
        #-- 2 --
        # [ result  :=  result with elements corresponding to
        #       digits found in row rx (except for column cx) ]
        for  col in range(MAT_L):
            #-- 2 body --
            # [ if (col != cx) and
            #   (self has a nonzero value D in cell (rx, col) ->
            #     result[D-1]  :=  1
            #   else ->
            #     I ]
            if  col != cx:
                cell  =  self.get(rx, col)
                if  cell != EMPTY:
                    result[cell-1]  =  1

        #-- 3 --
        return result
# - - -   S u d o k u S o l v e r . _ _ u s e d I n C o l u m n

    def __usedInColumn ( self, x ):
        """What digits are used elsewhere in the column containing x?

          [ x is an integer in [0,BOARD_L) ->
              return a 9-element bitmap whose elements are true
              iff the corresponding digit is used elsewhere in
              the column containing board position x ]
        """

        #-- 1 --
        # [ rx      :=  the row index of board position x
        #   cx      :=  the column index of board position x
        #   result  :=  a list of MAT_L zeroes ]
        rx, cx  =  self.__xToRowCol ( x )
        result  =  [0] * MAT_L
        #-- 2 --
        # [ result  :=  result with elements corresponding to
        #       digits found in column cx (except for row rx) ]
        for  row in range(MAT_L):
            #-- 2 body --
            # [ if (row != rx) and
            #   (self has a nonzero value D in cell (rx, col) ->
            #     result[D-1]  :=  1
            #   else ->
            #     I ]
            if  row != rx:
                cell  =  self.get(row, cx)
                if  cell != EMPTY:
                    result[cell-1]  =  1

        #-- 3 --
        return result
# - - -   S u d o k u S o l v e r . _ _ u s e d I n S u b m a t r i x

    def __usedInSubmat ( self, x ):
        """What digits are used in the submatrix containing x?

          [ x is an integer in [0, BOARD_L) ->
              return a 9-element bitmap whose elements are true
              iff the corresponding digit is used elsewhere in
              the submatrix containing board position x ]
        """
        
        #-- 1 --
        # [ result  :=  a list of MAT_L zeroes
        #   rx      :=  index of the row containing board
        #               position x
        #   cx      :=  index of the column containing board
        #               position x
        result  =  [0] * MAT_L
        rx, cx  =  self.__xToRowCol ( x )

        #-- 2 --
        # [ rSub  :=  index of the row containing the upper left
        #             cell of the submatrix containing row rx
        #   cSub  :=  index of the column containing the upper left
        #             cell of the submatrix containing column cx ]
        rSub  =  int((rx // 3) * 3)
        cSub  =  int((cx // 3) * 3)
        #-- 3 --
        # [ result  :=  result with its elements set to 1 at
        #       each position corresponding to a digit that
        #       occurs in the submatrix whose upper left corner
        #       is at row rSub, column cSub, ignoring the cell at
        #       row rx, column cx ]
        for rowx in range(rSub, rSub+SUBMAT_L):
            for  colx in range(cSub, cSub+SUBMAT_L):
                #-- 3 body --
                # [ if (rowx != rx) or (colx != cx) and
                #   self's cell value V at row rowx, column colx is
                #   not EMPTY ->
                #     result[V-1]  :=  1
                #   else -> I ]
                if  ( ( rowx != rx ) or ( colx != cx ) ):
                    cell  =  self.get(rowx, colx)
                    if  cell != EMPTY:
                        result [ cell-1 ]  =  1

        #-- 4 --
        return result
# - - -   S u d o k u S o l v e r . _ _ s e t   - - -

    def __set ( self, x, value ):
        """Set or clear one cell of the board.

          [ (x is an integer in [0,BOARD_L)) and
            (value is an integer in [0,MAT_L]) ->
              if  self.changeObserver is not None ->
                notify self.changeObserver that cell x is being
                set to value
              in any case ->
                self.__board[x]  :=  value ]
        """
        #-- 1 --
        self.__board[x]     =   value
        self.nStateChanges  +=  1
        #-- 2 --
        # [ if self.changeObserver is not None ->
        #     notify self.changeObserver that cell x is being
        #     set to value
        if  self.changeObserver is not None:
            row, col  =  self.__xToRowCol ( x )
            self.changeObserver ( self, row, col, value )
# - - -   S u d o k u S o l v e r . _ _ x T o R o w C o l   - - -

    def __xToRowCol ( self, x ):
        """Translate board index to row and column indices.

          [ x is an integer in [0,BOARD_L) ->
             return (r,c) where r is x's row and c is x's column ]
        """
        return divmod ( x, 9 )