-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Puzzles.HexPuzzle
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A solution to the hexagon solver puzzle: <http://www5.cadence.com/2018ClubVQuiz_LP.html>
-- In case the above URL goes dead, here's an ASCII rendering of the problem.
--
-- We're given a board, with 19 hexagon cells. The cells are arranged as follows:
--
-- @
--                     01  02  03
--                   04  05  06  07
--                 08  09  10  11  12
--                   13  14  15  16
--                     17  18  19
-- @
--
--   - Each cell has a color, one of @BLACK@, @BLUE@, @GREEN@, or @RED@.
--
--   - At each step, you get to press one of the center buttons. That is,
--     one of 5, 6, 9, 10, 11, 14, or 15.
--
--   - Pressing a button that is currently colored @BLACK@ has no effect.
--
--   - Otherwise (i.e., if the pressed button is not @BLACK@), then colors
--     rotate clockwise around that button. For instance if you press 15
--     when it is not colored @BLACK@, then 11 moves to 16, 16 moves to 19,
--     19 moves to 18, 18 moves to 14, 14 moves to 10, and 10 moves to 11.
--
--   - Note that by "move," we mean the colors move: We still refer to the buttons
--     with the same number after a move.
--
-- You are given an initial board coloring, and a final one. Your goal is
-- to find a minimal sequence of button presses that will turn the original board
-- to the final one.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Puzzles.HexPuzzle where

import Data.SBV
import Data.SBV.Control

-- | Colors we're allowed
data Color = Black | Blue | Green | Red

-- | Make 'Color' a symbolic value.
mkSymbolicEnumeration ''Color

-- | Use 8-bit words for button numbers, even though we only have 1 to 19.
type Button  = Word8

-- | Symbolic version of button.
type SButton = SBV Button

-- | The grid is an array mapping each button to its color.
type Grid = SFunArray Button Color

-- | Given a button press, and the current grid, compute the next grid.
-- If the button is "unpressable", i.e., if it is not one of the center
-- buttons or it is currently colored black, we return the grid unchanged.
next :: SButton -> Grid -> Grid
next :: SButton -> Grid -> Grid
next SButton
b Grid
g = SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (Grid -> SButton -> SBV Color
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray Grid
g SButton
b SBV Color -> SBV Color -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Color
sBlack) Grid
g
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  SButton
5)                        ([Button] -> Grid
rot [ Button
1,  Button
2,  Button
6, Button
10,  Button
9,  Button
4])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  SButton
6)                        ([Button] -> Grid
rot [ Button
2,  Button
3,  Button
7, Button
11, Button
10,  Button
5])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.==  SButton
9)                        ([Button] -> Grid
rot [ Button
4,  Button
5, Button
10, Button
14, Button
13,  Button
8])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SButton
10)                        ([Button] -> Grid
rot [ Button
5,  Button
6, Button
11, Button
15, Button
14,  Button
9])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SButton
11)                        ([Button] -> Grid
rot [ Button
6,  Button
7, Button
12, Button
16, Button
15, Button
10])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SButton
14)                        ([Button] -> Grid
rot [ Button
9, Button
10, Button
15, Button
18, Button
17, Button
13])
         (Grid -> Grid) -> Grid -> Grid
forall a b. (a -> b) -> a -> b
$ SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (SButton
b SButton -> SButton -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SButton
15)                        ([Button] -> Grid
rot [Button
10, Button
11, Button
16, Button
19, Button
18, Button
14]) Grid
g
  where rot :: [Button] -> Grid
rot [Button]
xs = ((Button, SBV Color) -> Grid -> Grid)
-> Grid -> [(Button, SBV Color)] -> Grid
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Button
i, SBV Color
c) Grid
a -> Grid -> SButton -> SBV Color -> Grid
forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray Grid
a (Button -> SButton
forall a. SymVal a => a -> SBV a
literal Button
i) SBV Color
c) Grid
g ([Button] -> [SBV Color] -> [(Button, SBV Color)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Button]
new [SBV Color]
cur)
          where cur :: [SBV Color]
cur = (Button -> SBV Color) -> [Button] -> [SBV Color]
forall a b. (a -> b) -> [a] -> [b]
map (Grid -> SButton -> SBV Color
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray Grid
g (SButton -> SBV Color)
-> (Button -> SButton) -> Button -> SBV Color
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Button -> SButton
forall a. SymVal a => a -> SBV a
literal) [Button]
xs
                new :: [Button]
new = [Button] -> [Button]
forall a. [a] -> [a]
tail [Button]
xs [Button] -> [Button] -> [Button]
forall a. [a] -> [a] -> [a]
++ [[Button] -> Button
forall a. [a] -> a
head [Button]
xs]

-- | Iteratively search at increasing depths of button-presses to see if we can
-- transform from the initial board position to a final board position.
search :: [Color] -> [Color] -> IO ()
search :: [Color] -> [Color] -> IO ()
search [Color]
initial [Color]
final = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do Grid
emptyGrid :: Grid <- String -> Maybe (SBV Color) -> Symbolic Grid
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"emptyGrid" (SBV Color -> Maybe (SBV Color)
forall a. a -> Maybe a
Just SBV Color
sBlack)
                                   let initGrid :: Grid
initGrid = ((Button, Color) -> Grid -> Grid)
-> Grid -> [(Button, Color)] -> Grid
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Button
i, Color
c) Grid
a -> Grid -> SButton -> SBV Color -> Grid
forall (array :: * -> * -> *) b a.
(SymArray array, SymVal b) =>
array a b -> SBV a -> SBV b -> array a b
writeArray Grid
a (Button -> SButton
forall a. SymVal a => a -> SBV a
literal Button
i) (Color -> SBV Color
forall a. SymVal a => a -> SBV a
literal Color
c)) Grid
emptyGrid ([Button] -> [Color] -> [(Button, Color)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Button
1..] [Color]
initial)
                                   Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Grid -> [SButton] -> Query ()
