-----------------------------------------------------------------------------
-- |
-- 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 = forall a. Symbolic a -> IO a
runSMT forall a b. (a -> b) -> a -> b
$ do
  SBV Integer
idx <- String -> Symbolic (SBV Integer)
sInteger String
"idx"
  SArray (Integer, Integer) Integer
arr <- forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> Symbolic (array a b)
newArray_ forall a. Maybe a
Nothing :: Symbolic (SArray (Integer, Integer) Integer)

  -- we'll assert that arr[idx][idx] = 10
  let val :: SBV Integer
val = forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray (Integer, Integer) Integer
arr (forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV Integer
idx, SBV Integer
idx))
  forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SBV Integer
val forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal Integer
10

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