obdd 0.2.7 → 0.3.1

raw patch · 3 files changed

+79/−14 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• obdd.cabal +1/−1
• src/OBDD/Data.hs +76/−12
• src/OBDD/Operation.hs +2/−1

@@ -1,5 +1,5 @@ Name:                obdd-Version:             0.2.7+Version:             0.3.1 Cabal-Version:       >= 1.6 Build-type: Simple Synopsis:            Ordered Reduced Binary Decision Diagrams

@@ -14,10 +14,11 @@ , number_of_models , some_model, all_models , fold, foldM+, toDot -- * for internal use , Node (..) , make-, register+, register, checked_register , cached, top , access @@ -42,8 +43,9 @@ import Data.Set ( Set ) import qualified Data.Set as S -import Control.Monad.State.Strict -   (State, runState, evalState, get, put)+import Control.Arrow ( (&&&) )+import Control.Monad.State.Strict+   (State, runState, evalState, get, put, gets, modify) import qualified System.Random import Control.Monad.Fix import Control.Monad ( forM, guard )@@ -77,16 +79,18 @@      -> ( v -> a -> a -> a )      -> OBDD v -> a fold leaf branch o =-    let a = A.array (0,top o) $ do-            i <- A.indices a-            return (i, case IM.lookup i $ core o of-                Nothing -> undefined-                Just n  -> case n of-                    Leaf c -> leaf c+    let f = leaf False ; t = leaf True+        m0 = M.fromList +           [(icore_false,f), (icore_true,t)]+        m = foldl ( \ m (i,n) -> +            let val = case n of                     Branch v l r -> -                        branch v (a A.! l) (a A.! r) )-    in  a A.! top o+                        branch v (m M.! l) (m M.! r) +            in M.insert i val m+          ) m0 $ IM.toAscList $ core o+    in  m M.! top o + foldM :: (Monad m, Ord v)      => ( Bool -> m a )      -> ( v -> a -> a -> m a )@@ -256,4 +260,64 @@ 		    , icore = VIIM.insert (v, l, r) i                              $ icore s 		    }-	        return i  +	        return i++checked_register :: Ord v+	 => Node v Index+       -> State ( OBDD v ) Index+checked_register n = case n of+    Branch v l r -> do+      s <- get +      let check_var_ordering b = case IM.lookup b (core s ) of +                  Just (Branch av _ _) | not (v > av) -> +                      error "wrong variable ordering"+                  _ -> return ()+      check_var_ordering l ; check_var_ordering r+      register n+    _ -> register n+++-- | toDot outputs a string in format suitable for input to the "dot" program+-- from the graphviz suite.+toDot :: (Show v) => OBDD v -> String+toDot (OBDD idmap _ _ top _) =+    unlines [ "digraph BDD {"+            -- Start in oval mode+            , "node[shape=oval];"+            , evalState (helper $ idToNode top) S.empty+            , "}"+            ]+  where+    idToNode =+        let getNode = \i -> case i of+                          0 -> Leaf False+                          1 -> Leaf True+                          _ -> idmap IM.! i+        in id &&& getNode++    mkLabel lbl = "[label=\"" ++ lbl ++ "\"];"++    helper (thisId, Leaf b) = return $+        -- switch to rectangle nodes for the leaf, before going back to ovals.+        unlines [ "node[shape=rectangle];"+                , show thisId ++ mkLabel (show b)+                , "node[shape=oval];"+                ]+    helper (thisId, Branch vid l r) = do+        -- Ensure we don't traverse children multiple times, if we have more+        -- than one edge into a given node.+        beenHere <- gets (thisId `S.member`)+        if beenHere+            then return ""+            else do+                lstr <- helper $ idToNode l+                rstr <- helper $ idToNode r+                modify (thisId `S.insert`)+                let idStr = show thisId+                return $ unlines+                   [ idStr ++ mkLabel (show vid)+                   , lstr+                   , idStr ++ "->" ++ show l ++ mkLabel "0"+                   , rstr+                   , idStr ++ "->" ++ show r ++ mkLabel "1"+                   ]

@@ -79,7 +79,8 @@       => ( Bool -> Bool -> Bool )       -> OBDD v -> OBDD v -> OBDD v binary op x y = make $ do-    let handle x y = cached (top x, top y) $ case ( access x , access y ) of+    let -- register = checked_register -- for testing+        handle x y = cached (top x, top y) $ case ( access x , access y ) of 	            ( Leaf p , Leaf q ) -> register $ Leaf $ op p q 		    ( ax, ay ) -> case comp ax ay of 		        LT -> do