    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.BMC
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Bounded model checking interface. See "Documentation.SBV.Examples.ProofTools.BMC"
    -- for an example use case.
    -----------------------------------------------------------------------------

    {-# LANGUAGE FlexibleContexts #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.BMC (
             bmc, bmcWith
           ) where

    import Data.SBV
    import Data.SBV.Control

    import Control.Monad (when)

    -- | Bounded model checking, using the default solver. See "Documentation.SBV.Examples.ProofTools.BMC"
    -- for an example use case.
    --
    -- Note that the BMC engine does *not* guarantee that the solution is unique. However, if it does
    -- find a solution at depth @i@, it is guaranteed that there are no shorter solutions.
    bmc :: (EqSymbolic st, Queriable IO st res)
        => Maybe Int                            -- ^ Optional bound
        -> Bool                                 -- ^ Verbose: prints iteration count
        -> Symbolic ()                          -- ^ Setup code, if necessary. (Typically used for 'Data.SBV.setOption' calls. Pass @return ()@ if not needed.)
        -> (st -> SBool)                        -- ^ Initial condition
        -> (st -> [st])                         -- ^ Transition relation
        -> (st -> SBool)                        -- ^ Goal to cover, i.e., we find a set of transitions that satisfy this predicate.
        -> IO (Either String (Int, [res]))      -- ^ Either a result, or a satisfying path of given length and intermediate observations.
    bmc :: Maybe Int
    -> Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> (st -> SBool)
    -> IO (Either String (Int, [res]))
    bmc = SMTConfig
    -> Maybe Int
    -> Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> (st -> SBool)
    -> IO (Either String (Int, [res]))
    forall st res.
    (EqSymbolic st, Queriable IO st res) =>
    SMTConfig
    -> Maybe Int
    -> Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> (st -> SBool)
    -> IO (Either String (Int, [res]))
    bmcWith SMTConfig
    defaultSMTCfg

    -- | Bounded model checking, configurable with the solver
    bmcWith :: (EqSymbolic st, Queriable IO st res)
            => SMTConfig
            -> Maybe Int
            -> Bool
            -> Symbolic ()
            -> (st -> SBool)
            -> (st -> [st])
            -> (st -> SBool)
            -> IO (Either String (Int, [res]))
    bmcWith :: SMTConfig
    -> Maybe Int
    -> Bool
    -> Symbolic ()
    -> (st -> SBool)
    -> (st -> [st])
    -> (st -> SBool)
    -> IO (Either String (Int, [res]))
    bmcWith cfg :: SMTConfig
    cfg mbLimit :: Maybe Int
    mbLimit chatty :: Bool
    chatty setup :: Symbolic ()
    setup initial :: st -> SBool
    initial trans :: st -> [st]
    trans goal :: st -> SBool
    goal
      = SMTConfig
    -> Symbolic (Either String (Int, [res]))
    -> IO (Either String (Int, [res]))
    forall a. SMTConfig -> Symbolic a -> IO a
    runSMTWith SMTConfig
    cfg (Symbolic (Either String (Int, [res]))
     -> IO (Either String (Int, [res])))
    -> Symbolic (Either String (Int, [res]))
    -> IO (Either String (Int, [res]))
    forall a b. (a -> b) -> a -> b
    $ do Symbolic ()
    setup
                            Query (Either String (Int, [res]))
    -> Symbolic (Either String (Int, [res]))
    forall a. Query a -> Symbolic a
    query (Query (Either String (Int, [res]))
     -> Symbolic (Either String (Int, [res])))
    -> Query (Either String (Int, [res]))
    -> Symbolic (Either String (Int, [res]))
    forall a b. (a -> b) -> a -> b
    $ do st
    state <- QueryT IO st
    forall (m :: * -> *) a b. Queriable m a b => QueryT m a
    create
                                       SBool -> QueryT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ st -> SBool
    initial st
    state
                                       Int -> st -> [st] -> Query (Either String (Int, [res]))
    forall b.
    Queriable IO st b =>
    Int -> st -> [st] -> QueryT IO (Either String (Int, [b]))
    go 0 st
    state []
       where go :: Int -> st -> [st] -> QueryT IO (Either String (Int, [b]))
    go i :: Int
    i _ _
              | Just l :: Int
    l <- Maybe Int
    mbLimit, Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    l
              = Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either String (Int, [b]) -> QueryT IO (Either String (Int, [b])))
    -> Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall a b. (a -> b) -> a -> b
    $ String -> Either String (Int, [b])
    forall a b. a -> Either a b
    Left (String -> Either String (Int, [b]))
    -> String -> Either String (Int, [b])
    forall a b. (a -> b) -> a -> b
    $ "BMC limit of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    l String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " reached"
             go i :: Int
    i curState :: st
    curState sofar :: [st]
    sofar = do Bool -> QueryT IO () -> QueryT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> QueryT IO ()
    forall a. IO a -> Query a
    io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "BMC: Iteration: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                      Int -> QueryT IO ()
    push 1
                                      SBool -> QueryT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ st -> SBool
    goal st
    curState
                                      CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                                      case CheckSatResult
    cs of
                                        Sat   -> do Bool -> QueryT IO () -> QueryT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> QueryT IO ()
    forall a. IO a -> Query a
    io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "BMC: Solution found at iteration " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                                    [b]
    ms <- (st -> QueryT IO b) -> [st] -> QueryT IO [b]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM st -> QueryT IO b
    forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
    project (st
    curState st -> [st] -> [st]
    forall a. a -> [a] -> [a]
    : [st]
    sofar)
                                                    Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either String (Int, [b]) -> QueryT IO (Either String (Int, [b])))
    -> Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall a b. (a -> b) -> a -> b
    $ (Int, [b]) -> Either String (Int, [b])
    forall a b. b -> Either a b
    Right (Int
    i, [b] -> [b]
    forall a. [a] -> [a]
    reverse [b]
    ms)
                                        Unk   -> do Bool -> QueryT IO () -> QueryT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    chatty (QueryT IO () -> QueryT IO ()) -> QueryT IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ IO () -> QueryT IO ()
    forall a. IO a -> Query a
    io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "BMC: Backend solver said unknown at iteration " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show  Int
    i
                                                    Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either String (Int, [b]) -> QueryT IO (Either String (Int, [b])))
    -> Either String (Int, [b]) -> QueryT IO (Either String (Int, [b]))
    forall a b. (a -> b) -> a -> b
    $ String -> Either String (Int, [b])
    forall a b. a -> Either a b
    Left (String -> Either String (Int, [b]))
    -> String -> Either String (Int, [b])
    forall a b. (a -> b) -> a -> b
    $ "BMC: Solver said unknown in iteration " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i
                                        Unsat -> do Int -> QueryT IO ()
    pop 1
                                                    st
    nextState <- QueryT IO st
    forall (m :: * -> *) a b. Queriable m a b => QueryT m a
    create
                                                    SBool -> QueryT IO ()
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
    forall a b. (a -> b) -> a -> b
    $ (st -> SBool) -> [st] -> SBool
    forall a. (a -> SBool) -> [a] -> SBool
    sAny (st
    nextState st -> st -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .==) (st -> [st]
    trans st
    curState)
                                                    Int -> st -> [st] -> QueryT IO (Either String (Int, [b]))
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) st
    nextState (st
    curState st -> [st] -> [st]
    forall a. a -> [a] -> [a]
    : [st]
    sofar)