    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.NestedArray
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates how to model nested-arrays, i.e., arrays of arrays in SBV.
    -- Instead of SMTLib's nested model, in SBV we use a tuple as an index,
    -- which is isomorphic to nested arrays.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Misc.NestedArray where

    import Data.SBV
    import Data.SBV.Tuple
    import Data.SBV.Control

    -- | Model a nested array that is indexed by integers, and we store
    -- another integer to integer array in each index. We have:
    --
    -- >>> nestedArray
    -- (0,10)
    nestedArray :: IO (Integer, Integer)
    nestedArray :: IO (Integer, Integer)
    nestedArray = Symbolic (Integer, Integer) -> IO (Integer, Integer)
    forall a. Symbolic a -> IO a
    runSMT (Symbolic (Integer, Integer) -> IO (Integer, Integer))
    -> Symbolic (Integer, Integer) -> IO (Integer, Integer)
    forall a b. (a -> b) -> a -> b
    $ do
      SBV Integer
    idx <- String -> Symbolic (SBV Integer)
    sInteger String
    "idx"
      SArray (Integer, Integer) Integer
    arr <- Maybe (SBV Integer) -> Symbolic (SArray (Integer, Integer) Integer)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe (SBV b) -> Symbolic (array a b)
    newArray_ Maybe (SBV Integer)
    forall a. Maybe a
    Nothing :: Symbolic (SArray (Integer, Integer) Integer)

      -- we'll assert that arr[idx][idx] = 10
      let val :: SBV Integer
    val = SArray (Integer, Integer) Integer
    -> SBV (Integer, Integer) -> SBV Integer
    forall a b. SArray a b -> SBV a -> SBV b
    forall (array :: * -> * -> *) a b.
    SymArray array =>
    array a b -> SBV a -> SBV b
    readArray SArray (Integer, Integer) Integer
    arr ((SBV Integer, SBV Integer) -> SBV (Integer, Integer)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SBV Integer
    idx, SBV Integer
    idx))
      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 Integer
    val SBV Integer -> SBV Integer -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== Integer -> SBV Integer
    forall a. SymVal a => a -> SBV a
    literal Integer
    10

      Query (Integer, Integer) -> Symbolic (Integer, Integer)
    forall a. Query a -> Symbolic a
    query (Query (Integer, Integer) -> Symbolic (Integer, Integer))
    -> Query (Integer, Integer) -> Symbolic (Integer, Integer)
    forall a b. (a -> b) -> a -> b
    $ do
        CheckSatResult
    cs <- Query CheckSatResult
    checkSat
        case CheckSatResult
    cs of
          CheckSatResult
    Sat -> do Integer
    idxVal <- SBV Integer -> Query Integer
    forall a. SymVal a => SBV a -> Query a
    getValue SBV Integer
    idx
                    Integer
    elt    <- SBV Integer -> Query Integer
    forall a. SymVal a => SBV a -> Query a
    getValue (SArray (Integer, Integer) Integer
    -> SBV (Integer, Integer) -> SBV Integer
    forall a b. SArray a b -> SBV a -> SBV b
    forall (array :: * -> * -> *) a b.
    SymArray array =>
    array a b -> SBV a -> SBV b
    readArray SArray (Integer, Integer) Integer
    arr ((SBV Integer, SBV Integer) -> SBV (Integer, Integer)
    forall tup a. Tuple tup a => a -> SBV tup
    tuple (SBV Integer
    idx, SBV Integer
    idx)))
                    (Integer, Integer) -> Query (Integer, Integer)
    forall a. a -> QueryT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer
    idxVal, Integer
    elt)
          CheckSatResult
    _   -> String -> Query (Integer, Integer)
    forall a. HasCallStack => String -> a
    error (String -> Query (Integer, Integer))
    -> String -> Query (Integer, Integer)
    forall a b. (a -> b) -> a -> b
    $ String
    "Solver said: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CheckSatResult -> String
    forall a. Show a => a -> String
    show CheckSatResult
    cs