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

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 :: SBV U2Member -> STime
sCrossTime SBV U2Member
m =   SBool -> STime -> STime -> STime
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV U2Member
m SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
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 (SBV U2Member
m SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
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 (SBV U2Member
m SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
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 -> SBV Location
flash  :: SLocation   -- ^ location of the flash
                     , Status -> SBV Location
lBono  :: SLocation   -- ^ location of Bono
                     , Status -> SBV Location
lEdge  :: SLocation   -- ^ location of Edge
                     , Status -> SBV Location
lAdam  :: SLocation   -- ^ location of Adam
                     , Status -> SBV Location
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
$cto :: forall x. Rep Status x -> Status
$cfrom :: forall x. Status -> Rep Status x
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
select :: [Status] -> Status -> SBV b -> Status
$cselect :: forall b.
(Ord b, SymVal b, Num b) =>
[Status] -> Status -> SBV b -> Status
symbolicMerge :: Bool -> SBool -> Status -> Status -> Status
$csymbolicMerge :: Bool -> SBool -> Status -> Status -> 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 :: STime
-> SBV Location
-> SBV Location
-> SBV Location
-> SBV Location
-> SBV Location
-> Status
Status { time :: STime
time   = STime
0
               , flash :: SBV Location
flash  = SBV Location
sHere
               , lBono :: SBV Location
lBono  = SBV Location
sHere
               , lEdge :: SBV Location
lEdge  = SBV Location
sHere
               , lAdam :: SBV Location
lAdam  = SBV Location
sHere
               , lLarry :: SBV Location
lLarry = SBV Location
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 -> StateT Status Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Status -> StateT Status Identity ())
-> Status -> StateT Status Identity ()
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 (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 :: (Status -> a) -> Move a
peek = (Status -> a) -> Move 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 :: SBV U2Member -> Move (SBV Location)
whereIs SBV U2Member
p =  SBool
-> Move (SBV Location)
-> Move (SBV Location)
-> Move (SBV Location)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV U2Member
p SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
sBono) ((Status -> SBV Location) -> Move (SBV Location)
forall a. (Status -> a) -> Move a
peek Status -> SBV Location
lBono)
           (Move (SBV Location) -> Move (SBV Location))
-> Move (SBV Location) -> Move (SBV Location)
forall a b. (a -> b) -> a -> b
$ SBool
-> Move (SBV Location)
-> Move (SBV Location)
-> Move (SBV Location)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV U2Member
p SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
sEdge) ((Status -> SBV Location) -> Move (SBV Location)
forall a. (Status -> a) -> Move a
peek Status -> SBV Location
lEdge)
           (Move (SBV Location) -> Move (SBV Location))
-> Move (SBV Location) -> Move (SBV Location)
forall a b. (a -> b) -> a -> b
$ SBool
-> Move (SBV Location)
-> Move (SBV Location)
-> Move (SBV Location)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV U2Member
p SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
sAdam) ((Status -> SBV Location) -> Move (SBV Location)
forall a. (Status -> a) -> Move a
peek Status -> SBV Location
lAdam)
                               ((Status -> SBV Location) -> Move (SBV Location)
forall a. (Status -> a) -> Move a
peek Status -> SBV Location
lLarry)

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

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

-- | Increment the time, when only one person crosses
bumpTime1 :: SU2Member -> Move ()
bumpTime1 :: SBV U2Member -> StateT Status Identity ()
bumpTime1 SBV U2Member
p = (Status -> Status) -> StateT Status Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> StateT Status Identity ())
-> (Status -> Status) -> StateT Status Identity ()
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
+ SBV U2Member -> STime
sCrossTime SBV U2Member
p}

-- | Increment the time, when two people cross together
bumpTime2 :: SU2Member -> SU2Member -> Move ()
bumpTime2 :: SBV U2Member -> SBV U2Member -> StateT Status Identity ()
bumpTime2 SBV U2Member
p1 SBV U2Member
p2 = (Status -> Status) -> StateT Status Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Status -> Status) -> StateT Status Identity ())
-> (Status -> Status) -> StateT Status Identity ()
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
+ SBV U2Member -> STime
sCrossTime SBV U2Member
p1 STime -> STime -> STime
forall a. OrdSymbolic a => a -> a -> a
`smax` SBV U2Member -> STime
sCrossTime SBV U2Member
p2}

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

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

-- | Move two members, again with the flash
move2 :: SU2Member -> SU2Member -> Move ()
move2 :: SBV U2Member -> SBV U2Member -> StateT Status Identity ()
move2 SBV U2Member
p1 SBV U2Member
p2 = do SBV Location
f  <- (Status -> SBV Location) -> Move (SBV Location)
forall a. (Status -> a) -> Move a
peek Status -> SBV Location
flash
                 SBV Location
l1 <- SBV U2Member -> Move (SBV Location)
whereIs SBV U2Member
p1
                 SBV Location
l2 <- SBV U2Member -> Move (SBV Location)
whereIs SBV U2Member
p2
                 -- only do the move if both people and the flash are at the same side
                 SBool -> StateT Status Identity () -> StateT Status Identity ()
