-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Strings.RegexCrossword
-- Copyright : (c) Joel Burget
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- This example solves regex crosswords from <http://regexcrossword.com>
-----------------------------------------------------------------------------

{-# 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 Prelude hiding ((!!))
import Data.SBV.String ((!!))

import qualified Data.SBV.String as S
import qualified Data.SBV.RegExp as R

-- | Solve a given crossword, returning the corresponding rows
solveCrossword :: [R.RegExp] -> [R.RegExp] -> IO [String]
solveCrossword :: [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rowRegExps [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

        -- constrain rows
        let mkRow :: RegExp -> SymbolicT IO (SBV String)
mkRow 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

        -- constrain columns
        let mkCol :: RegExp -> SymbolicT IO (SBV String)
mkCol 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

        -- constrain each "cell" as they rows/columns intersect:
        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 <- [Integer
0..Integer
numColsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
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 <- [Integer
0..Integer
numRowsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
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)

        -- Now query to extract the solution
        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
                     CheckSatResult
Unk    -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"Solver returned unknown!"
                     DSat{} -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"Solver returned delta-sat!"
                     CheckSatResult
Unsat  -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"There are no solutions to this puzzle!"
                     CheckSatResult
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

-- | Solve <http://regexcrossword.com/challenges/intermediate/puzzles/1>
--
-- >>> puzzle1
-- ["ATO","WEL"]
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 String
"NOTAD")  -- [NOTAD]*
             , RegExp
"WEL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"BAL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"EAR"      -- WEL|BAL|EAR
             ]

        cs :: [RegExp]
cs = [ RegExp
"UB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"IE" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AW"         -- UB|IE|AW
             , RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"TUBE")   -- [TUBE]*
             , String -> RegExp
R.oneOf String
"BORF" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
R.All     -- [BORF].
             ]

-- | Solve <http://regexcrossword.com/challenges/intermediate/puzzles/2>
--
-- >>> puzzle2
-- ["WA","LK","ER"]
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 String
"AWE")       -- [AWE]+
             , RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf String
"ALP") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"K" -- [ALP]+K
             , RegExp
"PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"ER" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"EP"            -- (PR|ER|EP)
             ]

        cs :: [RegExp]
cs = [ String -> RegExp
R.oneOf String
"BQW" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* (RegExp
"PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"LE") -- [BQW](PR|LE)
             , RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf String
"RANK")      -- [RANK]+
             ]

-- | Solve <http://regexcrossword.com/challenges/palindromeda/puzzles/3>
--
-- >>> puzzle3
-- ["RATS","ABUT","TUBA","STAR"]
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 String
"TRASH")                -- [TRASH]*
            , (RegExp
"FA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AB") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"TUP")  -- (FA|AB)[TUP]*
            , RegExp -> RegExp
R.KStar (RegExp
"BA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"TH" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"TU")             -- (BA|TH|TU)*
            , RegExp -> RegExp
R.KStar RegExp
R.All RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All      -- .*A.*
            ]

       cs :: [RegExp]
cs = [ RegExp -> RegExp
R.KStar (RegExp
"TS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"RA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"QA")                     -- (TS|RA|QA)*
            , RegExp -> RegExp
R.KStar (RegExp
"AB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"UT" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AR")                     -- (AB|UT|AR)*
            , (RegExp
"K" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"T") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"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
* (RegExp
"A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"R")  -- (K|T)U.*(A|R)
            , RegExp -> RegExp
R.KPlus (RegExp
"AR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"FS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"ST")                     -- (AR|FS|ST)+
            ]