obdd 0.2.5 → 0.2.7
raw patch · 3 files changed
+68/−12 lines, 3 filesdep +arraydep ~containers
Dependencies added: array
Dependency ranges changed: containers
Files
- obdd.cabal +4/−3
- src/OBDD/Data.hs +42/−1
- src/OBDD/Operation.hs +22/−8
obdd.cabal view
@@ -1,5 +1,5 @@ Name: obdd-Version: 0.2.5+Version: 0.2.7 Cabal-Version: >= 1.6 Build-type: Simple Synopsis: Ordered Reduced Binary Decision Diagrams@@ -12,7 +12,7 @@ Maintainer: Johannes Waldmann <waldmann@imn.htwk-leipzig.de> library- Build-Depends: base==4.*, random, mtl, containers+ Build-Depends: base==4.*, random, mtl, containers>=0.5, array Hs-Source-Dirs: src Exposed-Modules: OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property Other-Modules: OBDD.IntIntMap, OBDD.VarIntIntMap@@ -21,5 +21,6 @@ Source-Repository head Type: git- Location: git://dfa.imn.htwk-leipzig.de/srv/git/obdd/+ Location: git://github.com/jwaldmann/haskell-obdd.git+
src/OBDD/Data.hs view
@@ -1,4 +1,5 @@ {-# language GeneralizedNewtypeDeriving #-}+{-# language RecursiveDo #-} -- | implementation of reduced ordered binary decision diagrams. @@ -12,6 +13,7 @@ , null, satisfiable , number_of_models , some_model, all_models+, fold, foldM -- * for internal use , Node (..) , make@@ -35,12 +37,19 @@ import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as M +import qualified Data.Array as A+ import Data.Set ( Set ) import qualified Data.Set as S -import Control.Monad.State.Strict+import Control.Monad.State.Strict + (State, runState, evalState, get, put) import qualified System.Random+import Control.Monad.Fix+import Control.Monad ( forM, guard )+import qualified Control.Monad ( foldM ) + import Prelude hiding ( null ) import qualified Prelude @@ -62,6 +71,38 @@ -- ^ inputs and output for binary op -- (unary will be simulated by binary) }++fold :: Ord v + => ( Bool -> a )+ -> ( 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+ Branch v l r -> + branch v (a A.! l) (a A.! r) )+ in a A.! top o++foldM :: (Monad m, Ord v)+ => ( Bool -> m a )+ -> ( v -> a -> a -> m a )+ -> OBDD v -> m a+foldM leaf branch o = do+ f <- leaf False ; t <- leaf True+ let m0 = M.fromList + [(icore_false,f), (icore_true,t)]+ m <- Control.Monad.foldM ( \ m (i,n) -> do+ val <- case n of+ Branch v l r -> + branch v (m M.! l) (m M.! r) + return $ M.insert i val m+ ) m0 $ IM.toAscList $ core o+ return $ m M.! top o+ icore_false = 0 :: Index icore_true = 1 :: Index
src/OBDD/Operation.hs view
@@ -6,6 +6,7 @@ , unary, binary , instantiate , exists, exists_many+, fold, foldM ) where@@ -13,8 +14,8 @@ import OBDD.Data import OBDD.Make -import Data.Map ( Map )-import qualified Data.Map as M+import qualified Data.List ( sortBy)+import Data.Function (on) import Data.Set ( Set ) import qualified Data.Set as S@@ -34,14 +35,28 @@ and :: Ord v => [ OBDD v ] -> OBDD v-and = foldr ( && ) ( constant True ) +and = fold_by_size (constant True) (&&)+-- and = foldr ( && ) ( constant True ) -- writing foldl or fold' here -- makes performance MUCH worse! or :: Ord v => [ OBDD v ] -> OBDD v-or = foldr ( || ) ( constant False ) +or = fold_by_size (constant False) (||)+-- or = foldr ( || ) ( constant False ) +fold_by_size base reduce fs =+ let handle fs = case fs of+ [] -> base+ [f1 ] -> f1+ f1 : f2 : rest -> + let f = reduce f1 f2+ in handle $ insert f rest+ insert f gs = case gs of+ g : hs | size f > size g -> g : insert f hs+ _ -> f : gs+ in handle $ Data.List.sortBy (compare `on` size) fs + -- | FIXME this is a silly implementation. Negation should be done -- by switching values in Leaves (?) not :: Ord v => OBDD v -> OBDD v @@ -112,14 +127,13 @@ let handle x = cached ( top x, top x ) $ case access x of Leaf p -> register $ Leaf p Branch v l r -> - if v == var- then do+ if v == var then do let t = if val then r else l handle t- else do+ else do l' <- handle l r' <- handle r- register $ Branch v l' r'+ register $ Branch v l' r' handle x comp x y = case (x , y) of