-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.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>
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.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 :: Int -> Solution -> SBool
isValid Int
n Solution
s = forall a. (a -> SBool) -> [a] -> SBool
sAll forall {a}. (OrdSymbolic a, Num a) => a -> SBool
rangeFine Solution
s SBool -> SBool -> SBool
.&& forall a. EqSymbolic a => [a] -> SBool
distinct Solution
s SBool -> SBool -> SBool
.&& forall a. (a -> SBool) -> [a] -> SBool
sAll (Int, Int) -> SBool
checkDiag [(Int, Int)]
ijs
  where rangeFine :: a -> SBool
rangeFine a
x = a
x forall a. OrdSymbolic a => a -> a -> SBool
.>= a
1 SBool -> SBool -> SBool
.&& a
x forall a. OrdSymbolic a => a -> a -> SBool
.<= forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
        ijs :: [(Int, Int)]
ijs = [(Int
i, Int
j) | Int
i <- [Int
1..Int
n], Int
j <- [Int
iforall a. Num a => a -> a -> a
+Int
1..Int
n]]
        checkDiag :: (Int, Int) -> SBool
checkDiag (Int
i, Int
j) = SWord8
diffR forall a. EqSymbolic a => a -> a -> SBool
./= SWord8
diffC
           where qi :: SWord8
qi = Solution
s forall a. [a] -> Int -> a
!! (Int
iforall a. Num a => a -> a -> a
-Int
1)
                 qj :: SWord8
qj = Solution
s forall a. [a] -> Int -> a
!! (Int
jforall a. Num a => a -> a -> a
-Int
1)
                 diffR :: SWord8
diffR = forall a. Mergeable a => SBool -> a -> a -> a
ite (SWord8
qi forall a. OrdSymbolic a => a -> a -> SBool
.>= SWord8
qj) (SWord8
qiforall a. Num a => a -> a -> a
-SWord8
qj) (SWord8
qjforall a. Num a => a -> a -> a
-SWord8
qi)
                 diffC :: SWord8
diffC = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
jforall a. Num a => a -> a -> a
-Int
i)

-- | Given @n@, it solves the @n-queens@ puzzle, printing all possible solutions.
nQueens :: Int -> IO ()
nQueens :: Int -> IO ()
nQueens Int
n
 | Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"n must be non-negative, received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
 | Bool
True  = do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Finding all " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
"-queens solutions.."
              AllSatResult
res <- forall a. Provable a => a -> IO AllSatResult
allSat forall a b. (a -> b) -> a -> b
$ Int -> Solution -> SBool
isValid Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. SymVal a => Int -> Symbolic [SBV a]
mkExistVars Int
n
              Int
cnt <- forall a.
SatModel a =>
([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels forall a. a -> a
id forall {a} {a}. Show a => a -> (a, [Word8]) -> IO ()
disp AllSatResult
res
              String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Found: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
cnt forall a. [a] -> [a] -> [a]
++ String
" solution(s)."
   where disp :: a -> (a, [Word8]) -> IO ()
disp a
i (a
_, [Word8]
s) = do String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ String
"Solution #" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
i forall a. [a] -> [a] -> [a]
++ String
": "
                            [Word8] -> IO ()
dispSolution [Word8]
s
         dispSolution :: [Word8] -> IO ()
         dispSolution :: [Word8] -> IO ()
dispSolution [Word8]
model
           | Int
lmod forall a. Eq a => a -> a -> Bool
/= Int
n = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible! Backend solver returned " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
lmod forall a. [a] -> [a] -> [a]
++ String
" values, was expecting: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
           | Bool
True      = do String -> IO ()
putStr forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show [Word8]
model
                            String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
" (Valid: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int -> Solution -> SBool
isValid Int
n (forall a b. (a -> b) -> [a] -> [b]
map forall a. SymVal a => a -> SBV a
literal [Word8]
model)) forall a. [a] -> [a] -> [a]
++ String
")"
           where lmod :: Int
lmod  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Word8]
model