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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Puzzles.HexPuzzle

Description

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.

Synopsis

Documentation

data Color Source #

Colors we're allowed

Constructors

Black 
Blue 
Green 
Red 
Instances
Eq Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

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

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

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 #

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 :: (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 #

Ord Color Source # 
Instance details

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 #

Read Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

readsPrec :: Int -> ReadS Color #

readList :: ReadS [Color] #

readPrec :: ReadPrec Color #

readListPrec :: ReadPrec [Color] #

Show Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

showsPrec :: Int -> Color -> ShowS #

show :: Color -> String #

showList :: [Color] -> ShowS #

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 #

isInteger :: Color -> Bool Source #

isUninterpreted :: Color -> Bool Source #

isChar :: Color -> Bool Source #

isString :: Color -> Bool Source #

showType :: Color -> String Source #

SymWord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

forall :: String -> Symbolic (SBV Color) Source #

forall_ :: Symbolic (SBV Color) Source #

mkForallVars :: Int -> Symbolic [SBV Color] Source #

exists :: String -> Symbolic (SBV Color) Source #

exists_ :: Symbolic (SBV Color) Source #

mkExistVars :: Int -> Symbolic [SBV Color] Source #

free :: String -> Symbolic (SBV Color) Source #

free_ :: Symbolic (SBV Color) Source #

mkFreeVars :: Int -> Symbolic [SBV Color] Source #

symbolic :: String -> Symbolic (SBV Color) Source #

symbolics :: [String] -> Symbolic [SBV Color] Source #

literal :: Color -> SBV Color Source #

unliteral :: SBV Color -> Maybe Color Source #

fromCW :: CW -> Color Source #

isConcrete :: SBV Color -> Bool Source #

isSymbolic :: SBV Color -> Bool Source #

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

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color) Source #

SatModel Color Source #

Make Color a symbolic value.

Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

parseCWs :: [CW] -> Maybe (Color, [CW]) Source #

cvtModel :: (Color -> Maybe b) -> Maybe (Color, [CW]) -> Maybe (b, [CW]) Source #

SMTValue Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

Methods

sexprToVal :: SExpr -> Maybe Color Source #

type SColor = SBV Color Source #

Give symbolic colors a name for convenience.

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 = SFunArray 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,11,9,14,6]
Found: [10,10,9,11,14,6]
There are no more solutions.