Split bmc into two bmcCover and bmcRefute

This makes the intention more clear. Update the docs accordingly.

CHANGES.md

@@ -41,7 +41,8 @@
     generalizes the use cases, and it is easy to translate from existing applications. Simply change your old
     'State -> [State]' function to 'State -> State -> SBool', which can be achieved by 
     'newTrans s1 s2 = s2 `sElem` oldTrans s1', though you probably want to code this in a more readable way
-    depending on the actual transition relation you want to model.
+    depending on the actual transition relation you want to model. Furthermore, the function bmc is now
+    split into two bmcRefute and bmcCover, to indicate use cases more clearly.
 
   * [BACKWARDS COMPATIBILITY] Removed the Fresh class, which was used as a proxy for the Queriable class as
     an easier to instantiate version. The extra functionality unfortunately made writing custom Queriable

Data/SBV/Tools/BMC.hs

@@ -17,58 +17,110 @@
 {-# OPTIONS_GHC -Wall -Werror #-}
 
 module Data.SBV.Tools.BMC (
-         bmc, bmcWith
+         bmcRefute, bmcRefuteWith, bmcCover, bmcCoverWith
        ) 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 :: (Queriable IO st, res ~ QueryResult st)
+-- | 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.
-bmc = bmcWith defaultSMTCfg
+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
 
--- | Bounded model checking, configurable with the solver
+-- | 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)
-        => SMTConfig
+        => BMCKind
+        -> SMTConfig
         -> Maybe Int
         -> Bool
         -> Symbolic ()
         -> (st -> SBool)
         -> (st -> st -> SBool)
         -> (st -> SBool)
         -> IO (Either String (Int, [res]))
-bmcWith cfg mbLimit chatty setup initial trans goal
+bmcWith kind cfg mbLimit chatty setup initial trans goal
   = runSMTWith cfg $ do setup
                         query $ do state <- create
                                    constrain $ initial state
                                    go 0 state []
-   where go i _ _
+   where (what, badResult) = case kind of
+                              Cover  -> ("BMC Cover",  "Cover can't be established.")
+                              Refute -> ("BMC Refute", "Cannot refute the claim.")
+
+         go i _ _
           | Just l <- mbLimit, i >= l
-          = return $ Left $ "BMC limit of " ++ show l ++ " reached"
-         go i curState sofar = do when chatty $ io $ putStrLn $ "BMC: Iteration: " ++ show i
+          = return $ Left $ what ++ " limit of " ++ show l ++ " reached. " ++ badResult
+
+         go i curState sofar = do when chatty $ io $ putStrLn $ what ++ ": Iteration: " ++ show i
+
                                   push 1
-                                  constrain $ goal curState
+
+                                  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 "BMC: Solver returned an unexpected delta-sat result."
-                                    Sat    -> do when chatty $ io $ putStrLn $ "BMC: Solution found at iteration " ++ show i
+                                    DSat{} -> error $ what ++ ": Solver returned an unexpected delta-sat result."
+                                    Sat    -> do when chatty $ io $ putStrLn $ what ++ ": Solution found at iteration " ++ show i
                                                  ms <- mapM project (curState : sofar)
                                                  return $ Right (i, reverse ms)
-                                    Unk    -> do when chatty $ io $ putStrLn $ "BMC: Backend solver said unknown at iteration " ++ show  i
-                                                 return $ Left $ "BMC: Solver said unknown in iteration " ++ show i
+                                    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

Documentation/SBV/Examples/ProofTools/BMC.hs

@@ -58,7 +58,7 @@ instance Queriable IO (S SInteger) where
 
 -- | We parameterize over the initial state for different variations.
 problem :: Int -> (S SInteger -> SBool) -> IO (Either String (Int, [S Integer]))
-problem lim initial = bmc (Just lim) True setup initial trans goal
+problem lim initial = bmcCover (Just lim) True setup initial trans goal
   where
         -- This is where we would put solver options, typically via
         -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
@@ -82,11 +82,11 @@ problem lim initial = bmc (Just lim) True setup initial trans goal
 -- | Example 1: We start from @x=0@, @y=10@, and search up to depth @10@. We have:
 --
 -- >>> ex1
--- BMC: Iteration: 0
--- BMC: Iteration: 1
--- BMC: Iteration: 2
--- BMC: Iteration: 3
--- BMC: Solution found at iteration 3
+-- BMC Cover: Iteration: 0
+-- BMC Cover: Iteration: 1
+-- BMC Cover: Iteration: 2
+-- BMC Cover: Iteration: 3
+-- BMC Cover: Solution found at iteration 3
 -- Right (3,[(0,10),(0,6),(0,2),(2,2)])
 --
 -- As expected, there's a solution in this case. Furthermore, since the BMC engine
@@ -102,17 +102,17 @@ ex1 = problem 10 isInitial
 -- | Example 2: We start from @x=0@, @y=11@, and search up to depth @10@. We have:
 --
 -- >>> ex2
--- BMC: Iteration: 0
--- BMC: Iteration: 1
--- BMC: Iteration: 2
--- BMC: Iteration: 3
--- BMC: Iteration: 4
--- BMC: Iteration: 5
--- BMC: Iteration: 6
--- BMC: Iteration: 7
--- BMC: Iteration: 8
--- BMC: Iteration: 9
--- Left "BMC limit of 10 reached"
+-- BMC Cover: Iteration: 0
+-- BMC Cover: Iteration: 1
+-- BMC Cover: Iteration: 2
+-- BMC Cover: Iteration: 3
+-- BMC Cover: Iteration: 4
+-- BMC Cover: Iteration: 5
+-- BMC Cover: Iteration: 6
+-- BMC Cover: Iteration: 7
+-- BMC Cover: Iteration: 8
+-- BMC Cover: Iteration: 9
+-- Left "BMC Cover limit of 10 reached. Cover can't be established."
 --
 -- As expected, there's no solution in this case. While SBV (and BMC) cannot establish
 -- that there is no solution at a larger depth, you can see that this will never be the

Documentation/SBV/Examples/Puzzles/DieHard.hs

@@ -74,14 +74,14 @@ instance Queriable IO SState where
 -- | Solve the problem using a BMC search. We have:
 --
 -- >>> dieHard
--- BMC: Iteration: 0
--- BMC: Iteration: 1
--- BMC: Iteration: 2
--- BMC: Iteration: 3
--- BMC: Iteration: 4
--- BMC: Iteration: 5
--- BMC: Iteration: 6
--- BMC: Solution found at iteration 6
+-- BMC Cover: Iteration: 0
+-- BMC Cover: Iteration: 1
+-- BMC Cover: Iteration: 2
+-- BMC Cover: Iteration: 3
+-- BMC Cover: Iteration: 4
+-- BMC Cover: Iteration: 5
+-- BMC Cover: Iteration: 6
+-- BMC Cover: Solution found at iteration 6
 -- Big: 0, Small: 0 (Initial)
 -- Big: 5, Small: 0 (FillBig)
 -- Big: 2, Small: 3 (BigToSmall)
@@ -90,7 +90,7 @@ instance Queriable IO SState where
 -- Big: 5, Small: 2 (FillBig)
 -- Big: 4, Small: 3 (BigToSmall)
 dieHard :: IO ()
-dieHard = display =<< bmc Nothing True (pure ()) initial trans goal
+dieHard = display =<< bmcCover Nothing True (pure ()) initial trans goal
   where -- we start from empty jugs, and try to reach a state where big has 4 gallons
         initial State{big, small, action} = (big, small, action) .== (0, 0, sInitial)
         goal    State{big}                = big .== 4