whenS (SBV Location
f SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
l1 SBool -> SBool -> SBool
.&& SBV Location
f SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
l2) (StateT Status Identity () -> StateT Status Identity ())
-> StateT Status Identity () -> StateT Status Identity ()
forall a b. (a -> b) -> a -> b
$ do SBV U2Member -> SBV U2Member -> StateT Status Identity ()
bumpTime2 SBV U2Member
p1 SBV U2Member
p2
                                                    StateT Status Identity ()
xferFlash
                                                    SBV U2Member -> StateT Status Identity ()
xferPerson SBV U2Member
p1
                                                    SBV U2Member -> StateT Status Identity ()
xferPerson SBV U2Member
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, SBV U2Member, SBV U2Member)
 -> StateT Status Identity Status)
-> Actions -> Move [Status]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SBool, SBV U2Member, SBV U2Member)
-> StateT Status Identity Status
step
 where step :: (SBool, SBV U2Member, SBV U2Member)
-> StateT Status Identity Status
step (SBool
b, SBV U2Member
p1, SBV U2Member
p2) = SBool
-> StateT Status Identity ()
-> StateT Status Identity ()
-> StateT Status Identity ()
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b (SBV U2Member -> StateT Status Identity ()
move1 SBV U2Member
p1) (SBV U2Member -> SBV U2Member -> StateT Status Identity ()
move2 SBV U2Member
p1 SBV U2Member
p2) StateT Status Identity ()
-> StateT Status Identity Status -> StateT Status Identity Status
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, SBV U2Member, SBV U2Member) -> SBool) -> Actions -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (SBool, SBV U2Member, SBV U2Member) -> SBool
check Actions
as SBool -> SBool -> SBool
.&& [SBV Location] -> [SBV Location] -> SBool
forall a. EqSymbolic a => [a] -> [a] -> SBool
zigZag ([SBV Location] -> [SBV Location]
forall a. [a] -> [a]
cycle [SBV Location
sThere, SBV Location
sHere]) ((Status -> SBV Location) -> [Status] -> [SBV Location]
forall a b. (a -> b) -> [a] -> [b]
map Status -> SBV Location
flash [Status]
states) SBool -> SBool -> SBool
.&& (SBV Location -> SBool) -> [SBV Location] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll (SBV Location -> SBV Location -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Location
sThere) [Status -> SBV Location
lBono Status
end, Status -> SBV Location
lEdge Status
end, Status -> SBV Location
lAdam Status
end, Status -> SBV Location
lLarry Status
end]
  where check :: (SBool, SBV U2Member, SBV U2Member) -> SBool
check (SBool
s, SBV U2Member
p1, SBV U2Member
p2) =   (SBool -> SBool
sNot SBool
s SBool -> SBool -> SBool
.=> SBV U2Member
p1 SBV U2Member -> SBV U2Member -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SBV U2Member
p2)       -- for two person moves, ensure first person is "larger"
                          SBool -> SBool -> SBool
.&& (SBool
s      SBool -> SBool -> SBool
.=> SBV U2Member
p2 SBV U2Member -> SBV U2Member -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV U2Member
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. [a] -> a
last [Status]
states
        zigZag :: [a] -> [a] -> SBool
zigZag [a]
reqs [a]
locs = [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (a -> a -> SBool) -> [a] -> [a] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==) [a]
locs [a]
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, SBV U2Member, SBV U2Member)
genAct = do SBool
b  <- Symbolic SBool
forall a. SymVal a => Symbolic (SBV a)
exists_
                              SBV U2Member
p1 <- Symbolic (SBV U2Member)
forall a. SymVal a => Symbolic (SBV a)
exists_
                              SBV U2Member
p2 <- Symbolic (SBV U2Member)
forall a. SymVal a => Symbolic (SBV a)
exists_
                              (SBool, SBV U2Member, SBV U2Member)
-> SymbolicT IO (SBool, SBV U2Member, SBV U2Member)
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool
b, SBV U2Member
p1, SBV U2Member
p2)
              AllSatResult
res <- Symbolic SBool -> IO AllSatResult
forall a. Provable a => a -> IO AllSatResult
allSat (Symbolic SBool -> IO AllSatResult)
-> Symbolic SBool -> IO AllSatResult
forall a b. (a -> b) -> a -> b
$ Actions -> SBool
isValid (Actions -> SBool) -> SymbolicT IO Actions -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Int -> SymbolicT IO (SBool, SBV U2Member, SBV U2Member))
-> [Int] -> SymbolicT IO Actions
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SymbolicT IO (SBool, SBV U2Member, SBV U2Member)
-> Int -> SymbolicT IO (SBool, SBV U2Member, SBV U2Member)
forall a b. a -> b -> a
const SymbolicT IO (SBool, SBV U2Member, SBV U2Member)
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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return ()
         where lss :: Int
lss  = [(Bool, U2Member, U2Member)] -> 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 :: a -> String
sh2 a
t = let s :: String
s = a -> String
forall a. Show a => a -> String
show a
t in if String -> 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)