    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.ProofTools.BMC
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A BMC example, showing how traditional state-transition reachability
    -- problems can be coded using SBV, using bounded model checking.
    --
    -- We imagine a system with two integer variables, @x@ and @y@. At each
    -- iteration, we can either increment @x@ by @2@, or decrement @y@ by @4@.
    --
    -- Can we reach a state where @x@ and @y@ are the same starting from @x=0@
    -- and @y=10@?
    --
    -- What if @y@ starts at @11@?
    -----------------------------------------------------------------------------

    {-# LANGUAGE DeriveTraversable     #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE NamedFieldPuns        #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.ProofTools.BMC where

    import Data.SBV
    import Data.SBV.Tools.BMC
    import Data.SBV.Control

    -- * System state

    -- | System state, containing the two integers.
    data S a = S { forall a. S a -> a
    x :: a, forall a. S a -> a
    y :: a }
             deriving ((forall a b. (a -> b) -> S a -> S b)
    -> (forall a b. a -> S b -> S a) -> Functor S
    forall a b. a -> S b -> S a
    forall a b. (a -> b) -> S a -> S b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> S a -> S b
    fmap :: forall a b. (a -> b) -> S a -> S b
    $c<$ :: forall a b. a -> S b -> S a
    <$ :: forall a b. a -> S b -> S a
    Functor, (forall m. Monoid m => S m -> m)
    -> (forall m a. Monoid m => (a -> m) -> S a -> m)
    -> (forall m a. Monoid m => (a -> m) -> S a -> m)
    -> (forall a b. (a -> b -> b) -> b -> S a -> b)
    -> (forall a b. (a -> b -> b) -> b -> S a -> b)
    -> (forall b a. (b -> a -> b) -> b -> S a -> b)
    -> (forall b a. (b -> a -> b) -> b -> S a -> b)
    -> (forall a. (a -> a -> a) -> S a -> a)
    -> (forall a. (a -> a -> a) -> S a -> a)
    -> (forall a. S a -> [a])
    -> (forall a. S a -> Bool)
    -> (forall a. S a -> Int)
    -> (forall a. Eq a => a -> S a -> Bool)
    -> (forall a. Ord a => S a -> a)
    -> (forall a. Ord a => S a -> a)
    -> (forall a. Num a => S a -> a)
    -> (forall a. Num a => S a -> a)
    -> Foldable S
    forall a. Eq a => a -> S a -> Bool
    forall a. Num a => S a -> a
    forall a. Ord a => S a -> a
    forall m. Monoid m => S m -> m
    forall a. S a -> Bool
    forall a. S a -> Int
    forall a. S a -> [a]
    forall a. (a -> a -> a) -> S a -> a
    forall m a. Monoid m => (a -> m) -> S a -> m
    forall b a. (b -> a -> b) -> b -> S a -> b
    forall a b. (a -> b -> b) -> b -> S a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => S m -> m
    fold :: forall m. Monoid m => S m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> S a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> S a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> S a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> S a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> S a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> S a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> S a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> S a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> S a -> a
    foldr1 :: forall a. (a -> a -> a) -> S a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> S a -> a
    foldl1 :: forall a. (a -> a -> a) -> S a -> a
    $ctoList :: forall a. S a -> [a]
    toList :: forall a. S a -> [a]
    $cnull :: forall a. S a -> Bool
    null :: forall a. S a -> Bool
    $clength :: forall a. S a -> Int
    length :: forall a. S a -> Int
    $celem :: forall a. Eq a => a -> S a -> Bool
    elem :: forall a. Eq a => a -> S a -> Bool
    $cmaximum :: forall a. Ord a => S a -> a
    maximum :: forall a. Ord a => S a -> a
    $cminimum :: forall a. Ord a => S a -> a
    minimum :: forall a. Ord a => S a -> a
    $csum :: forall a. Num a => S a -> a
    sum :: forall a. Num a => S a -> a
    $cproduct :: forall a. Num a => S a -> a
    product :: forall a. Num a => S a -> a
    Foldable, Functor S
    Foldable S
    Functor S
    -> Foldable S
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> S a -> f (S b))
    -> (forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> S a -> m (S b))
    -> (forall (m :: * -> *) a. Monad m => S (m a) -> m (S a))
    -> Traversable S
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> S a -> f (S b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => S (f a) -> f (S a)
    $cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> S a -> m (S b)
    $csequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    sequence :: forall (m :: * -> *) a. Monad m => S (m a) -> m (S a)
    Traversable)

    -- | Show the state as a pair
    instance Show a => Show (S a) where
      show :: S a -> String
    show S{a
    x :: forall a. S a -> a
    x :: a
    x, a
    y :: forall a. S a -> a
    y :: a
    y} = (a, a) -> String
    forall a. Show a => a -> String
    show (a
    x, a
    y)

    -- | Symbolic equality for @S@.
    instance EqSymbolic a => EqSymbolic (S a) where
       S {x :: forall a. S a -> a
    x = a
    x1, y :: forall a. S a -> a
    y = a
    y1} .== :: S a -> S a -> SBool
    .== S {x :: forall a. S a -> a
    x = a
    x2, y :: forall a. S a -> a
    y = a
    y2} = a
    x1 a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    x2 SBool -> SBool -> SBool
    .&& a
    y1 a -> a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== a
    y2

    -- | 'Fresh' instance for our state
    instance Fresh IO (S SInteger) where
      fresh :: QueryT IO (S SInteger)
    fresh = SInteger -> SInteger -> S SInteger
    forall a. a -> a -> S a
    S (SInteger -> SInteger -> S SInteger)
    -> QueryT IO SInteger -> QueryT IO (SInteger -> S SInteger)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_ QueryT IO (SInteger -> S SInteger)
    -> QueryT IO SInteger -> QueryT IO (S SInteger)
    forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QueryT IO SInteger
    forall a. SymVal a => Query (SBV a)
    freshVar_

    -- * Encoding the problem

    -- | We parameterize over the initial state for different variations.
    problem :: Int -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
    problem :: Int
    -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
    problem Int
    lim S SInteger -> SBool
    initial = Maybe Int
    -> Bool
    -> Symbolic ()
    -> (S SInteger -> SBool)
    -> (S SInteger -> [S SInteger])
    -> (S SInteger -> SBool)
    -> IO (Either String (Int, [S Integer]))
    forall st res.
    (EqSymbolic st, Queriable IO st, res ~ QueryResult st) =>
    Maybe Int
    -> Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> (st -> SBool)
    -> IO (Either String (Int, [res]))
    bmc (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    lim) Bool
    True Symbolic ()
    setup S SInteger -> SBool
    initial S SInteger -> [S SInteger]
    trans S SInteger -> SBool
    goal
      where
            -- This is where we would put solver options, typically via
            -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
            -- so we simply do nothing.
            setup :: Symbolic ()
            setup :: Symbolic ()
    setup = () -> Symbolic ()
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

            -- Transition relation: At each step we either
            -- get to increase @x@ by 2, or decrement @y@ by 4:
            trans :: S SInteger -> [S SInteger]
            trans :: S SInteger -> [S SInteger]
    trans S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = [ S { x :: SInteger
    x = SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    2, y :: SInteger
    y = SInteger
    y     }
                            , S { x :: SInteger
    x = SInteger
    x,     y :: SInteger
    y = SInteger
    y SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - SInteger
    4 }
                            ]

            -- Goal state is when @x@ equals @y@:
            goal :: S SInteger -> SBool
            goal :: S SInteger -> SBool
    goal S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = SInteger
    x SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    y

    -- * Examples

    -- | Example 1: We start from @x=0@, @y=10@, and search up to depth @10@. We have:
    --
    -- >>> ex1
    -- BMC: Iteration: 0
    -- BMC: Iteration: 1
    -- BMC: Iteration: 2
    -- BMC: Iteration: 3
    -- BMC: Solution found at iteration 3
    -- Right (3,[(0,10),(0,6),(0,2),(2,2)])
    --
    -- As expected, there's a solution in this case. Furthermore, since the BMC engine
    -- found a solution at depth @3@, we also know that there is no solution at
    -- depths @0@, @1@, or @2@; i.e., this is "a" shortest solution. (That is,
    -- it may not be unique, but there isn't a shorter sequence to get us to
    -- our goal.)
    ex1 :: IO (Either String (Int, [S Integer]))
    ex1 :: IO (Either String (Int, [S Integer]))
    ex1 = Int
    -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
    problem Int
    10 S SInteger -> SBool
    isInitial
      where isInitial :: S SInteger -> SBool
            isInitial :: S SInteger -> SBool
    isInitial S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = SInteger
    x SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0 SBool -> SBool -> SBool
    .&& SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    10

    -- | Example 2: We start from @x=0@, @y=11@, and search up to depth @10@. We have:
    --
    -- >>> ex2
    -- BMC: Iteration: 0
    -- BMC: Iteration: 1
    -- BMC: Iteration: 2
    -- BMC: Iteration: 3
    -- BMC: Iteration: 4
    -- BMC: Iteration: 5
    -- BMC: Iteration: 6
    -- BMC: Iteration: 7
    -- BMC: Iteration: 8
    -- BMC: Iteration: 9
    -- Left "BMC limit of 10 reached"
    --
    -- As expected, there's no solution in this case. While SBV (and BMC) cannot establish
    -- that there is no solution at a larger depth, you can see that this will never be the
    -- case: In each step we do not change the parity of either variable. That is, @x@
    -- will remain even, and @y@ will remain odd. So, there will never be a solution at
    -- any depth. This isn't the only way to see this result of course, but the point
    -- remains that BMC is just not capable of establishing inductive facts.
    ex2 :: IO (Either String (Int, [S Integer]))
    ex2 :: IO (Either String (Int, [S Integer]))
    ex2 = Int
    -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
    problem Int
    10 S SInteger -> SBool
    isInitial
      where isInitial :: S SInteger -> SBool
            isInitial :: S SInteger -> SBool
    isInitial S{SInteger
    x :: forall a. S a -> a
    x :: SInteger
    x, SInteger
    y :: forall a. S a -> a
    y :: SInteger
    y} = SInteger
    x SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    0 SBool -> SBool -> SBool
    .&& SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== SInteger
    11