{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Strings.RegexCrossword where
import Data.List (genericLength, transpose)
import Data.SBV
import Data.SBV.Control
import Data.SBV.String ((.!!))
import qualified Data.SBV.String as S
import qualified Data.SBV.RegExp as R
solveCrossword :: [R.RegExp] -> [R.RegExp] -> IO [String]
solveCrossword :: [RegExp] -> [RegExp] -> IO [String]
solveCrossword rowRegExps :: [RegExp]
rowRegExps colRegExps :: [RegExp]
colRegExps = Symbolic [String] -> IO [String]
forall a. Symbolic a -> IO a
runSMT (Symbolic [String] -> IO [String])
-> Symbolic [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ do
let numRows :: Integer
numRows = [RegExp] -> Integer
forall i a. Num i => [a] -> i
genericLength [RegExp]
rowRegExps
numCols :: Integer
numCols = [RegExp] -> Integer
forall i a. Num i => [a] -> i
genericLength [RegExp]
colRegExps
let mkRow :: RegExp -> SymbolicT IO (SBV String)
mkRow rowRegExp :: RegExp
rowRegExp = do SBV String
row <- SymbolicT IO (SBV String)
forall a. SymVal a => Symbolic (SBV a)
free_
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV String
row SBV String -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
`R.match` RegExp
rowRegExp
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV String -> SInteger
S.length SBV String
row SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
numCols
SBV String -> SymbolicT IO (SBV String)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV String
row
[SBV String]
rows <- (RegExp -> SymbolicT IO (SBV String))
-> [RegExp] -> SymbolicT IO [SBV String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RegExp -> SymbolicT IO (SBV String)
mkRow [RegExp]
rowRegExps
let mkCol :: RegExp -> SymbolicT IO (SBV String)
mkCol colRegExp :: RegExp
colRegExp = do SBV String
col <- SymbolicT IO (SBV String)
forall a. SymVal a => Symbolic (SBV a)
free_
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV String
col SBV String -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
`R.match` RegExp
colRegExp
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV String -> SInteger
S.length SBV String
col SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
numRows
SBV String -> SymbolicT IO (SBV String)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV String
col
[SBV String]
cols <- (RegExp -> SymbolicT IO (SBV String))
-> [RegExp] -> SymbolicT IO [SBV String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RegExp -> SymbolicT IO (SBV String)
mkCol [RegExp]
colRegExps
let rowss :: [[SChar]]
rowss = [[SBV String
r SBV String -> SInteger -> SChar
.!! Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [0..Integer
numColsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1]] | SBV String
r <- [SBV String]
rows]
let colss :: [[SChar]]
colss = [[SChar]] -> [[SChar]]
forall a. [[a]] -> [[a]]
transpose [[SBV String
c SBV String -> SInteger -> SChar
.!! Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [0..Integer
numRowsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1]] | SBV String
c <- [SBV String]
cols]
SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd ([SBool] -> SBool) -> [SBool] -> SBool
forall a b. (a -> b) -> a -> b
$ (SChar -> SChar -> SBool) -> [SChar] -> [SChar] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SChar -> SChar -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==) ([[SChar]] -> [SChar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SChar]]
rowss) ([[SChar]] -> [SChar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SChar]]
colss)
Query [String] -> Symbolic [String]
forall a. Query a -> Symbolic a
query (Query [String] -> Symbolic [String])
-> Query [String] -> Symbolic [String]
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
case CheckSatResult
cs of
Unk -> String -> Query [String]
forall a. HasCallStack => String -> a
error "Solver returned unknown!"
Unsat -> String -> Query [String]
forall a. HasCallStack => String -> a
error "There are no solutions to this puzzle!"
Sat -> (SBV String -> QueryT IO String) -> [SBV String] -> Query [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV String -> QueryT IO String
forall a. SymVal a => SBV a -> Query a
getValue [SBV String]
rows
puzzle1 :: IO [String]
puzzle1 :: IO [String]
puzzle1 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf "NOTAD")
, "WEL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "BAL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "EAR"
]
cs :: [RegExp]
cs = [ "UB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "IE" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "AW"
, RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf "TUBE")
, String -> RegExp
R.oneOf "BORF" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
R.All
]
puzzle2 :: IO [String]
puzzle2 :: IO [String]
puzzle2 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf "AWE")
, RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf "ALP") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* "K"
, "PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "ER" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "EP"
]
cs :: [RegExp]
cs = [ String -> RegExp
R.oneOf "BQW" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* ("PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "LE")
, RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf "RANK")
]
puzzle3 :: IO [String]
puzzle3 :: IO [String]
puzzle3 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf "TRASH")
, ("FA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "AB") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf "TUP")
, RegExp -> RegExp
R.KStar ("BA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "TH" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "TU")
, RegExp -> RegExp
R.KStar RegExp
R.All RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* "A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All
]
cs :: [RegExp]
cs = [ RegExp -> RegExp
R.KStar ("TS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "RA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "QA")
, RegExp -> RegExp
R.KStar ("AB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "UT" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "AR")
, ("K" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "T") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* "U" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* ("A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "R")
, RegExp -> RegExp
R.KPlus ("AR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "FS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "ST")
]