    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Uninterpreted.AUF
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Formalizes and proves the following theorem, about arithmetic,
    -- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf>
    -- slide number 24):
    --
    -- @
    --    x + 2 = y  implies  f (read (write (a, x, 3), y - 2)) = f (y - x + 1)
    -- @
    --
    -- We interpret the types as follows (other interpretations certainly possible):
    --
    --    [/x/] 'SWord32' (32-bit unsigned address)
    --
    --    [/y/] 'SWord32' (32-bit unsigned address)
    --
    --    [/a/] An array, indexed by 32-bit addresses, returning 32-bit unsigned integers
    --
    --    [/f/] An uninterpreted function of type @'SWord32' -> 'SWord64'@
    --
    -- The function @read@ and @write@ are usual array operations.
    -----------------------------------------------------------------------------

    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Uninterpreted.AUF where

    import Data.SBV

    --------------------------------------------------------------
    -- * Model using functional arrays
    --------------------------------------------------------------

    -- | Uninterpreted function in the theorem
    f :: SWord32 -> SWord64
    f :: SWord32 -> SWord64
    f = String -> SWord32 -> SWord64
    forall a. Uninterpreted a => String -> a
    uninterpret "f"

    -- | Correctness theorem. We state it for all values of @x@, @y@, and
    -- the given array @a@. Note that we're being generic in the type of
    -- array we're expecting.
    thm :: SymArray a => SWord32 -> SWord32 -> a Word32 Word32 -> SBool
    thm :: SWord32 -> SWord32 -> a Word32 Word32 -> SBool
    thm x :: SWord32
    x y :: SWord32
    y a :: a Word32 Word32
    a = SBool
    lhs SBool -> SBool -> SBool
    .=> SBool
    rhs
      where lhs :: SBool
    lhs = SWord32
    x SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    + 2 SWord32 -> SWord32 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SWord32
    y
            rhs :: SBool
    rhs =     SWord32 -> SWord64
    f (a Word32 Word32 -> SWord32 -> SWord32
    forall (array :: * -> * -> *) a b.
    SymArray array =>
    array a b -> SBV a -> SBV b
    readArray (a Word32 Word32 -> SWord32 -> SWord32 -> a Word32 Word32
    forall (array :: * -> * -> *) b a.
    (SymArray array, SymVal b) =>
    array a b -> SBV a -> SBV b -> array a b
    writeArray a Word32 Word32
    a SWord32
    x 3) (SWord32
    y SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    - 2))
                  SWord64 -> SWord64 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SWord32 -> SWord64
    f (SWord32
    y SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    - SWord32
    x SWord32 -> SWord32 -> SWord32
    forall a. Num a => a -> a -> a
    + 1)

    -- | Prove it using SMT-Lib arrays.
    --
    -- >>> proveSArray
    -- Q.E.D.
    proveSArray :: IO ThmResult
    proveSArray :: IO ThmResult
    proveSArray = 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
                    SWord32
    x <- String -> Symbolic SWord32
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "x"
                    SWord32
    y <- String -> Symbolic SWord32
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "y"
                    SArray Word32 Word32
    a :: SArray Word32 Word32 <- Maybe SWord32 -> Symbolic (SArray Word32 Word32)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe (SBV b) -> Symbolic (array a b)
    newArray_ Maybe SWord32
    forall a. Maybe a
    Nothing
                    SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SWord32 -> SWord32 -> SArray Word32 Word32 -> SBool
    forall (a :: * -> * -> *).
    SymArray a =>
    SWord32 -> SWord32 -> a Word32 Word32 -> SBool
    thm SWord32
    x SWord32
    y SArray Word32 Word32
    a

    -- | Prove it using SBV's internal functional arrays.
    --
    -- >>> proveSFunArray
    -- Q.E.D.
    proveSFunArray :: IO ThmResult
    proveSFunArray :: IO ThmResult
    proveSFunArray = 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
                    SWord32
    x <- String -> Symbolic SWord32
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "x"
                    SWord32
    y <- String -> Symbolic SWord32
    forall a. SymVal a => String -> Symbolic (SBV a)
    free "y"
                    SFunArray Word32 Word32
    a :: SFunArray Word32 Word32 <- Maybe SWord32 -> Symbolic (SFunArray Word32 Word32)
    forall (array :: * -> * -> *) a b.
    (SymArray array, HasKind a, HasKind b) =>
    Maybe (SBV b) -> Symbolic (array a b)
    newArray_ Maybe SWord32
    forall a. Maybe a
    Nothing
                    SBool -> SymbolicT IO SBool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
    forall a b. (a -> b) -> a -> b
    $ SWord32 -> SWord32 -> SFunArray Word32 Word32 -> SBool
    forall (a :: * -> * -> *).
    SymArray a =>
    SWord32 -> SWord32 -> a Word32 Word32 -> SBool
    thm SWord32
    x SWord32
    y SFunArray Word32 Word32
    a