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