-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.LambdaArray
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates how lambda-abstractions can be used to model arrays.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Misc.LambdaArray where

import Data.SBV

-- | Given an array, and bounds on it, initialize it within the bounds to the element given.
-- Otherwise, leave it untouched.
memset :: SArray Integer Integer -> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset :: SArray Integer Integer
-> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset SArray Integer Integer
mem SInteger
lo SInteger
hi SInteger
newVal = (SInteger -> SInteger) -> SArray Integer Integer
forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b
lambdaArray SInteger -> SInteger
update
  where update :: SInteger -> SInteger
        update :: SInteger -> SInteger
update SInteger
idx = let oldVal :: SInteger
oldVal = SArray Integer Integer -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
readArray SArray Integer Integer
mem SInteger
idx
                     in SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
idx SBool -> SBool -> SBool
.&& SInteger
idx SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi) SInteger
newVal SInteger
oldVal

-- | Prove a simple property: If we read from the initialized region, we get the initial value. We have:
--
-- >>> memsetExample
-- Q.E.D.
memsetExample :: IO ThmResult
memsetExample :: IO ThmResult
memsetExample = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
   mem  <- String -> Symbolic (SArray Integer Integer)
forall a b. (SymVal a, SymVal b) => String -> Symbolic (SArray a b)
sArray   String
"mem"
   lo   <- sInteger "lo"
   hi   <- sInteger "hi"
   zero <- sInteger "zero"

   -- Get an index within lo/hi
   idx  <- sInteger "idx"
   constrain $ idx .>= lo .&& idx .<= hi

   -- It must be the case that we get zero back after mem-setting
   pure $ readArray (memset mem lo hi zero) idx .== zero

-- | Get an example of reading a value out of range. The value returned should be out-of-range for lo/hi
--
-- >>> outOfInit
-- Satisfiable. Model:
--   mem  = ([], 1) :: Array Integer Integer
--   lo   =       0 :: Integer
--   hi   =       0 :: Integer
--   zero =       0 :: Integer
--   idx  =       1 :: Integer
--   Read =       1 :: Integer
outOfInit :: IO SatResult
outOfInit :: IO SatResult
outOfInit = SymbolicT IO () -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO () -> IO SatResult)
-> SymbolicT IO () -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
   mem  <- String -> Symbolic (SArray Integer Integer)
forall a b. (SymVal a, SymVal b) => String -> Symbolic (SArray a b)
sArray String
"mem"
   lo   <- sInteger "lo"
   hi   <- sInteger "hi"
   zero <- sInteger "zero"

   -- Get a meaningful range:
   constrain $ lo .<= hi

   -- Get an index
   idx  <- sInteger "idx"

   -- Let read produce non-zero
   constrain $ observe "Read" (readArray (memset mem lo hi zero) idx) ./= zero