better wording

LeventErkok · Nov 5, 2024 · 3d9b021 · 3d9b021
1 parent a5806c0
commit 3d9b021
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/Data/SBV/Tools/BMC.hs b/Data/SBV/Tools/BMC.hs
@@ -95,9 +95,9 @@ bmcWith kind cfg mbLimit chatty setup initial trans goal
                         query $ do state <- create
                                    constrain $ initial state
                                    go 0 state []
-   where (what, badResult) = case kind of
-                              Cover  -> ("BMC Cover",  "Cover can't be established.")
-                              Refute -> ("BMC Refute", "Cannot refute the claim.")
+   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
@@ -116,7 +116,7 @@ bmcWith kind cfg mbLimit chatty setup initial trans goal
 
                                   case cs of
                                     DSat{} -> error $ what ++ ": Solver returned an unexpected delta-sat result."
-                                    Sat    -> do when chatty $ io $ putStrLn $ what ++ ": Solution found at iteration " ++ show i
+                                    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

diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs
@@ -84,7 +84,7 @@ problem lim initial = bmcCover (Just lim) True setup initial trans goal
 -- BMC Cover: Iteration: 1
 -- BMC Cover: Iteration: 2
 -- BMC Cover: Iteration: 3
--- BMC Cover: Solution found at iteration 3
+-- BMC Cover: Satisfying state 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

diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs
@@ -80,7 +80,7 @@ instance Queriable IO SState where
 -- BMC Cover: Iteration: 4
 -- BMC Cover: Iteration: 5
 -- BMC Cover: Iteration: 6
--- BMC Cover: Solution found at iteration 6
+-- BMC Cover: Satisfying state found at iteration 6
 -- Big: 0, Small: 0 (Initial)
 -- Big: 5, Small: 0 (FillBig)
 -- Big: 2, Small: 3 (BigToSmall)