Generalize the type of bmc

LeventErkok · Nov 2, 2024 · ad41023 · ad41023
1 parent 1509066
commit ad41023
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 7 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -33,6 +33,12 @@
   * SBV now prints the elements of uninterpreted sorts more simply for z3. Previously, we simply used the
     name z3 produced, which looked like @T!val!i@ for the uninterpreted type @T@, we know convert it to @T_i@.
 
+  * [BACKWARDS COMPATIBILITY] Changed the signature of the functions bmc (and bmcWith) so they take
+    the transition as a relation, instead of a function returning multiple values. This 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'.
+
 ### Version 10.12, 2024-08-11
 
   * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.

diff --git a/Data/SBV/Tools/BMC.hs b/Data/SBV/Tools/BMC.hs
@@ -35,7 +35,7 @@ bmc :: (EqSymbolic st, Queriable IO st, res ~ QueryResult st)
     -> 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 -> 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
@@ -47,7 +47,7 @@ bmcWith :: (EqSymbolic st, Queriable IO st, res ~ QueryResult st)
         -> Bool
         -> Symbolic ()
         -> (st -> SBool)
-        -> (st -> [st])
+        -> (st -> st -> SBool)
         -> (st -> SBool)
         -> IO (Either String (Int, [res]))
 bmcWith cfg mbLimit chatty setup initial trans goal
@@ -71,5 +71,5 @@ bmcWith cfg mbLimit chatty setup initial trans goal
                                                  return $ Left $ "BMC: Solver said unknown in iteration " ++ show i
                                     Unsat  -> do pop 1
                                                  nextState <- create
-                                                 constrain $ sAny (nextState .==) (trans curState)
+                                                 constrain $ curState `trans` nextState
                                                  go (i+1) nextState (curState : sofar)
diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs
@@ -63,10 +63,10 @@ problem lim initial = bmc (Just lim) True setup initial trans goal
 
         -- Transition relation: At each step we either
         -- get to increase @x@ by 2, or decrement @y@ by 4:
-        trans :: S SInteger -> [S SInteger]
-        trans S{x, y} = [ S { x = x + 2, y = y     }
-                        , S { x = x,     y = y - 4 }
-                        ]
+        trans :: S SInteger -> S SInteger -> SBool
+        trans S{x, y} next = next `sElem` [ S { x = x + 2, y = y     }
+                                          , S { x = x,     y = y - 4 }
+                                          ]
 
         -- Goal state is when @x@ equals @y@:
         goal :: S SInteger -> SBool