    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Puzzles.U2Bridge
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The famous U2 bridge crossing puzzle: <http://www.braingle.com/brainteasers/515/u2.html>
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveAnyClass       #-}
    {-# LANGUAGE DeriveDataTypeable   #-}
    {-# LANGUAGE DeriveGeneric        #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE StandaloneDeriving   #-}
    {-# LANGUAGE TemplateHaskell      #-}

    {-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}

    module Documentation.SBV.Examples.Puzzles.U2Bridge where

    import Control.Monad       (unless)
    import Control.Monad.State (State, runState, put, get, gets, modify, evalState)

    import Data.List(sortOn)

    import GHC.Generics (Generic)

    import Data.SBV

    -------------------------------------------------------------
    -- * Modeling the puzzle
    -------------------------------------------------------------

    -- | U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the
    -- call to mkSymbolicEnumeration.
    data U2Member = Bono | Edge | Adam | Larry

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

    -- | Model time using 32 bits
    type Time  = Word32

    -- | Symbolic variant for time
    type STime = SBV Time

    -- | Crossing times for each member of the band
    crossTime :: U2Member -> Time
    crossTime :: U2Member -> Time
    crossTime U2Member
    Bono  = Time
    1
    crossTime U2Member
    Edge  = Time
    2
    crossTime U2Member
    Adam  = Time
    5
    crossTime U2Member
    Larry = Time
    10

    -- | The symbolic variant.. The duplication is unfortunate.
    sCrossTime :: SU2Member -> STime
    sCrossTime :: SU2Member -> STime
    sCrossTime SU2Member
    m =   SBool -> STime -> STime -> STime
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    m SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sBono) (Time -> STime
    forall a. SymVal a => a -> SBV a
    literal (U2Member -> Time
    crossTime U2Member
    Bono))
                   (STime -> STime) -> STime -> STime
    forall a b. (a -> b) -> a -> b
    $ SBool -> STime -> STime -> STime
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    m SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sEdge) (Time -> STime
    forall a. SymVal a => a -> SBV a
    literal (U2Member -> Time
    crossTime U2Member
    Edge))
                   (STime -> STime) -> STime -> STime
    forall a b. (a -> b) -> a -> b
    $ SBool -> STime -> STime -> STime
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    m SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sAdam) (Time -> STime
    forall a. SymVal a => a -> SBV a
    literal (U2Member -> Time
    crossTime U2Member
    Adam))
                                       (Time -> STime
    forall a. SymVal a => a -> SBV a
    literal (U2Member -> Time
    crossTime U2Member
    Larry)) -- Must be Larry

    -- | Location of the flash
    data Location = Here | There

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

    -- | The status of the puzzle after each move
    --
    -- This type is equipped with an automatically derived 'Mergeable' instance
    -- because each field is 'Mergeable'. A 'Generic' instance must also be derived
    -- for this to work, and the @DeriveAnyClass@ language extension must be
    -- enabled. The derived 'Mergeable' instance simply walks down the structure
    -- field by field and merges each one. An equivalent hand-written 'Mergeable'
    -- instance is provided in a comment below.
    data Status = Status { Status -> STime
    time   :: STime       -- ^ elapsed time
                         , Status -> SLocation
    flash  :: SLocation   -- ^ location of the flash
                         , Status -> SLocation
    lBono  :: SLocation   -- ^ location of Bono
                         , Status -> SLocation
    lEdge  :: SLocation   -- ^ location of Edge
                         , Status -> SLocation
    lAdam  :: SLocation   -- ^ location of Adam
                         , Status -> SLocation
    lLarry :: SLocation   -- ^ location of Larry
                         } deriving ((forall x. Status -> Rep Status x)
    -> (forall x. Rep Status x -> Status) -> Generic Status
    forall x. Rep Status x -> Status
    forall x. Status -> Rep Status x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Status -> Rep Status x
    from :: forall x. Status -> Rep Status x
    $cto :: forall x. Rep Status x -> Status
    to :: forall x. Rep Status x -> Status
    Generic, Bool -> SBool -> Status -> Status -> Status
    (Bool -> SBool -> Status -> Status -> Status)
    -> (forall b.
        (Ord b, SymVal b, Num b) =>
        [Status] -> Status -> SBV b -> Status)
    -> Mergeable Status
    forall b.
    (Ord b, SymVal b, Num b) =>
    [Status] -> Status -> SBV b -> Status
    forall a.
    (Bool -> SBool -> a -> a -> a)
    -> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
    -> Mergeable a
    $csymbolicMerge :: Bool -> SBool -> Status -> Status -> Status
    symbolicMerge :: Bool -> SBool -> Status -> Status -> Status
    $cselect :: forall b.
    (Ord b, SymVal b, Num b) =>
    [Status] -> Status -> SBV b -> Status
    select :: forall b.
    (Ord b, SymVal b, Num b) =>
    [Status] -> Status -> SBV b -> Status
    Mergeable)

    -- The derived Mergeable instance is equivalent to the following:
    --
    -- instance Mergeable Status where
    --   symbolicMerge f t s1 s2 = Status { time   = symbolicMerge f t (time   s1) (time   s2)
    --                                    , flash  = symbolicMerge f t (flash  s1) (flash  s2)
    --                                    , lBono  = symbolicMerge f t (lBono  s1) (lBono  s2)
    --                                    , lEdge  = symbolicMerge f t (lEdge  s1) (lEdge  s2)
    --                                    , lAdam  = symbolicMerge f t (lAdam  s1) (lAdam  s2)
    --                                    , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2)
    --                                    }

    -- | Start configuration, time elapsed is 0 and everybody is here
    start :: Status
    start :: Status
    start = Status { time :: STime
    time   = STime
    0
                   , flash :: SLocation
    flash  = SLocation
    sHere
                   , lBono :: SLocation
    lBono  = SLocation
    sHere
                   , lEdge :: SLocation
    lEdge  = SLocation
    sHere
                   , lAdam :: SLocation
    lAdam  = SLocation
    sHere
                   , lLarry :: SLocation
    lLarry = SLocation
    sHere
                   }

    -- | A puzzle move is modeled as a state-transformer
    type Move a = State Status a

    -- | Mergeable instance for 'Move' simply pushes the merging the data after run of each branch
    -- starting from the same state.
    instance Mergeable a => Mergeable (Move a) where
      symbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a
    symbolicMerge Bool
    f SBool
    t Move a
    a Move a
    b
        = do Status
    s <- StateT Status Identity Status
    forall s (m :: * -> *). MonadState s m => m s
    get
             let (a
    ar, Status
    s1) = Move a -> Status -> (a, Status)
    forall s a. State s a -> s -> (a, s)
    runState Move a
    a Status
    s
                 (a
    br, Status
    s2) = Move a -> Status -> (a, Status)
    forall s a. State s a -> s -> (a, s)
    runState Move a
    b Status
    s
             Status -> Move ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Status -> Move ()) -> Status -> Move ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> SBool -> Status -> Status -> Status
    forall a. Mergeable a => Bool -> SBool -> a -> a -> a
    symbolicMerge Bool
    f SBool
    t Status
    s1 Status
    s2
             a -> Move a
    forall a. a -> StateT Status Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Move a) -> a -> Move a
    forall a b. (a -> b) -> a -> b
    $ Bool -> SBool -> a -> a -> a
    forall a. Mergeable a => Bool -> SBool -> a -> a -> a
    symbolicMerge Bool
    f SBool
    t a
    ar a
    br

    -- | Read the state via an accessor function
    peek :: (Status -> a) -> Move a
    peek :: forall a. (Status -> a) -> Move a
    peek = (Status -> a) -> StateT Status Identity a
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets

    -- | Given an arbitrary member, return his location
    whereIs :: SU2Member -> Move SLocation
    whereIs :: SU2Member -> Move SLocation
    whereIs SU2Member
    p =  SBool -> Move SLocation -> Move SLocation -> Move SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sBono) ((Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    lBono)
               (Move SLocation -> Move SLocation)
    -> Move SLocation -> Move SLocation
    forall a b. (a -> b) -> a -> b
    $ SBool -> Move SLocation -> Move SLocation -> Move SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sEdge) ((Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    lEdge)
               (Move SLocation -> Move SLocation)
    -> Move SLocation -> Move SLocation
    forall a b. (a -> b) -> a -> b
    $ SBool -> Move SLocation -> Move SLocation -> Move SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sAdam) ((Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    lAdam)
                                   ((Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    lLarry)

    -- | Transferring the flash to the other side
    xferFlash :: Move ()
    xferFlash :: Move ()
    xferFlash = (Status -> Status) -> Move ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
    forall a b. (a -> b) -> a -> b
    $ \Status
    s -> Status
    s{flash :: SLocation
    flash = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (Status -> SLocation
    flash Status
    s SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sHere) SLocation
    sThere SLocation
    sHere}

    -- | Transferring a person to the other side
    xferPerson :: SU2Member -> Move ()
    xferPerson :: SU2Member -> Move ()
    xferPerson SU2Member
    p =  do ~[SLocation
    lb, SLocation
    le, SLocation
    la, SLocation
    ll] <- ((Status -> SLocation) -> Move SLocation)
    -> [Status -> SLocation] -> StateT Status Identity [SLocation]
    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 (Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek [Status -> SLocation
    lBono, Status -> SLocation
    lEdge, Status -> SLocation
    lAdam, Status -> SLocation
    lLarry]
                       let move :: SLocation -> SLocation
    move SLocation
    l = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SLocation
    l SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sHere) SLocation
    sThere SLocation
    sHere
                           lb' :: SLocation
    lb' = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sBono)  (SLocation -> SLocation
    move SLocation
    lb) SLocation
    lb
                           le' :: SLocation
    le' = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sEdge)  (SLocation -> SLocation
    move SLocation
    le) SLocation
    le
                           la' :: SLocation
    la' = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sAdam)  (SLocation -> SLocation
    move SLocation
    la) SLocation
    la
                           ll' :: SLocation
    ll' = SBool -> SLocation -> SLocation -> SLocation
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SU2Member
    p SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sLarry) (SLocation -> SLocation
    move SLocation
    ll) SLocation
    ll
                       (Status -> Status) -> Move ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
    forall a b. (a -> b) -> a -> b
    $ \Status
    s -> Status
    s{lBono :: SLocation
    lBono = SLocation
    lb', lEdge :: SLocation
    lEdge = SLocation
    le', lAdam :: SLocation
    lAdam = SLocation
    la', lLarry :: SLocation
    lLarry = SLocation
    ll'}

    -- | Increment the time, when only one person crosses
    bumpTime1 :: SU2Member -> Move ()
    bumpTime1 :: SU2Member -> Move ()
    bumpTime1 SU2Member
    p = (Status -> Status) -> Move ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
    forall a b. (a -> b) -> a -> b
    $ \Status
    s -> Status
    s{time :: STime
    time = Status -> STime
    time Status
    s STime -> STime -> STime
    forall a. Num a => a -> a -> a
    + SU2Member -> STime
    sCrossTime SU2Member
    p}

    -- | Increment the time, when two people cross together
    bumpTime2 :: SU2Member -> SU2Member -> Move ()
    bumpTime2 :: SU2Member -> SU2Member -> Move ()
    bumpTime2 SU2Member
    p1 SU2Member
    p2 = (Status -> Status) -> Move ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Status -> Status) -> Move ()) -> (Status -> Status) -> Move ()
    forall a b. (a -> b) -> a -> b
    $ \Status
    s -> Status
    s{time :: STime
    time = Status -> STime
    time Status
    s STime -> STime -> STime
    forall a. Num a => a -> a -> a
    + SU2Member -> STime
    sCrossTime SU2Member
    p1 STime -> STime -> STime
    forall a. OrdSymbolic a => a -> a -> a
    `smax` SU2Member -> STime
    sCrossTime SU2Member
    p2}

    -- | Symbolic version of 'Control.Monad.when'
    whenS :: SBool -> Move () -> Move ()
    whenS :: SBool -> Move () -> Move ()
    whenS SBool
    t Move ()
    a = SBool -> Move () -> Move () -> Move ()
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    t Move ()
    a (() -> Move ()
    forall a. a -> StateT Status Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    -- | Move one member, remembering to take the flash
    move1 :: SU2Member -> Move ()
    move1 :: SU2Member -> Move ()
    move1 SU2Member
    p = do SLocation
    f <- (Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    flash
                 SLocation
    l <- SU2Member -> Move SLocation
    whereIs SU2Member
    p
                 -- only do the move if the person and the flash are at the same side
                 SBool -> Move () -> Move ()
    whenS (SLocation
    f SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    l) (Move () -> Move ()) -> Move () -> Move ()
    forall a b. (a -> b) -> a -> b
    $ do SU2Member -> Move ()
    bumpTime1 SU2Member
    p
                                      Move ()
    xferFlash
                                      SU2Member -> Move ()
    xferPerson SU2Member
    p

    -- | Move two members, again with the flash
    move2 :: SU2Member -> SU2Member -> Move ()
    move2 :: SU2Member -> SU2Member -> Move ()
    move2 SU2Member
    p1 SU2Member
    p2 = do SLocation
    f  <- (Status -> SLocation) -> Move SLocation
    forall a. (Status -> a) -> Move a
    peek Status -> SLocation
    flash
                     SLocation
    l1 <- SU2Member -> Move SLocation
    whereIs SU2Member
    p1
                     SLocation
    l2 <- SU2Member -> Move SLocation
    whereIs SU2Member
    p2
                     -- only do the move if both people and the flash are at the same side
                     SBool -> Move () -> Move ()
    whenS (SLocation
    f SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    l1 SBool -> SBool -> SBool
    .&& SLocation
    f SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    l2) (Move () -> Move ()) -> Move () -> Move ()
    forall a b. (a -> b) -> a -> b
    $ do SU2Member -> SU2Member -> Move ()
    bumpTime2 SU2Member
    p1 SU2Member
    p2
                                                        Move ()
    xferFlash
                                                        SU2Member -> Move ()
    xferPerson SU2Member
    p1
                                                        SU2Member -> Move ()
    xferPerson SU2Member
    p2

    -------------------------------------------------------------
    -- * Actions
    -------------------------------------------------------------

    -- | A move action is a sequence of triples. The first component is symbolically
    -- True if only one member crosses. (In this case the third element of the triple
    -- is irrelevant.) If the first component is (symbolically) False, then both members
    -- move together
    type Actions = [(SBool, SU2Member, SU2Member)]

    -- | Run a sequence of given actions.
    run :: Actions -> Move [Status]
    run :: Actions -> Move [Status]
    run = ((SBool, SU2Member, SU2Member) -> StateT Status Identity Status)
    -> Actions -> Move [Status]
    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 (SBool, SU2Member, SU2Member) -> StateT Status Identity Status
    step
     where step :: (SBool, SU2Member, SU2Member) -> StateT Status Identity Status
    step (SBool
    b, SU2Member
    p1, SU2Member
    p2) = SBool -> Move () -> Move () -> Move ()
    forall a. Mergeable a => SBool -> a -> a -> a
    ite SBool
    b (SU2Member -> Move ()
    move1 SU2Member
    p1) (SU2Member -> SU2Member -> Move ()
    move2 SU2Member
    p1 SU2Member
    p2) Move ()
    -> StateT Status Identity Status -> StateT Status Identity Status
    forall a b.
    StateT Status Identity a
    -> StateT Status Identity b -> StateT Status Identity b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> StateT Status Identity Status
    forall s (m :: * -> *). MonadState s m => m s
    get

    -------------------------------------------------------------
    -- * Recognizing valid solutions
    -------------------------------------------------------------

    -- | Check if a given sequence of actions is valid, i.e., they must all
    -- cross the bridge according to the rules and in less than 17 seconds
    isValid :: Actions -> SBool
    isValid :: Actions -> SBool
    isValid Actions
    as = Status -> STime
    time Status
    end STime -> STime -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= STime
    17 SBool -> SBool -> SBool
    .&& ((SBool, SU2Member, SU2Member) -> SBool) -> Actions -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (SBool, SU2Member, SU2Member) -> SBool
    check Actions
    as SBool -> SBool -> SBool
    .&& [SLocation] -> [SLocation] -> SBool
    forall {b}. EqSymbolic b => [b] -> [b] -> SBool
    zigZag ([SLocation] -> [SLocation]
    forall a. HasCallStack => [a] -> [a]
    cycle [SLocation
    sThere, SLocation
    sHere]) ((Status -> SLocation) -> [Status] -> [SLocation]
    forall a b. (a -> b) -> [a] -> [b]
    map Status -> SLocation
    flash [Status]
    states) SBool -> SBool -> SBool
    .&& (SLocation -> SBool) -> [SLocation] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAll (SLocation -> SLocation -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SLocation
    sThere) [Status -> SLocation
    lBono Status
    end, Status -> SLocation
    lEdge Status
    end, Status -> SLocation
    lAdam Status
    end, Status -> SLocation
    lLarry Status
    end]
      where check :: (SBool, SU2Member, SU2Member) -> SBool
    check (SBool
    s, SU2Member
    p1, SU2Member
    p2) =   (SBool -> SBool
    sNot SBool
    s SBool -> SBool -> SBool
    .=> SU2Member
    p1 SU2Member -> SU2Member -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> SU2Member
    p2)       -- for two person moves, ensure first person is "larger"
                              SBool -> SBool -> SBool
    .&& (SBool
    s      SBool -> SBool -> SBool
    .=> SU2Member
    p2 SU2Member -> SU2Member -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SU2Member
    sBono)   -- for one person moves, ensure second person is always "bono"
            states :: [Status]
    states = Move [Status] -> Status -> [Status]
    forall s a. State s a -> s -> a
    evalState (Actions -> Move [Status]
    run Actions
    as) Status
    start
            end :: Status
    end = [Status] -> Status
    forall a. HasCallStack => [a] -> a
    last [Status]
    states
            zigZag :: [b] -> [b] -> SBool
    zigZag [b]
    reqs [b]
    locs = [SBool] -> SBool
    sAnd ([SBool] -> SBool) -> [SBool] -> SBool
    forall a b. (a -> b) -> a -> b
    $ (b -> b -> SBool) -> [b] -> [b] -> [SBool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith b -> b -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    (.==) [b]
    locs [b]
    reqs

    -------------------------------------------------------------
    -- * Solving the puzzle
    -------------------------------------------------------------

    -- | See if there is a solution that has precisely @n@ steps
    solveN :: Int -> IO Bool
    solveN :: Int -> IO Bool
    solveN Int
    n = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Checking for solutions with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " move" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    plu Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "."
                  let genAct :: SymbolicT IO (SBool, SU2Member, SU2Member)
    genAct = do SBool
    b  <- SymbolicT IO SBool
    forall a. SymVal a => Symbolic (SBV a)
    free_
                                  SU2Member
    p1 <- Symbolic SU2Member
    forall a. SymVal a => Symbolic (SBV a)
    free_
                                  SU2Member
    p2 <- Symbolic SU2Member
    forall a. SymVal a => Symbolic (SBV a)
    free_
                                  (SBool, SU2Member, SU2Member)
    -> SymbolicT IO (SBool, SU2Member, SU2Member)
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool
    b, SU2Member
    p1, SU2Member
    p2)
                  AllSatResult
    res <- SymbolicT IO SBool -> IO AllSatResult
    forall a. Satisfiable a => a -> IO AllSatResult
    allSat (SymbolicT IO SBool -> IO AllSatResult)
    -> SymbolicT IO SBool -> IO AllSatResult
    forall a b. (a -> b) -> a -> b
    $ Actions -> SBool
    isValid (Actions -> SBool) -> SymbolicT IO Actions -> SymbolicT IO SBool
    forall a b. (a -> b) -> SymbolicT IO a -> SymbolicT IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (Int -> SymbolicT IO (SBool, SU2Member, SU2Member))
    -> [Int] -> SymbolicT IO Actions
    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 (SymbolicT IO (SBool, SU2Member, SU2Member)
    -> Int -> SymbolicT IO (SBool, SU2Member, SU2Member)
    forall a b. a -> b -> a
    const SymbolicT IO (SBool, SU2Member, SU2Member)
    genAct) [Int
    1..Int
    n]
                  Int
    cnt <- ([(Bool, [(Bool, U2Member, U2Member)])]
     -> [(Bool, [(Bool, U2Member, U2Member)])])
    -> (Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ())
    -> AllSatResult
    -> IO Int
    forall a.
    SatModel a =>
    ([(Bool, a)] -> [(Bool, a)])
    -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
    displayModels (((Bool, [(Bool, U2Member, U2Member)]) -> String)
    -> [(Bool, [(Bool, U2Member, U2Member)])]
    -> [(Bool, [(Bool, U2Member, U2Member)])]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    sortOn (Bool, [(Bool, U2Member, U2Member)]) -> String
    forall a. Show a => a -> String
    show) Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
    disp AllSatResult
    res
                  if Int
    cnt Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                              else do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Found: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    cnt String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " solution" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    plu Int
    cnt String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " with " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " move" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall {a}. (Eq a, Num a) => a -> String
    plu Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "."
                                      Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
      where plu :: a -> String
    plu a
    v = if a
    v a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    1 then String
    "" else String
    "s"
            disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
            disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()
    disp Int
    i (Bool
    _, [(Bool, U2Member, U2Member)]
    ss)
             | Int
    lss Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    n = String -> IO ()
    forall a. HasCallStack => String -> a
    error (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Expected " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " results; got: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    lss
             | Bool
    True     = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Solution #" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": "
                             Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
    go Bool
    False Time
    0 [(Bool, U2Member, U2Member)]
    ss
                             () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
             where lss :: Int
    lss  = [(Bool, U2Member, U2Member)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Bool, U2Member, U2Member)]
    ss
                   go :: Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
    go Bool
    _ Time
    t []                   = String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Total time: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Time -> String
    forall a. Show a => a -> String
    show Time
    t
                   go Bool
    l Time
    t ((Bool
    True,  U2Member
    a, U2Member
    _):[(Bool, U2Member, U2Member)]
    rest) = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Time -> String
    forall a. Show a => a -> String
    sh2 Time
    t String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Bool -> String
    shL Bool
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ U2Member -> String
    forall a. Show a => a -> String
    show U2Member
    a
                                                    Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
    go (Bool -> Bool
    not Bool
    l) (Time
    t Time -> Time -> Time
    forall a. Num a => a -> a -> a
    + U2Member -> Time
    crossTime U2Member
    a) [(Bool, U2Member, U2Member)]
    rest
                   go Bool
    l Time
    t ((Bool
    False, U2Member
    a, U2Member
    b):[(Bool, U2Member, U2Member)]
    rest) = do String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Time -> String
    forall a. Show a => a -> String
    sh2 Time
    t String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Bool -> String
    shL Bool
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ U2Member -> String
    forall a. Show a => a -> String
    show U2Member
    a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ", " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ U2Member -> String
    forall a. Show a => a -> String
    show U2Member
    b
                                                    Bool -> Time -> [(Bool, U2Member, U2Member)] -> IO ()
    go (Bool -> Bool
    not Bool
    l) (Time
    t Time -> Time -> Time
    forall a. Num a => a -> a -> a
    + U2Member -> Time
    crossTime U2Member
    a Time -> Time -> Time
    forall a. Ord a => a -> a -> a
    `max` U2Member -> Time
    crossTime U2Member
    b) [(Bool, U2Member, U2Member)]
    rest
                   sh2 :: p -> String
    sh2 p
    t = let s :: String
    s = p -> String
    forall a. Show a => a -> String
    show p
    t in if String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    s Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    2 then Char
    ' ' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s else String
    s
                   shL :: Bool -> String
    shL Bool
    False = String
    " --> "
                   shL Bool
    True  = String
    " <-- "

    -- | Solve the U2-bridge crossing puzzle, starting by testing solutions with
    -- increasing number of steps, until we find one. We have:
    --
    -- >>> solveU2
    -- Checking for solutions with 1 move.
    -- Checking for solutions with 2 moves.
    -- Checking for solutions with 3 moves.
    -- Checking for solutions with 4 moves.
    -- Checking for solutions with 5 moves.
    -- Solution #1:
    --  0 --> Edge, Bono
    --  2 <-- Bono
    --  3 --> Larry, Adam
    -- 13 <-- Edge
    -- 15 --> Edge, Bono
    -- Total time: 17
    -- Solution #2:
    --  0 --> Edge, Bono
    --  2 <-- Edge
    --  4 --> Larry, Adam
    -- 14 <-- Bono
    -- 15 --> Edge, Bono
    -- Total time: 17
    -- Found: 2 solutions with 5 moves.
    --
    -- Finding all possible solutions to the puzzle.
    solveU2 :: IO ()
    solveU2 :: IO ()
    solveU2 = Int -> IO ()
    go Int
    1
     where go :: Int -> IO ()
    go Int
    i = do Bool
    p <- Int -> IO Bool
    solveN Int
    i
                     Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    p (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> IO ()
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)