content: -----------------------------------------------------------------------------
  -- |
  -- 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 = bmcRefuteWith 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 = bmcWith 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 = bmcCoverWith 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 = bmcWith 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 kind cfg mbLimit chatty setup initial trans goal
    = runSMTWith cfg $ do setup
                          query $ do state <- create
                                     constrain $ initial state
                                     go 0 state []
     where (what, badResult, goodResult) = case kind of
                                             Cover  -> ("BMC Cover",  "Cover can't be established.", "Satisfying")
                                             Refute -> ("BMC Refute", "Cannot refute the claim.",    "Failing")
  
           go i _ _
            | Just l <- mbLimit, i >= l
            = return $ Left $ what ++ " limit of " ++ show l ++ " reached. " ++ badResult
  
           go i curState sofar = do when chatty $ io $ putStrLn $ what ++ ": Iteration: " ++ show i
  
                                    push 1
  
                                    let g = goal curState
                                    constrain $ case kind of
                                                  Cover  ->      g   -- Covering the goal
                                                  Refute -> sNot g   -- Trying to refute the goal, so satisfy the negation
  
                                    cs <- checkSat
  
                                    case cs of
                                      DSat{} -> error $ what ++ ": Solver returned an unexpected delta-sat result."
                                      Sat    -> do when chatty $ io $ putStrLn $ what ++ ": " ++ goodResult ++ " state found at iteration " ++ show i
                                                   ms <- mapM project (curState : sofar)
                                                   return $ Right (i, reverse ms)
                                      Unk    -> do when chatty $ io $ putStrLn $ what ++ ": Backend solver said unknown at iteration " ++ show  i
                                                   return $ Left $ what ++ ": Solver said unknown in iteration " ++ show i
                                      Unsat  -> do pop 1
                                                   nextState <- create
                                                   constrain $ curState `trans` nextState
                                                   go (i+1) nextState (curState : sofar)
  