content: -----------------------------------------------------------------------------
  -- |
  -- 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 = runSMT $ do
    idx <- sInteger "idx"
    arr <- sArray_ :: Symbolic (SArray (Integer, Integer) Integer)
  
    -- we'll assert that arr[idx][idx] = 10
    let val = readArray arr (tuple (idx, idx))
    constrain $ val .== literal 10
  
    query $ do
      cs <- checkSat
      case cs of
        Sat -> do idxVal <- getValue idx
                  elt    <- getValue (readArray arr (tuple (idx, idx)))
                  pure (idxVal, elt)
        _   -> error $ "Solver said: " ++ show cs
  