    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.HexPuzzle
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- 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 = SArray 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 a b. SArray a b -> SBV a -> SBV b
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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 b a. SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b
    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 a b. SArray a b -> SBV a -> SBV b
    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. HasCallStack => [a] -> [a]
    tail [Button]
    xs [Button] -> [Button] -> [Button]
    forall a. [a] -> [a] -> [a]
    ++ [[Button] -> Button
    forall a. HasCallStack => [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 a b. (a -> b -> b) -> b -> [a] -> b
    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 b a. SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a b. SArray a b -> SBV a -> SBV b
    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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. QuantifiedBool a => a -> Query ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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]