obdd 0.2.3 → 0.2.5
raw patch · 7 files changed
+131/−53 lines, 7 filessetup-changed
Files
- Setup.hs +2/−1
- obdd.cabal +2/−1
- src/OBDD/Data.hs +64/−48
- src/OBDD/IntIntMap.hs +31/−0
- src/OBDD/Operation.hs +8/−3
- src/OBDD/Property.hs +1/−0
- src/OBDD/VarIntIntMap.hs +23/−0
Setup.hs view
@@ -1,1 +1,2 @@-module Main (main) where import Distribution.Simple ; main = defaultMain+import Distribution.Simple+main = defaultMain
obdd.cabal view
@@ -1,5 +1,5 @@ Name: obdd-Version: 0.2.3+Version: 0.2.5 Cabal-Version: >= 1.6 Build-type: Simple Synopsis: Ordered Reduced Binary Decision Diagrams@@ -15,6 +15,7 @@ Build-Depends: base==4.*, random, mtl, containers Hs-Source-Dirs: src Exposed-Modules: OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property+ Other-Modules: OBDD.IntIntMap, OBDD.VarIntIntMap ghc-options: -funbox-strict-fields
src/OBDD/Data.hs view
@@ -23,6 +23,15 @@ where +import Data.IntMap.Strict ( IntMap )+import qualified Data.IntMap.Strict as IM++import OBDD.IntIntMap (IntIntMap)+import qualified OBDD.IntIntMap as IIM++import OBDD.VarIntIntMap (VarIntIntMap)+import qualified OBDD.VarIntIntMap as VIIM+ import Data.Map.Strict ( Map ) import qualified Data.Map.Strict as M @@ -35,20 +44,28 @@ import Prelude hiding ( null ) import qualified Prelude -newtype Index = Index { unIndex :: Int }- deriving ( Eq, Ord, Num, Enum, Show )+-- newtype Index = Index { unIndex :: Int }+-- deriving ( Eq, Ord, Num, Enum, Show ) +type Index = Int ; unIndex = id+ -- | assumes total ordering on variables data OBDD v = OBDD- { core :: !(Map Index ( Node v Index ))- , icore :: !(Map ( Node v Index ) Index)- , counter :: Map Index Integer -- ^ number of assignments+ { core :: !(IntMap ( Node v Index ))+ + -- , icore :: !(Map ( Node v Index ) Index)+ , icore :: !(VarIntIntMap v Index) , next :: !Index , top :: !Index- , cache :: ! (Map ( Index, Index ) Index) -- ^ inputs and output for binary op- -- (unary will be simulated by binary)+ + , cache :: !(IntIntMap Index) + -- ^ inputs and output for binary op+ -- (unary will be simulated by binary) } +icore_false = 0 :: Index +icore_true = 1 :: Index + size = unIndex . next -- | Number of satisfying assignments with given set of variables.@@ -72,51 +89,50 @@ xr <- fun r post let xlr = xl + xr m <- get- put $ M.insert ( top o ) xlr m+ put $! M.insert ( top o ) xlr m return $ ( 2 ^ length pre ) * xlr in evalState ( fun o $ reverse $ S.toAscList vs ) M.empty empty :: OBDD v empty = OBDD - { core = M.empty- , icore = M.empty- , counter = M.empty- , next = 0- , top = -42 -- error "OBDD.Data.empty"- , cache = M.empty+ { core = IM.empty+ , icore = VIIM.empty+ , next = 2+ , top = 0+ , cache = IIM.empty } data Node v i = Leaf !Bool | Branch !v !i !i deriving ( Eq, Ord ) -{-! for Node derive: ToDoc !-}- access :: OBDD v -> Node v ( OBDD v )-access s = case M.lookup ( top s ) ( core s ) of- Nothing -> error "OBDD.Data.access"- Just n -> case n of- Leaf p -> Leaf p- Branch v l r -> - Branch v ( s { top = l } ) ( s { top = r } )--count :: OBDD v -> Index -> Integer-count s i = case M.lookup i ( counter s ) of- Nothing -> error "OBDD.Data.count"- Just n -> n+access s = case top s of+ 0 -> Leaf False+ 1 -> Leaf True+ t -> case IM.lookup ( top s ) ( core s ) of+ Nothing -> error "OBDD.Data.access"+ Just n -> case n of+ Leaf p -> error "Leaf in core"+ Branch v l r -> + Branch v ( s { top = l } ) + ( s { top = r } ) -- | does the OBDD have any models? satisfiable :: OBDD v -> Bool-satisfiable s = 0 < count s ( top s )+satisfiable = not . null -- | does the OBDD not have any models? null :: OBDD v -> Bool-null s = 0 == count s ( top s )-+null s = case access s of+ Leaf False -> True + _ -> False -- | randomly select one model, if possible-some_model :: Ord v => OBDD v -> IO ( Maybe ( Map v Bool ) )+some_model :: Ord v + => OBDD v + -> IO ( Maybe ( Map v Bool ) ) some_model s = case access s of Leaf True -> return $ Just $ M.empty Leaf False -> return Nothing@@ -131,7 +147,8 @@ Just m <- some_model t return $ Just $ M.insert v p m --- | list of all models (WARNING not using variables that had been deleted)+-- | list of all models (WARNING not using +-- variables that had been deleted) all_models :: Ord v => OBDD v -> [ Map v Bool ] all_models s = case access s of Leaf True -> return M.empty@@ -162,7 +179,7 @@ fresh = do s <- get let i = next s- put $ s { next = succ i }+ put $! s { next = succ i } return i cached :: Ord v@@ -171,32 +188,31 @@ -> State ( OBDD v ) Index cached (l,r) action = do s <- get- case M.lookup (l,r) $ cache s of+ case IIM.lookup (l, r) $ cache s of Just i -> return i Nothing -> do i <- action s <- get- put $ s { cache = M.insert ( l,r) i $ cache s }+ put $! s { cache = IIM.insert (l, r) i + $ cache s } return i register :: Ord v => Node v Index -> State ( OBDD v ) Index-register n = do- s <- get- case M.lookup n ( icore s ) of+register n = case n of+ Leaf False -> return 0+ Leaf True -> return 1+ Branch v l r -> if l == r then return l else do+ s <- get + case VIIM.lookup (v, l, r) ( icore s ) of Just i -> return i- Nothing -> case n of- Branch v l r | l == r -> return l -- TRICK (?)- _ -> do+ Nothing -> do i <- fresh s <- get- let c = case n of- Leaf p -> if p then 1 else 0- Branch v l r -> count s l + count s r - put $ s - { core = M.insert i n $ core s- , icore = M.insert n i $ icore s- , counter = M.insert i c $ counter s+ put $! s + { core = IM.insert i n $ core s+ , icore = VIIM.insert (v, l, r) i + $ icore s } return i
+ src/OBDD/IntIntMap.hs view
@@ -0,0 +1,31 @@+module OBDD.IntIntMap + +( IntIntMap () +, empty, lookup, insert, singleton+) + +where++import Prelude hiding ( lookup ) + +import Data.IntMap (IntMap)+import qualified Data.IntMap.Strict as M++newtype IntIntMap v = IntIntMap (IntMap (IntMap v))++empty = IntIntMap M.empty++singleton (i, j) v = + IntIntMap $ M.singleton i (M.singleton j v) ++lookup (i, j) (IntIntMap mm) = do+ m <- M.lookup i mm+ M.lookup j m++insert (i, j) v (IntIntMap mm) = + case M.lookup i mm of+ Nothing -> IntIntMap + $ M.insert i (M.singleton j v) mm + Just m -> IntIntMap + $ M.insert i (M.insert j v m) mm +
src/OBDD/Operation.hs view
@@ -19,7 +19,8 @@ import Data.Set ( Set ) import qualified Data.Set as S -import Data.List ( foldl' )+-- import Data.List ( foldl' )+-- don't use, see below import Prelude hiding ( (&&), (||), and, or, not ) import qualified Prelude@@ -30,11 +31,15 @@ ( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v ( || ) = binary ( Prelude.|| ) ++ and :: Ord v => [ OBDD v ] -> OBDD v-and = foldl' ( && ) ( constant True ) +and = foldr ( && ) ( constant True ) +-- writing foldl or fold' here +-- makes performance MUCH worse! or :: Ord v => [ OBDD v ] -> OBDD v-or = foldl' ( || ) ( constant False ) +or = foldr ( || ) ( constant False ) -- | FIXME this is a silly implementation. Negation should be done
src/OBDD/Property.hs view
@@ -3,6 +3,7 @@ ( null, satisfiable , number_of_models , some_model, all_models+, size ) where
+ src/OBDD/VarIntIntMap.hs view
@@ -0,0 +1,23 @@+module OBDD.VarIntIntMap where++import qualified OBDD.IntIntMap as I+import qualified Data.Map.Strict as M+import Prelude hiding ( lookup ) + ++newtype VarIntIntMap k v = + VarIntIntMap ( M.Map k ( I.IntIntMap v ))+ +empty = VarIntIntMap M.empty++lookup (k, i, j) (VarIntIntMap mm) = do+ m <- M.lookup k mm+ I.lookup (i, j) m++insert (k, i, j) v (VarIntIntMap mm) = + case M.lookup k mm of+ Nothing -> VarIntIntMap + $ M.insert k (I.singleton (i, j) v) mm+ Just m -> VarIntIntMap + $ M.insert k (I.insert (i, j) v m) mm+