    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.SBV.Examples.Puzzles.NQueens
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- Solves the NQueens puzzle: <http://en.wikipedia.org/wiki/Eight_queens_puzzle>
    -----------------------------------------------------------------------------

    module Data.SBV.Examples.Puzzles.NQueens where

    import Data.SBV

    -- | A solution is a sequence of row-numbers where queens should be placed
    type Solution = [SWord8]

    -- | Checks that a given solution of @n@-queens is valid, i.e., no queen
    -- captures any other.
    isValid :: Int -> Solution -> SBool
    isValid n s = bAll rangeFine s &&& allDifferent s &&& bAll checkDiag ijs
      where rangeFine x = x .>= 1 &&& x .<= fromIntegral n
            ijs = [(i, j) | i <- [1..n], j <- [i+1..n]]
            checkDiag (i, j) = diffR ./= diffC
               where qi = s !! (i-1)
                     qj = s !! (j-1)
                     diffR = ite (qi .>= qj) (qi-qj) (qj-qi)
                     diffC = fromIntegral (j-i)

    -- | Given @n@, it solves the @n-queens@ puzzle, printing all possible solutions.
    nQueens :: Int -> IO ()
    nQueens n
     | n < 0 = putStrLn $ "n must be non-negative, received: " ++ show n
     | True  = do putStrLn $ "Finding all " ++ show n ++ "-queens solutions.."
                  res <- allSat $ isValid n `fmap` mkExistVars n
                  cnt <- displayModels disp res
                  putStrLn $ "Found: " ++ show cnt ++ " solution(s)."
       where disp i (_, s) = do putStr $ "Solution #" ++ show i ++ ": "
                                dispSolution s
             dispSolution :: [Word8] -> IO ()
             dispSolution model
               | lmod /= n = error $ "Impossible! Backend solver returned " ++ show lmod ++ " values, was expecting: " ++ show n
               | True      = do putStr $ show model
                                putStrLn $ " (Valid: " ++ show (isValid n (map literal model)) ++ ")"
               where lmod  = length model