Documentation.SBV.Examples.Puzzles.HexPuzzle

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.

Documentation

data Color

Colors we're allowed

Constructors

Black

Blue

Green

Red

Instances

Data Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Color -> c Color

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Color

toConstr :: Color -> Constr

dataTypeOf :: Color -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Color)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Color)

gmapT :: (forall b. Data b => b -> b) -> Color -> Color

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Color -> r

gmapQ :: (forall d. Data d => d -> u) -> Color -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Color -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Color -> m Color

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Color -> m Color

Read Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

readsPrec :: Int -> ReadS Color

readList :: ReadS [Color]

readPrec :: ReadPrec Color

readListPrec :: ReadPrec [Color]

Show Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

showsPrec :: Int -> Color -> ShowS

show :: Color -> String

showList :: [Color] -> ShowS

Eq Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

(==) :: Color -> Color -> Bool

(/=) :: Color -> Color -> Bool

Ord Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

compare :: Color -> Color -> Ordering

(<) :: Color -> Color -> Bool

(<=) :: Color -> Color -> Bool

(>) :: Color -> Color -> Bool

(>=) :: Color -> Color -> Bool

max :: Color -> Color -> Color

min :: Color -> Color -> Color

SymVal Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Color)

literal :: Color -> SBV Color

fromCV :: CV -> Color

isConcretely :: SBV Color -> (Color -> Bool) -> Bool

sbvForall :: MonadSymbolic m => String -> m (SBV Color)

sbvForall_ :: MonadSymbolic m => m (SBV Color)

mkForallVars :: MonadSymbolic m => Int -> m [SBV Color]

sbvExists :: MonadSymbolic m => String -> m (SBV Color)

sbvExists_ :: MonadSymbolic m => m (SBV Color)

mkExistVars :: MonadSymbolic m => Int -> m [SBV Color]

free :: MonadSymbolic m => String -> m (SBV Color)

free_ :: MonadSymbolic m => m (SBV Color)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Color]

symbolic :: MonadSymbolic m => String -> m (SBV Color)

symbolics :: MonadSymbolic m => [String] -> m [SBV Color]

unliteral :: SBV Color -> Maybe Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

HasKind Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isRational :: Color -> Bool

isFP :: Color -> Bool

isUnbounded :: Color -> Bool

isUserSort :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

isList :: Color -> Bool

isSet :: Color -> Bool

isTuple :: Color -> Bool

isMaybe :: Color -> Bool

isEither :: Color -> Bool

showType :: Color -> String

SatModel Color

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

parseCVs :: [CV] -> Maybe (Color, [CV])

cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV])

type SColor = SBV Color

Symbolic version of the type Color.

sRed :: SBV Color

Symbolic version of the constructor Red.

sGreen :: SBV Color

Symbolic version of the constructor Green.

sBlue :: SBV Color

Symbolic version of the constructor Blue.

sBlack :: SBV Color

Symbolic version of the constructor Black.

type Button = Word8

Use 8-bit words for button numbers, even though we only have 1 to 19.

type SButton = SBV Button

Symbolic version of button.

type Grid = SArray Button Color

The grid is an array mapping each button to its color.

next :: SButton -> Grid -> Grid

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.

search :: [Color] -> [Color] -> IO ()

Iteratively search at increasing depths of button-presses to see if we can transform from the initial board position to a final board position.

example :: IO ()

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.