forall t. (Show t, Num t) => t -> Grid -> [SButton] -> Query ()
loop (Int
0 :: Int) Grid
initGrid []

  where loop :: t -> Grid -> [SButton] -> Query ()
loop t
i Grid
g [SButton]
sofar = do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Searching at depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i

                            -- Go into a new context, and see if we've reached a solution:
                            Int -> Query ()
push Int
1
                            SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ (Button -> SBV Color) -> [Button] -> [SBV Color]
forall a b. (a -> b) -> [a] -> [b]
map (Grid -> SButton -> SBV Color
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray Grid
g (SButton -> SBV Color)
-> (Button -> SButton) -> Button -> SBV Color
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Button -> SButton
forall a. SymVal a => a -> SBV a
literal) [Button
1..Button
19] [SBV Color] -> [SBV Color] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (Color -> SBV Color) -> [Color] -> [SBV Color]
forall a b. (a -> b) -> [a] -> [b]
map Color -> SBV Color
forall a. SymVal a => a -> SBV a
literal [Color]
final
                            CheckSatResult
cs <- Query CheckSatResult
checkSat

                            case CheckSatResult
cs of
                              CheckSatResult
Unk    -> String -> Query ()
forall a. HasCallStack => String -> a
error (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Solver said Unknown, depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i

                              DSat{} -> String -> Query ()
forall a. HasCallStack => String -> a
error (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ String
"Solver returned a delta-satisfiable result, depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i

                              CheckSatResult
Unsat  -> do -- It didn't work out. Pop and try again with one more move:
                                           Int -> Query ()
pop Int
1
                                           SButton
b <- String -> Query SButton
forall a. SymVal a => String -> Query (SBV a)
freshVar (String
"press_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i)
                                           SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ SButton
b SButton -> [SButton] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` (Button -> SButton) -> [Button] -> [SButton]
forall a b. (a -> b) -> [a] -> [b]
map Button -> SButton
forall a. SymVal a => a -> SBV a
literal [Button
5, Button
6, Button
9, Button
10, Button
11, Button
14, Button
15]
                                           t -> Grid -> [SButton] -> Query ()
loop (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) (SButton -> Grid -> Grid
next SButton
b Grid
g) ([SButton]
sofar [SButton] -> [SButton] -> [SButton]
forall a. [a] -> [a] -> [a]
++ [SButton
b])

                              CheckSatResult
Sat    -> do [Button]
vs <- (SButton -> QueryT IO Button) -> [SButton] -> QueryT IO [Button]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SButton -> QueryT IO Button
forall a. SymVal a => SBV a -> Query a
getValue [SButton]
sofar
                                           IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Button] -> String
forall a. Show a => a -> String
show [Button]
vs
                                           [SButton] -> [Button] -> Query ()
forall b. (SymVal b, Show b) => [SBV b] -> [b] -> Query ()
findOthers [SButton]
sofar [Button]
vs

        findOthers :: [SBV b] -> [b] -> Query ()
findOthers [SBV b]
vs = [b] -> Query ()
go
                where go :: [b] -> Query ()
go [b]
curVals = do SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Query ()) -> SBool -> Query ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sOr ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (SBV b -> b -> SBool) -> [SBV b] -> [b] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SBV b
v b
c -> SBV b
v SBV b -> SBV b -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
c) [SBV b]
vs [b]
curVals
                                      CheckSatResult
cs <- Query CheckSatResult
checkSat
                                      case CheckSatResult
cs of
                                       CheckSatResult
Unk    -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Unknown!"
                                       DSat{} -> String -> Query ()
forall a. HasCallStack => String -> a
error String
"Delta-sat!"
                                       CheckSatResult
Unsat  -> IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"There are no more solutions."
                                       CheckSatResult
Sat    -> do [b]
newVals <- (SBV b -> QueryT IO b) -> [SBV b] -> QueryT IO [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV b -> QueryT IO b
forall a. SymVal a => SBV a -> Query a
getValue [SBV b]
vs
                                                    IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show [b]
newVals
                                                    [b] -> Query ()
go [b]
newVals

-- | A particular example run. We have:
--
-- >>> example
-- Searching at depth: 0
-- Searching at depth: 1
-- Searching at depth: 2
-- Searching at depth: 3
-- Searching at depth: 4
-- Searching at depth: 5
-- Searching at depth: 6
-- Found: [10,10,9,11,14,6]
-- Found: [10,10,11,9,14,6]
-- There are no more solutions.
example :: IO ()
example :: IO ()
example = [Color] -> [Color] -> IO ()
search [Color]
initBoard [Color]
finalBoard
   where initBoard :: [Color]
initBoard  = [Color
Black, Color
Black, Color
Black, Color
Red, Color
Blue, Color
Green, Color
Red, Color
Black, Color
Green, Color
Green, Color
Green, Color
Black, Color
Red, Color
Green, Color
Green, Color
Red, Color
Black, Color
Black, Color
Black]
         finalBoard :: [Color]
finalBoard = [Color
Black, Color
Red, Color
Black, Color
Black, Color
Green, Color
Green, Color
Black, Color
Red, Color
Green, Color
Blue, Color
Green, Color
Red, Color
Black, Color
Green, Color
Green, Color
Black, Color
Black, Color
Red, Color
Black]