    -----------------------------------------------------------------------------
    -- |
    -- 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> SymbolicT IO a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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 a. a -> SymbolicT IO a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)+
                ]