-----------------------------------------------------------------------------
-- |
-- 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 SMTConfig
cfg Maybe Int
mbLimit Bool
chatty Symbolic ()
setup st -> SBool
initial st -> [st]
trans 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 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 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
$ String
"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]
++ String
" reached"
         go Int
i st
curState [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
$ String
"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 Int
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
                                    DSat{} -> String -> QueryT IO (Either String (Int, [b]))
forall a. HasCallStack => String -> a
error String
"BMC: Solver returned an unexpected delta-sat result."
                                    CheckSatResult
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
$ String
"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)
                                    CheckSatResult
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
$ String
"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
$ String
"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
                                    CheckSatResult
Unsat  -> do Int -> QueryT IO ()
pop Int
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
+Int
1) st
nextState (st
curState st -> [st] -> [st]
forall a. a -> [a] -> [a]
: [st]
sofar)