-----------------------------------------------------------------------------
-- |
-- 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
  idx <- String -> Symbolic (SBV Integer)
sInteger String
"idx"
  arr <- sArray_ :: Symbolic (SArray (Integer, Integer) Integer)

  -- we'll assert that arr[idx][idx] = 10
  let val = SArray (Integer, Integer) Integer
-> SBV (Integer, Integer) -> SBV Integer
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
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))
  constrain $ val .== literal 10

  query $ do
    cs <- checkSat
    case cs of
      CheckSatResult
Sat -> do idxVal <- SBV Integer -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SBV Integer
idx
                elt    <- getValue (readArray arr (tuple (idx, idx)))
                pure (idxVal, 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