sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Puzzles.HexPuzzle

Description

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.

Synopsis

- data Color
  - = Black
  - | Blue
  - | Green
  - | Red
- type SColor = SBV Color
- sRed :: SBV Color
- sGreen :: SBV Color
- sBlue :: SBV Color
- sBlack :: SBV Color
- type Button = Word8
- type SButton = SBV Button
- type Grid = SArray Button Color
- next :: SButton -> Grid -> Grid
- search :: [Color] -> [Color] -> IO ()
- example :: IO ()

# Documentation

data Color Source #

Colors we're allowed

Constructors

Black |
Blue |
Green |
Red |

#### Instances

Instances details

Data Color Source # |

Instance details

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 Source #

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

toConstr :: Color -> Constr Source #

dataTypeOf :: Color -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Read Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods readsPrec :: Int -> ReadS Color Source # readList :: ReadS [Color] Source # readPrec :: ReadPrec Color Source # readListPrec :: ReadPrec [Color] Source #
Show Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods showsPrec :: Int -> Color -> ShowS Source # show :: Color -> String Source # showList :: [Color] -> ShowS Source #
Eq Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods (==) :: Color -> Color -> Bool Source # (/=) :: Color -> Color -> Bool Source #
Ord Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods compare :: Color -> Color -> Ordering Source # (<) :: Color -> Color -> Bool Source # (<=) :: Color -> Color -> Bool Source # (>) :: Color -> Color -> Bool Source # (>=) :: Color -> Color -> Bool Source # max :: Color -> Color -> Color Source # min :: Color -> Color -> Color Source #
SymVal Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

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

literal :: Color -> SBV Color Source #

fromCV :: CV -> Color Source #

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

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

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

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

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

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

unliteral :: SBV Color -> Maybe Color Source #

isConcrete :: SBV Color -> Bool Source #

isSymbolic :: SBV Color -> Bool Source #

HasKind Color Source # |

Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

kindOf :: Color -> Kind Source #

hasSign :: Color -> Bool Source #

intSizeOf :: Color -> Int Source #

isBoolean :: Color -> Bool Source #

isBounded :: Color -> Bool Source #

isReal :: Color -> Bool Source #

isFloat :: Color -> Bool Source #

isDouble :: Color -> Bool Source #

isRational :: Color -> Bool Source #

isFP :: Color -> Bool Source #

isUnbounded :: Color -> Bool Source #

isUserSort :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

isList :: Color -> Bool Source #

isSet :: Color -> Bool Source #

isTuple :: Color -> Bool Source #

isMaybe :: Color -> Bool Source #

isEither :: Color -> Bool Source #

showType :: Color -> String Source #

SatModel Color Source # |
Instance details Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle Methods parseCVs :: [CV] -> Maybe (Color, [CV]) Source # cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CV]) -> Maybe (b, [CV]) Source #

type SColor = SBV Color Source #

Symbolic version of the type `Color`.

sRed :: SBV Color Source #

Symbolic version of the constructor `Red`.

sGreen :: SBV Color Source #

Symbolic version of the constructor `Green`.

sBlue :: SBV Color Source #

Symbolic version of the constructor `Blue`.

sBlack :: SBV Color Source #

Symbolic version of the constructor `Black`.

type Button = Word8 Source #

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

type SButton = SBV Button Source #

Symbolic version of button.

type Grid = SArray Button Color Source #

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

next :: SButton -> Grid -> Grid Source #

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 () Source #

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 () Source #

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.