    -----------------------------------------------------------------------------
    -- |
    -- 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