content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# OPTIONS_GHC -Wall #-}
  module Main where
  
  import Control.Monad
  import Data.Array.IArray
  import Data.Char
  import System.Environment
  import System.Exit
  import System.IO
  import qualified ToySolver.SAT as SAT
  import ToySolver.Internal.Util (setEncodingChar8)
  
  main :: IO ()
  main = do
  #ifdef FORCE_CHAR8
    setEncodingChar8
  #endif
  
    args <- getArgs
    case args of
      [fname] -> do
        s <- readFile fname
        let b = readBoard $ filter (not . isSpace) $ removeComments s
        ans <- solve b
        case ans of
          Nothing -> hPutStrLn stderr "NO SOLUTION"
          Just b2 -> do
            hPutStrLn stderr "SOLUTION FOUND"
            printAnswer b2
      _ -> do
        hPutStrLn stderr "Usage: sudoku input.sdk"
        exitFailure
  
  removeComments :: String -> String
  removeComments = unlines . filter p . lines
    where
      p ('#':_) = False
      p _ = True
  
  readBoard :: String -> Array (Int,Int) (Maybe Int)
  readBoard s = array ((1,1),(9,9)) $
    [ (idx, if isDigit c then Just (read [c]) else Nothing)
    | (idx, c) <- zip [(i,j) | i <- [1..9], j <- [1..9]] s
    ]
  
  solve :: Array (Int,Int) (Maybe Int) -> IO (Maybe (Array (Int,Int) Int))
  solve board = do
    solver <- SAT.newSolver
    SAT.setLogger solver (hPutStrLn stderr)
  
    (vs :: Array (Int,Int,Int) SAT.Var) <-
      liftM (array ((1,1,1), (9,9,9))) $
        forM [(i,j,k) | i<-[1..9], j<-[1..9], k<-[1..9]] $ \idx -> do
          v <- SAT.newVar solver
          return (idx,v)
  
    forM_ (assocs board) $ \((i,j), m) -> do
      case m of
        Nothing -> return ()
        Just k -> SAT.addClause solver [vs ! (i,j,k)]
  
    -- Every cell contains exactly one digit.
    forM_ [1..9] $ \i -> do
      forM_ [1..9] $ \j -> do
        SAT.addExactly solver [vs ! (i,j,k) | k <- [1..9]] 1
  
    forM_ [1..9] $ \k -> do
      -- Every row contains exactly one occurence of the digit.
      forM_ [1..9] $ \i -> do
        SAT.addExactly solver [vs ! (i,j,k) | j <- [1..9]] 1
      -- Every column contains exactly one occurence of the digit.
      forM_ [1..9] $ \j -> do
        SAT.addExactly solver [vs ! (i,j,k) | i <- [1..9]] 1
      -- Every block contains exactly one occurence of the digit.
      forM_ [0..2] $ \bi ->
        forM_ [0..2] $ \bj ->
          SAT.addExactly solver [vs ! (bi*3 + i', bj*3 + j', k) | i' <- [1..3], j' <- [1..3]] 1
  
    ret <- SAT.solve solver
    if ret then do
      m <- SAT.getModel solver
      return $ Just $ array ((1,1),(9,9)) [((i,j),k) | ((i,j,k),v) <- assocs vs, m ! v]
    else
      return Nothing
  
  printAnswer :: Array (Int,Int) Int -> IO ()
  printAnswer b =
    forM_ [1..9] $ \i ->
      putStrLn $ concat [show (b ! (i,j)) | j <- [1..9]]
  