-----------------------------------------------------------------------------
-- |
-- 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
   SArray Integer Integer
mem  <- String -> Symbolic (SArray Integer Integer)
forall a b. (SymVal a, SymVal b) => String -> Symbolic (SArray a b)
sArray   String
"mem"
   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 key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
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:
--   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
   SArray Integer Integer
mem  <- String -> Symbolic (SArray Integer Integer)
forall a b. (SymVal a, SymVal b) => String -> Symbolic (SArray a b)
sArray String
"mem"
   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 key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
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