    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Lists.Nested
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates nested lists
    -----------------------------------------------------------------------------

    {-# LANGUAGE OverloadedLists     #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Lists.Nested where

    import Data.SBV
    import Data.SBV.Control

    import Prelude hiding ((!!))
    import Data.SBV.List ((!!))
    import qualified Data.SBV.List as L

    -- | Simple example demonstrating the use of nested lists. We have:
    --
    -- Turned off. See: https://github.com/Z3Prover/z3/issues/2820
    -- nestedExample
    -- [[1,2,3],[4,5,6,7],[8,9,10],[11,12,13]]
    nestedExample :: IO ()
    nestedExample :: IO ()
    nestedExample = Symbolic () -> IO ()
    forall a. Symbolic a -> IO a
    runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do SList [Integer]
    a :: SList [Integer] <- String -> Symbolic (SList [Integer])
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "a"

                                SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SList [Integer]
    a SList [Integer] -> SInteger -> SBV [Integer]
    forall a. SymVal a => SList a -> SInteger -> SBV a
    !! SInteger
    0 SBV [Integer] -> SBV [Integer] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [Integer
    Item (SBV [Integer])
    1, Integer
    Item (SBV [Integer])
    2, Integer
    Item (SBV [Integer])
    3]
                                SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SList [Integer]
    a SList [Integer] -> SInteger -> SBV [Integer]
    forall a. SymVal a => SList a -> SInteger -> SBV a
    !! SInteger
    1 SBV [Integer] -> SBV [Integer] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [Integer
    Item (SBV [Integer])
    4, Integer
    Item (SBV [Integer])
    5, Integer
    Item (SBV [Integer])
    6, Integer
    Item (SBV [Integer])
    7]
                                SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SList [Integer] -> SList [Integer]
    forall a. SymVal a => SList a -> SList a
    L.tail (SList [Integer] -> SList [Integer]
    forall a. SymVal a => SList a -> SList a
    L.tail SList [Integer]
    a) SList [Integer] -> SList [Integer] -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [[Integer
    Item [Integer]
    8, Integer
    Item [Integer]
    9, Integer
    Item [Integer]
    10], [Integer
    Item [Integer]
    11, Integer
    Item [Integer]
    12, Integer
    Item [Integer]
    13]]
                                SBool -> Symbolic ()
    forall a. QuantifiedBool a => a -> Symbolic ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ SList [Integer] -> SInteger
    forall a. SymVal a => SList a -> SInteger
    L.length SList [Integer]
    a SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    4

                                Query () -> Symbolic ()
    forall a. Query a -> Symbolic a
    query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                                           case CheckSatResult
    cs of
                                             CheckSatResult
    Unk    -> String -> Query ()
    forall a. HasCallStack => String -> a
    error String
    "Solver said unknown!"
                                             DSat{} -> String -> Query ()
    forall a. HasCallStack => String -> a
    error String
    "Unexpected dsat result.."
                                             CheckSatResult
    Unsat  -> IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn String
    "Unsat"
                                             CheckSatResult
    Sat    -> do [[Integer]]
    v <- SList [Integer] -> Query [[Integer]]
    forall a. SymVal a => SBV a -> Query a
    getValue SList [Integer]
    a
                                                          IO () -> Query ()
    forall a. IO a -> Query a
    io (IO () -> Query ()) -> IO () -> Query ()
    forall a b. (a -> b) -> a -> b
    $ [[Integer]] -> IO ()
    forall a. Show a => a -> IO ()
    print [[Integer]]
    v