-----------------------------------------------------------------------------
-- |
-- 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 (
         bmcRefute, bmcRefuteWith, bmcCover, bmcCoverWith
       ) where

import Data.SBV
import Data.SBV.Control

import Control.Monad (when)

-- | Are we covering or refuting?
data BMCKind = Refute
             | Cover

-- | Refutation using bounded model checking, using the default solver. This version tries to refute the goal
-- in a depth-first fashion. Note that this method can find a refutation, but will never find a "proof."
-- If it finds a refutation, it will be the shortest, though not necessarily unique.
bmcRefute :: (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 -> SBool)                  -- ^ 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.
bmcRefute :: forall st res.
(Queriable IO st, res ~ QueryResult st) =>
Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcRefute = SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
forall st res.
(Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcRefuteWith SMTConfig
defaultSMTCfg

-- | Refutation using a given solver.
bmcRefuteWith :: (Queriable IO st, res ~ QueryResult st)
    => SMTConfig                            -- ^ Solver to use
    -> 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 -> SBool)                  -- ^ 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.
bmcRefuteWith :: forall st res.
(Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcRefuteWith = BMCKind
-> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
forall st res.
(Queriable IO st, res ~ QueryResult st) =>
BMCKind
-> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith BMCKind
Refute

-- | Covers using bounded model checking, using the default solver. This version tries to cover the goal
-- in a depth-first fashion. Note that this method can find a cover, but will never find determine that a goal is
-- not coverable. If it finds a cover, it will be the shortest, though not necessarily unique.
bmcCover :: (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 -> SBool)                  -- ^ 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.
bmcCover :: forall st res.
(Queriable IO st, res ~ QueryResult st) =>
Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcCover = SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
forall st res.
(Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcCoverWith SMTConfig
defaultSMTCfg

-- | Cover using a given solver.
bmcCoverWith :: (Queriable IO st, res ~ QueryResult st)
    => SMTConfig                            -- ^ Solver to use
    -> 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 -> SBool)                  -- ^ 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.
bmcCoverWith :: forall st res.
(Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcCoverWith = BMCKind
-> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
forall st res.
(Queriable IO st, res ~ QueryResult st) =>
BMCKind
-> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith BMCKind
Cover

-- | Bounded model checking, configurable with the solver. Not exported; use 'bmcCover', 'bmcRefute' and their "with" variants.
bmcWith :: (Queriable IO st, res ~ QueryResult st)
        => BMCKind -> SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> st -> SBool) -> (st -> SBool)
        -> IO (Either String (Int, [res]))
bmcWith :: forall st res.
(Queriable IO st, res ~ QueryResult st) =>
BMCKind
-> SMTConfig
-> Maybe Int
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> st -> SBool)
-> (st -> SBool)
-> IO (Either String (Int, [res]))
bmcWith BMCKind
kind SMTConfig
cfg Maybe Int
mbLimit Bool
chatty Symbolic ()
setup st -> SBool
initial st -> st -> SBool
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 (String
what, String
badResult, String
goodResult) = case BMCKind
kind of
                                           BMCKind
Cover  -> (String
"BMC Cover",  String
"Cover can't be established.", String
"Satisfying")
                                           BMCKind
Refute -> (String
"BMC Refute", String
"Cannot refute the claim.",    String
"Failing")

         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
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
badResult

         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
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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

                                  let g :: SBool
g = st -> SBool
goal st
curState
                                  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
$ case BMCKind
kind of
                                                BMCKind
Cover  ->      SBool
g   -- Covering the goal
                                                BMCKind
Refute -> SBool -> SBool
sNot SBool
g   -- Trying to refute the goal, so satisfy the negation

                                  cs <- Query CheckSatResult
checkSat

                                  case cs of
                                    DSat{} -> String -> Query (Either String (Int, [res]))
forall a. HasCallStack => String -> a
error (String -> Query (Either String (Int, [res])))
-> String -> Query (Either String (Int, [res]))
forall a b. (a -> b) -> a -> b
$ String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goodResult String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" state 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
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": 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 $ curState `trans` nextState
                                                 go (i+1) nextState (curState : sofar)