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

  -- we'll assert that arr[idx][idx] = 10
  let val :: SInteger
val = SArray (Integer, Integer) Integer
-> SBV (Integer, Integer) -> SInteger
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray (Integer, Integer) Integer
arr ((SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
idx, SInteger
idx))
  SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
val SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
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 <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
idx
                Integer
elt    <- SInteger -> Query Integer
forall a. SymVal a => SBV a -> Query a
getValue (SArray (Integer, Integer) Integer
-> SBV (Integer, Integer) -> SInteger
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray SArray (Integer, Integer) Integer
arr ((SInteger, SInteger) -> SBV (Integer, Integer)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SInteger
idx, SInteger
idx)))
                (Integer, Integer) -> Query (Integer, Integer)
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