-----------------------------------------------------------------------------
-- |
-- 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 = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
        let numRows :: Integer
numRows = forall i a. Num i => [a] -> i
genericLength [RegExp]
rowRegExps
            numCols :: Integer
numCols = 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 <- forall a. SymVal a => Symbolic (SBV a)
free_
                                 forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV String
row forall a. RegExpMatchable a => a -> RegExp -> SBool
`R.match` RegExp
rowRegExp
                                 forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV String -> SInteger
S.length SBV String
row forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal Integer
numCols
                                 forall (m :: * -> *) a. Monad m => a -> m a
return SBV String
row

        [SBV String]
rows <- 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 <- forall a. SymVal a => Symbolic (SBV a)
free_
                                 forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV String
col forall a. RegExpMatchable a => a -> RegExp -> SBool
`R.match` RegExp
colRegExp
                                 forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV String -> SInteger
S.length SBV String
col forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal Integer
numRows
                                 forall (m :: * -> *) a. Monad m => a -> m a
return SBV String
col

        [SBV String]
cols <- 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
!! forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [Integer
0..Integer
numColsforall a. Num a => a -> a -> a
-Integer
1]] | SBV String
r <- [SBV String]
rows]
        let colss :: [[SChar]]
colss = forall a. [[a]] -> [[a]]
transpose [[SBV String
c SBV String -> SInteger -> SChar
!! forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [Integer
0..Integer
numRowsforall a. Num a => a -> a -> a
-Integer
1]] | SBV String
c <- [SBV String]
cols]

        forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
sAnd forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. EqSymbolic a => a -> a -> SBool
(.==) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SChar]]
rowss) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SChar]]
colss)

        -- Now query to extract the solution
        forall a. Query a -> Symbolic a
query forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                   case CheckSatResult
cs of
                     CheckSatResult
Unk    -> forall a. HasCallStack => String -> a
error String
"Solver returned unknown!"
                     DSat{} -> forall a. HasCallStack => String -> a
error String
"Solver returned delta-sat!"
                     CheckSatResult
Unsat  -> forall a. HasCallStack => String -> a
error String
"There are no solutions to this puzzle!"
                     CheckSatResult
Sat    -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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" forall a. Num a => a -> a -> a
+ RegExp
"BAL" forall a. Num a => a -> a -> a
+ RegExp
"EAR"      -- WEL|BAL|EAR
             ]

        cs :: [RegExp]
cs = [ RegExp
"UB" forall a. Num a => a -> a -> a
+ RegExp
"IE" 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" 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") forall a. Num a => a -> a -> a
* RegExp
"K" -- [ALP]+K
             , RegExp
"PR" forall a. Num a => a -> a -> a
+ RegExp
"ER" forall a. Num a => a -> a -> a
+ RegExp
"EP"            -- (PR|ER|EP)
             ]

        cs :: [RegExp]
cs = [ String -> RegExp
R.oneOf String
"BQW" forall a. Num a => a -> a -> a
* (RegExp
"PR" 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" forall a. Num a => a -> a -> a
+ RegExp
"AB") 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" forall a. Num a => a -> a -> a
+ RegExp
"TH" forall a. Num a => a -> a -> a
+ RegExp
"TU")             -- (BA|TH|TU)*
            , RegExp -> RegExp
R.KStar RegExp
R.All forall a. Num a => a -> a -> a
* RegExp
"A" forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All      -- .*A.*
            ]

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