-----------------------------------------------------------------------------
-- |
-- 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
lambdaAsArray SInteger -> SInteger
update
  where update :: SInteger -> SInteger
        update :: SInteger -> SInteger
update SInteger
idx = let oldVal :: SInteger
oldVal = SArray Integer Integer -> SInteger -> SInteger
forall a b. SArray a b -> SBV a -> SBV b
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
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
   SArray Integer Integer
mem  <- String -> Maybe SInteger -> Symbolic (SArray Integer Integer)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"mem" Maybe SInteger
forall a. Maybe a
Nothing

   SInteger
lo   <- String -> Symbolic SInteger
sInteger String
"lo"
   SInteger
hi   <- String -> Symbolic SInteger
sInteger String
"hi"
   SInteger
zero <- String -> Symbolic SInteger
sInteger String
"zero"

   -- Get an index within lo/hi
   SInteger
idx  <- String -> Symbolic SInteger
sInteger String
"idx"
   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
idx SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
lo SBool -> SBool -> SBool
.&& SInteger
idx SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi

   -- It must be the case that we get zero back after mem-setting
   SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SArray Integer Integer -> SInteger -> SInteger
forall a b. SArray a b -> SBV a -> SBV b
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray (SArray Integer Integer
-> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset SArray Integer Integer
mem SInteger
lo SInteger
hi SInteger
zero) SInteger
idx SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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:
--   Read = 1 :: Integer
--   lo   = 0 :: Integer
--   hi   = 0 :: Integer
--   zero = 0 :: Integer
--   idx  = 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
   SArray Integer Integer
mem  <- String -> Maybe SInteger -> Symbolic (SArray Integer Integer)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> Symbolic (array a b)
newArray String
"mem" Maybe SInteger
forall a. Maybe a
Nothing

   SInteger
lo   <- String -> Symbolic SInteger
sInteger String
"lo"
   SInteger
hi   <- String -> Symbolic SInteger
sInteger String
"hi"
   SInteger
zero <- String -> Symbolic SInteger
sInteger String
"zero"

   -- Get a meaningful range:
   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi

   -- Get an index
   SInteger
idx  <- String -> Symbolic SInteger
sInteger String
"idx"

   -- Let read produce non-zero
   SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ String -> SInteger -> SInteger
forall a. SymVal a => String -> SBV a -> SBV a
observe String
"Read" (SArray Integer Integer -> SInteger -> SInteger
forall a b. SArray a b -> SBV a -> SBV b
forall (array :: * -> * -> *) a b.
SymArray array =>
array a b -> SBV a -> SBV b
readArray (SArray Integer Integer
-> SInteger -> SInteger -> SInteger -> SArray Integer Integer
memset SArray Integer Integer
mem SInteger
lo SInteger
hi SInteger
zero) SInteger
idx) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SInteger
zero