```-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Examples.Puzzles.NQueens
-- Copyright   :  (c) Levent Erkok
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-- 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 \$ mkFreeVars n >>= return . isValid 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
```