diff --git a/abc-puzzle.cabal b/abc-puzzle.cabal --- a/abc-puzzle.cabal +++ b/abc-puzzle.cabal @@ -1,5 +1,5 @@ name: abc-puzzle -version: 0.2 +version: 0.2.1 synopsis: Generate instances of the ABC Logic Puzzle. description: This program generate instances of the ABC Logic Puzzle (). @@ -22,8 +22,8 @@ hs-source-dirs: src ghc-options: -W -- other-modules: - other-extensions: ImplicitParams, ConstraintKinds - build-depends: base >=4.7 && <5, vector >=0.10, minisat >=0.1, Safe >=0.1, random >=1.0, + other-extensions: ImplicitParams + build-depends: base >=3 && <5, array, minisat >=0.1, Safe >=0.1, random >=1.0, random-shuffle >= 0.0.4 default-language: Haskell2010 diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE ImplicitParams, ConstraintKinds #-} +{-# LANGUAGE ImplicitParams #-} -- ABC logic puzzle @@ -6,8 +6,7 @@ import Control.Monad import Data.List -import qualified Data.Vector as Vector -import Data.Vector (Vector, (!),(//)) +import Data.Array.IArray import MiniSat import Safe import System.Environment @@ -15,50 +14,57 @@ import System.Random.Shuffle import System.Random -type Puzzle = Vector (Vector Field) -- rows of columns -type Field = Vector Lit +type Puzzle = Array Int (Array Int Field) -- rows of columns +type Field = Array Int Lit data Hints = Hints { - top, right, bottom, left :: Vector Field} + top, right, bottom, left :: Array Int Field} data Full = Full { puzzle :: Puzzle, hints :: Hints} -type Env = (?size :: Int, ?letters :: Int, ?solver :: Solver) - -genLit :: Env => IO Lit +genLit :: (?solver :: Solver) => IO Lit genLit = newLit ?solver +replicateAM :: Monad m => Int -> m a -> m (Array Int a) +replicateAM l m = liftM (listArray (0,l-1)) (replicateM l m) -genField :: Env => IO Field -genField = Vector.replicateM (?letters+1) genLit +replicateA :: Int -> a -> Array Int a +replicateA l m = listArray (0,l-1) (replicate l m) -genPuzzle :: Env => IO Puzzle -genPuzzle = Vector.replicateM ?size $ Vector.replicateM ?size genField -genHints :: Env => IO Hints +genField :: (?letters :: Int, ?solver :: Solver) => IO Field +genField = replicateAM (?letters+1) genLit + +genPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Puzzle +genPuzzle = replicateAM ?size $ replicateAM ?size genField + +genHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Hints genHints = liftM4 Hints side side side side - where side = Vector.replicateM ?size genField + where side = replicateAM ?size genField -genFull :: Env => IO Full +genFull :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => IO Full genFull = liftM2 Full genPuzzle genHints -addClause' :: Env => [Lit] -> IO () +addClause' :: (?solver :: Solver) => [Lit] -> IO () addClause' c = addClause ?solver c >> return () -addClauses :: Env => [[Lit]] -> IO () +addClauses :: (?solver :: Solver) => [[Lit]] -> IO () addClauses = mapM_ addClause' -lx :: Env => [Int] +lx :: (?letters :: Int) => [Int] lx = [1 .. ?letters] -fx :: Env => [Int] +fx :: (?letters :: Int) => [Int] fx = [0 .. ?letters] -sx :: Env => [Int] +sx :: (?size :: Int) => [Int] sx = [0 .. ?size - 1] +sx_reverse :: (?size :: Int) => [Int] +sx_reverse = [?size - 1, (?size - 2).. 0] -conHint :: Env => Field -- ^ hint field + +conHint :: (?letters :: Int, ?solver :: Solver) => Field -- ^ hint field -> [Field] -- ^ neighbouring fields, the closest field is last -- in the list -> IO () @@ -67,83 +73,56 @@ where blanks = map (\f -> neg (f!0)) -conBottomHints :: Env => Vector Field -> Puzzle -> IO () +conBottomHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conBottomHints h p = sequence_ [conHint (h!i) [(p!j)!i|j<-[(?letters-1) .. (?size-1)]]| i <- sx] - >> mapM_ conField (Vector.toList h) + >> mapM_ conField (elems h) -conRightHints :: Env => Vector Field -> Puzzle -> IO () +conRightHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conRightHints h p = sequence_ [conHint (h!i) [(p!i)!j|j<-[(?letters-1) .. (?size-1)]]| i <- sx] - >> mapM_ conField (Vector.toList h) + >> mapM_ conField (elems h) -conTopHints :: Env => Vector Field -> Puzzle -> IO () +conTopHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conTopHints h p = sequence_ [conHint (h!i) [(p!j)!i|j<-[(?size - ?letters),(?size - ?letters - 1) .. 0]]| i <- sx] - >> mapM_ conField (Vector.toList h) + >> mapM_ conField (elems h) -conLeftHints :: Env => Vector Field -> Puzzle -> IO () +conLeftHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> Puzzle -> IO () conLeftHints h p = sequence_ [conHint (h!i) [(p!i)!j|j<-[(?size - ?letters),(?size - ?letters - 1) .. 0]]| i <- sx] - >> mapM_ conField (Vector.toList h) + >> mapM_ conField (elems h) -conHints :: Env => Full -> IO () +conHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Full -> IO () conHints (Full p h) = conBottomHints (bottom h) p >> conRightHints (right h) p >> conTopHints (top h) p >> conLeftHints (left h) p -conFull :: Env => Full -> IO () +conFull :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Full -> IO () conFull full = conPuzzle (puzzle full) >> conHints full -conField :: Env => Field -> IO () -conField l = do addClause' $ Vector.toList l +conField :: (?letters :: Int, ?solver :: Solver) => Field -> IO () +conField l = do addClause' $ elems l addClauses [ [neg (l!i), neg (l!j)] | i <- fx, j <- [0 .. i-1]] -conFields :: Env => Puzzle -> IO () +conFields :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conFields p = sequence_ [conField ((p!i)!j) | i <- sx, j <- sx] --- generate contstraits that avoid ambiguous configurations -conAmbFields :: Env => Puzzle -> IO () -conAmbFields p = when (?size >= 2) $ do - vis <- Vector.generateM ?size (\i -> Vector.generateM ?size (generate i)) - let getVis i j = if i < low || j < low || i >= hi || j >= hi then - [((vis!i)!j)] else [] - addClauses [ map neg [(((p!i)!j)!l), (((p!di)!dj)!l), (((p!i)!dj)!f), (((p!di)!j)!f)] - ++ getVis i j ++ getVis di dj ++ getVis i dj ++getVis di j - | i <- range, j <- range, di<-[0..i-1]++[i+1..(?size-1)] - , dj<-[j+1..(?size-1)], l <- lx, f<- fx, l/=f] - - where range = [0..(?size-2)] - low = ?size - ?letters + 1 - hi = ?letters - 1 - generate i j = if i < low || j < low || i >= hi || j >= hi - then do - lit <- genLit - con lit i j - return lit - else return (error "position is not on the fringe") - con lit i j = do - when (i < low) $ addClause' (lit : [neg (((p!i')!j)!0) |i'<-[0..i-1]]) - when (j < low) $ addClause' (lit : [neg (((p!i)!j')!0) |j'<-[0..j-1]]) - when (i >= hi) $ addClause' (lit : [neg (((p!i')!j)!0) |i'<-[i+1..(?size-1)]]) - when (j >= hi) $ addClause' (lit : [neg (((p!i)!j')!0) |j'<-[j+1..(?size-1)]]) - - -- fields must be different letters (however, both can be blank) -conDiffFields :: Env => Field -> Field -> IO () +conDiffFields :: (?letters :: Int, ?solver :: Solver) => Field -> Field -> IO () conDiffFields l1 l2 = do addClauses [[neg (l1!i), neg (l2!i)] | i <- lx] -conRows :: Env => Puzzle -> IO () +conRows :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conRows p = do -- fields must be different letters - sequence_ [conDiffFields (r!i) (r!j) | r <- Vector.toList p, i <- sx, j <- [0..i-1]] + sequence_ [conDiffFields (r!i) (r!j) | r <- elems p, i <- sx, j <- [0..i-1]] -- each letter must appear - addClauses [[(r!i)!l | i <- sx] | r <- Vector.toList p, l <- lx] + addClauses [[(r!i)!l | i <- sx] | r <- elems p, l <- lx] -conColumns :: Env => Puzzle -> IO () +conColumns :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conColumns p = do -- letters must be different letters sequence_ [conDiffFields ((p!i)!c) ((p!j)!c) | c <- sx, i <- sx, j <- [0..i-1]] -- each letter must appear addClauses [[((p!i!)c)!l | i <- sx] | c <- sx, l <- lx] -conPuzzle :: Env => Puzzle -> IO () +conPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO () conPuzzle p = conRows p >> conColumns p >> conFields p data Entry = Blank @@ -153,28 +132,28 @@ show Blank = " " show (Letter l) = [iterate succ 'A' !! l] -newtype Solution = Solution {unSolution :: Vector (Vector (Entry))} +newtype Solution = Solution {unSolution :: Array Int (Array Int (Entry))} instance Show Solution where - show = unlines . map (unwords . map show . Vector.toList) . Vector.toList . unSolution + show = unlines . map (unwords . map show . elems) . elems . unSolution -getSolution :: Env => Puzzle -> IO Solution -getSolution p = liftM Solution $ liftM Vector.fromList $ - sequence [ liftM Vector.fromList $ - sequence [ getEntry f | f <- Vector.toList r] | r <- Vector.toList p ] +getSolution :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Puzzle -> IO Solution +getSolution p = liftM Solution $ liftM (listArray (0,?size-1)) $ + sequence [ liftM (listArray (0,?size-1)) $ + sequence [ getEntry f | f <- elems r] | r <- elems p ] -getHints :: Env => Vector Field -> IO [Entry] -getHints h = sequence [ getEntry f | f <- Vector.toList h] +getHints :: (?size :: Int, ?letters :: Int, ?solver :: Solver) => Array Int Field -> IO [Entry] +getHints h = sequence [ getEntry f | f <- elems h] getAllHints :: Int -> [((Int,Int),Int)] -> AllHints getAllHints size hints = (AllHints t r b l (length hints)) - where [t,r,b,l] = [ emp // [ (i,Letter (letter-1)) | ((s',i),letter) <- hints, s' == s] | s <- [0..3]] - emp = Vector.replicate size Blank + where [t,r,b,l] = [ emp // [ (i,Letter (letter-1)) | ((s',i),letter) <- hints, s' == s] | s <- [0..3]] + emp = replicateA size Blank -data AllHints = AllHints {atop, aright, abottom, aleft :: Vector Entry, hintSize :: Int} deriving Show +data AllHints = AllHints {atop, aright, abottom, aleft :: Array Int Entry, hintSize :: Int} deriving Show -getEntry :: Env => Field -> IO Entry +getEntry :: (?letters :: Int, ?solver :: Solver) => Field -> IO Entry getEntry l = do Just b <- modelValue ?solver (l!0) if b then return Blank else getLetter where getLetter :: IO Entry @@ -183,7 +162,7 @@ return $ Letter n -- Adds clause to avoid the currently found solution. -removeCurrentSolution :: Env => IO Bool +removeCurrentSolution :: (?solver :: Solver) => IO Bool removeCurrentSolution = do n <- minisat_num_vars ?solver addClause ?solver =<< @@ -196,24 +175,22 @@ entryToInt Blank = 0 entryToInt (Letter i) = i + 1 -removeSolution :: Env' => Solution -> IO () +removeSolution :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full) => Solution -> IO () removeSolution (Solution sol) = addClause' [neg (entryValue ((i,j),entryToInt $ (sol!i)!j))| i<-sx,j<-sx] prettyHints :: AllHints -> String prettyHints (AllHints t r b l s) = - " | " ++ (intercalate " | " $ map show $ Vector.toList t) ++ " | \n" + " | " ++ (intercalate " | " $ map show $ elems t) ++ " | \n" ++ rule ++ intercalate rule rows ++ rule - ++ " | " ++ (intercalate " | " $ map show $ Vector.toList b) ++ " | \n\n" + ++ " | " ++ (intercalate " | " $ map show $ elems b) ++ " | \n\n" ++ "number of hints: " ++ show s ++ "\n" - where rule = "-" ++ concat (replicate size "+---") ++ "+-\n" - divider = concat (replicate size "| ") ++ "|" - rows = zipWith (\l r -> show l ++ divider ++ show r ++ "\n") (Vector.toList l) (Vector.toList r) - size = Vector.length t - -type Env' = (Env, ?full :: Full) + where rule = "--" ++ concat (replicate size "+---") ++ "+--\n" + divider = concat (replicate size " | ") ++ " | " + rows = zipWith (\l r -> show l ++ divider ++ show r ++ "\n") (elems l) (elems r) + size = length $ indices t -- complete list of entry positions @@ -226,19 +203,20 @@ ?letters = letters f <- genFull conFull f - conAmbFields (puzzle f) let ?full = f generateConfiguration -generateConfiguration :: Env' => IO AllHints +generateConfiguration :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full) + => IO AllHints generateConfiguration = do space <- shuffleM [ (i,j) | i <- sx, j<- sx] growPuzzle space [] -growPuzzle :: Env' => [(Int,Int)] -> [((Int,Int),Int)] -> IO AllHints +growPuzzle :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full) + => [(Int,Int)] -> [((Int,Int),Int)] -> IO AllHints -- reset search if we hit a hint selection with -- multiple solutions -growPuzzle [] _ = generateConfiguration +growPuzzle [] _ = putStrLn "did not find a puzzle" >> generateConfiguration growPuzzle (choice:space') entries = do letter <- randomRIO (0,?letters) let entries' = (choice,letter): entries @@ -247,41 +225,45 @@ else do -- We found an unsatisfiable set of hints. True <- solve ?solver (map entryValue entries) - generateHints - -generateHints :: Env' => IO AllHints -generateHints = do - s@(Solution sol) <- getSolution (puzzle ?full) - deleteSolver ?solver - solver <- newSolver - let ?solver = solver - f <- genFull - conFull f - let ?full = f - removeSolution s - let space = [((3,i),getLetter (Vector.toList (sol ! i))) | i <- sx] - ++ [((0,i),getLetter [(sol!j)!i | j<-sx]) | i <- sx] - ++ [((1,i),getLetter (reverse $ Vector.toList (sol ! i))) | i <- sx] - ++ [((2,i),getLetter $ reverse [(sol!j)!i | j<-sx]) | i <- sx] - space' <- shuffleM space - sat <- solve ?solver (map hintValue space') - minimize sat space' [] - where getLetter [] = error "Internal error: cannot find letter in solution!" - getLetter (Blank : r) = getLetter r - getLetter (Letter l : _) = l + 1 + s@(Solution sol) <- getSolution (puzzle ?full) + removeSolution s + let getLetters i = let soli = sol ! i + in [((3,i),getLetter [soli!j | j<- sx]), + ((0,i),getLetter [(sol!j)!i | j<-sx]), + ((1,i),getLetter [soli!j | j<- sx_reverse]), + ((2,i),getLetter [(sol!j)!i | j<-sx_reverse])] + space = concatMap getLetters sx + sat <- solve ?solver (map hintValue space) + if sat then generateConfiguration -- not unique, start again + else do -- check whether solution is it really unique + -- (we excluded some previous solutions) + deleteSolver ?solver + solver <- newSolver + let ?solver = solver + f <- genFull + conFull f + removeSolution s + sat <- solve ?solver (map hintValue space) + if sat then generateConfiguration -- not unique, start again + else do + space' <- shuffleM space + minimize space' [] + where getLetter = foldr getLetterRun (error "Internal error: cannot find letter in solution!") + getLetterRun Blank r = r + getLetterRun (Letter l) _ = l + 1 -- turn a hint position and letter into a literal -hintValue :: Env' => ((Int, Int), Int) -> Lit +hintValue :: (?full :: Full) => ((Int, Int), Int) -> Lit hintValue ((h,i),l) = (([top, right, bottom , left]!! h) (hints ?full) ! i) ! l -entryValue :: Env' => ((Int, Int), Int) -> Lit +entryValue :: (?full :: Full) => ((Int, Int), Int) -> Lit entryValue ((i,j),l) = (((puzzle ?full) ! i) ! j) ! l -minimize :: Env' => Bool -> [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints -minimize True [] _ = generateConfiguration -minimize False [] result = do +minimize :: (?size :: Int, ?letters :: Int, ?solver :: Solver, ?full :: Full) + => [((Int, Int), Int)] -> [((Int, Int), Int)] -> IO AllHints +minimize [] result = do -- We minimised the set of hints. Now we just verify that we indeed -- have a unique solution. deleteSolver ?solver @@ -297,9 +279,9 @@ sat' <- solve ?solver set when sat' (error "solution is wrong: not unique!") return(getAllHints ?size result) -minimize sat (h: r) acc = do sat' <- solve ?solver (map hintValue (r ++ acc)) - if sat' then minimize sat r (h:acc) - else minimize sat' r acc +minimize (h: r) acc = do sat' <- solve ?solver (map hintValue (r ++ acc)) + if sat' then minimize r (h:acc) + else minimize r acc main = do c <- getArgs