rules :: AkariInst -> Symbolic SBool
rules inst = do
    let width = length (head inst)
    let height = length inst

    board <-
        forM [0..height-1] $ \r ->
            forM [0..width-1] $ \c ->
                (symbolic (show r ++ "-" ++ show c) :: Symbolic SBool)

    let getVar r c = if r >= 0 && r < height && c >= 0 && c < width then Just $ (board !! r) !! c else Nothing

    addConstraints $ do
        forM_ (zip3 [0 .. ] inst board) $ \(r, instRow, boardRow) ->
            forM_ (zip3 [0 .. ] instRow boardRow) $ \(c, instCell, var) ->
                do
                    -- constraints to match input numbers

                    case instCell
                      of (_, Just i) -> do
                            -- number of bulbs adjacent to this square are correct
                            addConstraint $ literal i .==
                                (sum $ map (\var -> ite var (literal 1) (literal 0)) $
                                catMaybes $ [getVar (r+1) c, getVar (r-1) c, getVar r (c-1), getVar r (c+1)])
                         (_, Nothing) ->
                            return ()

                    -- general bulb constraints

                    case instCell
                      of (Wall, _) -> do
                            -- no bulb on a wall
                            addConstraint $ var .== literal False
                         (Space, _) -> do
                            -- this space is LIT
                            let visibleSpaceInclusive = getVisibleSpace inst (r, c)
                            addConstraint $ orList $ map (\(r, c) -> (board !! r) !! c) visibleSpaceInclusive 

                            -- this space cannot simulatenously have a bulb if it is otherwise lit
                            let visibleSpaceExclusive = filter (/= (r, c)) visibleSpaceInclusive
                            forM_ visibleSpaceExclusive $ \(r1, c1) -> do
                                addConstraint $ bnot $ var &&& ((board !! r1) !! c1)
  where
    getVisibleSpace inst (r, c) =
      let
        width = length (head inst)
        height = length inst
        getRun r c deltaR deltaC =
          let
            r1 = r + deltaR
            c1 = c + deltaC
            isSpace = if r1 >= 0 && c1 >= 0 && r1 < height && c1 < width then
                case (inst !! r1) !! c1 of (Wall, _) -> False
                                           (Space, _) -> True
                else False
          in
            if isSpace then (r1, c1) : getRun r1 c1 deltaR deltaC
                       else []
      in
        [(r,c)] ++ getRun r c 0 (-1) ++ getRun r c 0 1 ++ getRun r c 1 0 ++ getRun r c (-1) 0
rules :: AkariInst -> Symbolic SBool
rules inst = do
    let width = length (head inst)
    let height = length inst

    board <-
        forM [0..height-1] $ \r ->
            forM [0..width-1] $ \c ->
                (symbolic (show r ++ "-" ++ show c) :: Symbolic SBool)

    let getVar r c = if r >= 0 && r < height && c >= 0 && c < width then Just $ (board !! r) !! c else Nothing

    addConstraints $ do
        forM_ (zip3 [0 .. ] inst board) $ \(r, instRow, boardRow) ->
            forM_ (zip3 [0 .. ] instRow boardRow) $ \(c, instCell, var) ->
                do
                    -- constraints to match input numbers

                    case instCell
                      of (_, Just i) -> do
                            -- number of bulbs adjacent to this square are correct
                            addConstraint $ literal i .==
                                (sum $ map (\var -> ite var (literal 1) (literal 0)) $
                                catMaybes $ [getVar (r+1) c, getVar (r-1) c, getVar r (c-1), getVar r (c+1)])
                         (_, Nothing) ->
                            return ()

                    -- general bulb constraints

                    case instCell
                      of (Wall, _) -> do
                            -- no bulb on a wall
                            addConstraint $ var .== literal False
                         (Space, _) -> do
                            -- this space is LIT
                            let visibleSpaceInclusive = getVisibleSpace inst (r, c)
                            addConstraint $ orList $ map (\(r, c) -> (board !! r) !! c) visibleSpaceInclusive 

                            -- this space cannot simulatenously have a bulb if it is otherwise lit
                            let visibleSpaceExclusive = filter (/= (r, c)) visibleSpaceInclusive
                            forM_ visibleSpaceExclusive $ \(r1, c1) -> do
                                addConstraint $ bnot $ var &&& ((board !! r1) !! c1)
  where
    getVisibleSpace inst (r, c) =
      let
        width = length (head inst)
        height = length inst
        getRun r c deltaR deltaC =
          let
            r1 = r + deltaR
            c1 = c + deltaC
            isSpace = if r1 >= 0 && c1 >= 0 && r1 < height && c1 < width then
                case (inst !! r1) !! c1 of (Wall, _) -> False
                                           (Space, _) -> True
                else False
          in
            if isSpace then (r1, c1) : getRun r1 c1 deltaR deltaC
                       else []
      in
        [(r,c)] ++ getRun r c 0 (-1) ++ getRun r c 0 1 ++ getRun r c 1 0 ++ getRun r c (-1) 0
rules inst = do
    let width = length (head inst)
    let height = length inst

    board <-
        forM [0..height-1] $ \r ->
            forM [0..width-1] $ \c ->
                (symbolic (show r ++ "-" ++ show c) :: Symbolic SBool)

    let getVar r c = if r >= 0 && r < height && c >= 0 && c < width then Just $ (board !! r) !! c else Nothing

    addConstraints $ do
        forM_ (zip3 [0 .. ] inst board) $ \(r, instRow, boardRow) ->
            forM_ (zip3 [0 .. ] instRow boardRow) $ \(c, instCell, var) ->
                do
                    -- constraints to match input numbers

                    case instCell
                      of (_, Just i) -> do
                            -- number of bulbs adjacent to this square are correct
                            addConstraint $ literal i .==
                                (sum $ map (\var -> ite var (literal 1) (literal 0)) $
                                catMaybes $ [getVar (r+1) c, getVar (r-1) c, getVar r (c-1), getVar r (c+1)])
                         (_, Nothing) ->
                            return ()

                    -- general bulb constraints

                    case instCell
                      of (Wall, _) -> do
                            -- no bulb on a wall
                            addConstraint $ var .== literal False
                         (Space, _) -> do
                            -- this space is LIT
                            let visibleSpaceInclusive = getVisibleSpace inst (r, c)
                            addConstraint $ orList $ map (\(r, c) -> (board !! r) !! c) visibleSpaceInclusive 

                            -- this space cannot simulatenously have a bulb if it is otherwise lit
                            let visibleSpaceExclusive = filter (/= (r, c)) visibleSpaceInclusive
                            forM_ visibleSpaceExclusive $ \(r1, c1) -> do
                                addConstraint $ bnot $ var &&& ((board !! r1) !! c1)
  where
    getVisibleSpace inst (r, c) =
      let
        width = length (head inst)
        height = length inst
        getRun r c deltaR deltaC =
          let
            r1 = r + deltaR
            c1 = c + deltaC
            isSpace = if r1 >= 0 && c1 >= 0 && r1 < height && c1 < width then
                case (inst !! r1) !! c1 of (Wall, _) -> False
                                           (Space, _) -> True
                else False
          in
            if isSpace then (r1, c1) : getRun r1 c1 deltaR deltaC
                       else []
      in
        [(r,c)] ++ getRun r c 0 (-1) ++ getRun r c 0 1 ++ getRun r c 1 0 ++ getRun r c (-1) 0