{-# 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
data Color = Black | Blue | Green | Red
mkSymbolicEnumeration ''Color
type SColor = SBV Color
type Button = Word8
type SButton = SBV Button
type Grid = SFunArray Button Color
next :: SButton -> Grid -> Grid
next :: SButton -> Grid -> Grid
next b :: SButton
b g :: Grid
g = SBool -> Grid -> Grid -> Grid
forall a. Mergeable a => SBool -> a -> a -> a
ite (Grid -> SButton -> SBV Color
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
.== Color -> SBV Color
forall a. SymVal a => a -> SBV a
literal Color
Black) 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
.== 5) ([Button] -> Grid
rot [ 1, 2, 6, 10, 9, 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
.== 6) ([Button] -> Grid
rot [ 2, 3, 7, 11, 10, 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
.== 9) ([Button] -> Grid
rot [ 4, 5, 10, 14, 13, 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
.== 10) ([Button] -> Grid
rot [ 5, 6, 11, 15, 14, 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
.== 11) ([Button] -> Grid
rot [ 6, 7, 12, 16, 15, 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
.== 14) ([Button] -> Grid
rot [ 9, 10, 15, 18, 17, 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
.== 15) ([Button] -> Grid
rot [10, 11, 16, 19, 18, 14]) Grid
g
where rot :: [Button] -> Grid
rot xs :: [Button]
xs = ((Button, SBV Color) -> Grid -> Grid)
-> Grid -> [(Button, SBV Color)] -> Grid
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(i :: Button
i, c :: SBV Color
c) a :: Grid
a -> Grid -> SButton -> SBV Color -> Grid
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 (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. [a] -> [a]
tail [Button]
xs [Button] -> [Button] -> [Button]
forall a. [a] -> [a] -> [a]
++ [[Button] -> Button
forall a. [a] -> a
head [Button]
xs]
search :: [Color] -> [Color] -> IO ()
search :: [Color] -> [Color] -> IO ()
search initial :: [Color]
initial final :: [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 "emptyGrid" (SBV Color -> Maybe (SBV Color)
forall a. a -> Maybe a
Just (Color -> SBV Color
forall a. SymVal a => a -> SBV a
literal Color
Black))
let initGrid :: Grid
initGrid = ((Button, Color) -> Grid -> Grid)
-> Grid -> [(Button, Color)] -> Grid
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(i :: Button
i, c :: Color
c) a :: Grid
a -> Grid -> SButton -> SBV Color -> Grid
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 [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 (0 :: Int) Grid
initGrid []
where loop :: t -> Grid -> [SButton] -> Query ()
loop i :: t
i g :: Grid
g sofar :: [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
$ "Searching at depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i
Int -> Query ()
push 1
SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> 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 (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) [1..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
Unk -> String -> Query ()
forall a. HasCallStack => String -> a
error (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "Solver said Unknown, depth: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i
Unsat -> do
Int -> Query ()
pop 1
SButton
b <- String -> Query SButton
forall a. SymVal a => String -> Query (SBV a)
freshVar ("press_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i)
SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> 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 [5, 6, 9, 10, 11, 14, 15]
t -> Grid -> [SButton] -> Query ()
loop (t
it -> t -> t
forall a. Num a => a -> a -> a
+1) (SButton -> Grid -> Grid
next SButton
b Grid
g) ([SButton]
sofar [SButton] -> [SButton] -> [SButton]
forall a. [a] -> [a] -> [a]
++ [SButton
b])
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)
mapM SButton -> QueryT IO Button
forall a. SMTValue 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
$ "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, SMTValue b, Show b) =>
[SBV b] -> [b] -> Query ()
findOthers [SButton]
sofar [Button]
vs
findOthers :: [SBV b] -> [b] -> Query ()
findOthers vs :: [SBV b]
vs = [b] -> Query ()
go
where go :: [b] -> Query ()
go curVals :: [b]
curVals = do SBool -> Query ()
forall (m :: * -> *). SolverContext m => SBool -> 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 (\v :: SBV b
v c :: 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
Unk -> String -> Query ()
forall a. HasCallStack => String -> a
error "Unknown!"
Unsat -> IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn "There are no more solutions."
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)
mapM SBV b -> QueryT IO b
forall a. SMTValue 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
$ "Found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [b] -> String
forall a. Show a => a -> String
show [b]
newVals
[b] -> Query ()
go [b]
newVals
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]