-----------------------------------------------------------------------------
-- |
-- 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 #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE TypeOperators    #-}

{-# 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 ~ QueryResult st)
    => 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 ~ QueryResult st) =>
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 ~ QueryResult st) =>
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 ~ QueryResult st)
        => 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 ~ QueryResult st) =>
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 state <- QueryT IO st
forall (m :: * -> *) a. Queriable m a => QueryT m a
create
                                   constrain $ initial state
                                   go 0 state []
   where go :: Int -> st -> [st] -> Query (Either String (Int, [res]))
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, [res]) -> Query (Either String (Int, [res]))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Int, [res]) -> Query (Either String (Int, [res])))
-> Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Int, [res])
forall a b. a -> Either a b
Left (String -> Either String (Int, [res]))
-> String -> Either String (Int, [res])
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 a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ st -> SBool
goal st
curState
                                  cs <- Query CheckSatResult
checkSat
                                  case cs of
                                    DSat{} -> String -> Query (Either String (Int, [res]))
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
                                                 ms <- (st -> QueryT IO res) -> [st] -> QueryT IO [res]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM st -> QueryT IO res
st -> QueryT IO (QueryResult st)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project (st
curState st -> [st] -> [st]
forall a. a -> [a] -> [a]
: [st]
sofar)
                                                 return $ Right (i, reverse 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, [res]) -> Query (Either String (Int, [res]))
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Int, [res]) -> Query (Either String (Int, [res])))
-> Either String (Int, [res]) -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ String -> Either String (Int, [res])
forall a b. a -> Either a b
Left (String -> Either String (Int, [res]))
-> String -> Either String (Int, [res])
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
                                                 nextState <- QueryT IO st
forall (m :: * -> *) a. Queriable m a => QueryT m a
create
                                                 constrain $ sAny (nextState .==) (trans curState)
                                                 go (i+1) nextState (curState : sofar)