obdd 0.2 → 0.2.3
raw patch · 13 files changed
+404/−389 lines, 13 filesdep ~basesetup-changed
Dependency ranges changed: base
Files
- OBDD.hs +0/−24
- OBDD/Data.hs +0/−197
- OBDD/Make.hs +0/−24
- OBDD/Operation.hs +0/−123
- OBDD/Property.hs +0/−12
- Setup.hs +1/−0
- Setup.lhs +0/−5
- obdd.cabal +16/−4
- src/OBDD.hs +24/−0
- src/OBDD/Data.hs +202/−0
- src/OBDD/Make.hs +24/−0
- src/OBDD/Operation.hs +125/−0
- src/OBDD/Property.hs +12/−0
− OBDD.hs
@@ -1,24 +0,0 @@--- | reduced ordered binary decision diagrams--- (c) Johannes Waldmann, 2008------ this module is intended to be imported qualified--- because it overloads some Prelude names.------ for a similar, but much more elaborate project, see--- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf>--- but I'm not sure where that source code would be available.--module OBDD --( OBDD -, module OBDD.Property-, module OBDD.Operation-, module OBDD.Make-) --where--import OBDD.Data ( OBDD )-import OBDD.Property-import OBDD.Operation-import OBDD.Make
− OBDD/Data.hs
@@ -1,197 +0,0 @@-{-# language GeneralizedNewtypeDeriving #-}---- | implementation of reduced ordered binary decision diagrams.--module OBDD.Data --(--- * the data type- OBDD -- abstract--- * for external use-, null, satisfiable-, number_of_models-, some_model, all_models--- * for internal use-, Node (..)-, make-, register-, cached, top-, access--)--where--import Data.Map ( Map )-import qualified Data.Map as M--import Data.Set ( Set )-import qualified Data.Set as S--import Control.Monad.State-import qualified System.Random--import Prelude hiding ( null )-import qualified Prelude--newtype Index = Index Int deriving ( Eq, Ord, Num, Enum, Show )---- | 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- , next :: Index- , top :: Index- , cache :: Map ( Index, Index ) Index -- ^ inputs and output for binary op- -- (unary will be simulated by binary)- }---- | Number of satisfying assignments with given set of variables.--- The set of variables must be given since the current OBDD may not contain--- all variables that were used to construct it, since some nodes may have been removed--- because they had identical children.-number_of_models :: Ord v => Set v -> OBDD v -> Integer-number_of_models vs o = - let fun o vs = do- m <- get- case access o of- Leaf c -> case c of- False -> return 0- True -> return $ 2 ^ length vs- Branch v l r -> do- let ( pre, _ : post ) = span (/= v) vs- case M.lookup ( top o ) m of- Just x -> return $ ( 2 ^ length pre ) * x- Nothing -> do- xl <- fun l post- xr <- fun r post- let xlr = xl + xr- m <- get- 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 = error "OBDD.Data.empty"- , cache = M.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---- | does the OBDD have any models?-satisfiable :: OBDD v -> Bool-satisfiable s = 0 < count s ( top s )---- | does the OBDD not have any models?-null :: OBDD v -> Bool-null s = 0 == count s ( top s )----- | randomly select one model, if possible-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- Branch v l r -> do- let nonempty_children = do- ( p, t ) <- [ (False, l), (True, r) ] - guard $ case access t of- Leaf False -> False- _ -> True- return ( p, t )- (p, t) <- select_one nonempty_children- Just m <- some_model t- return $ Just $ M.insert v p m ---- | 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- Leaf False -> [ ]- Branch v l r -> do- let nonempty_children = do- ( p, t ) <- [ (False, l), (True, r) ] - guard $ case access t of- Leaf False -> False- _ -> True- return ( p, t )- (p, t) <- nonempty_children- m <- all_models t- return $ M.insert v p m - -select_one :: [a] -> IO a-select_one xs | not ( Prelude.null xs ) = do- i <- System.Random.randomRIO ( 0, length xs - 1 )- return $ xs !! i--make :: State ( OBDD v ) Index- -> OBDD v-make action = - let ( i, s ) = runState action empty - in s { top = i }--fresh :: State ( OBDD v ) Index-fresh = do- s <- get- let i = next s- put $ s { next = succ i }- return i--cached :: Ord v- => (Index, Index) - -> ( State ( OBDD v ) Index )- -> State ( OBDD v ) Index-cached (l,r) action = do- s <- get- case M.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 }- return i--register :: Ord v- => Node v Index- -> State ( OBDD v ) Index-register n = do- s <- get- case M.lookup n ( icore s ) of- Just i -> return i- Nothing -> case n of- Branch v l r | l == r -> return l -- TRICK (?)- _ -> 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- }- return i
− OBDD/Make.hs
@@ -1,24 +0,0 @@--- | builds basic OBDDs--module OBDD.Make --( constant, unit )--where--import OBDD.Data--import Data.Map ( Map )-import qualified Data.Map as M--constant :: Ord v => Bool -> OBDD v-constant b = make $ do- register $ Leaf b---- | Variable with given parity-unit :: Ord v => v -> Bool -> OBDD v-unit v p = make $ do- l <- register $ Leaf $ not p- r <- register $ Leaf $ p- register $ Branch v l r-
− OBDD/Operation.hs
@@ -1,123 +0,0 @@-{-# language ScopedTypeVariables #-}--module OBDD.Operation --( (&&), (||), not, and, or-, unary, binary-, instantiate-, exists, exists_many-)--where--import OBDD.Data-import OBDD.Make--import Data.Map ( Map )-import qualified Data.Map as M--import Data.Set ( Set )-import qualified Data.Set as S--import Prelude hiding ( (&&), (||), and, or, not )-import qualified Prelude--( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( && ) = binary ( Prelude.&& )--( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v-( || ) = binary ( Prelude.|| )--and :: Ord v => [ OBDD v ] -> OBDD v-and = foldr ( && ) ( constant True ) --or :: Ord v => [ OBDD v ] -> OBDD v-or = foldr ( || ) ( constant False ) ----- | FIXME this is a silly implementation. Negation should be done--- by switching values in Leaves (?)-not :: Ord v => OBDD v -> OBDD v -not = unary ( Prelude.not )--unary :: Ord v - => ( Bool -> Bool )- -> OBDD v -> OBDD v-unary op x = make $ do- let handle x = cached ( top x, top x ) $ case access x of- Leaf p -> register $ Leaf $ op p- Branch v l r -> do- l' <- handle l- r' <- handle r- register $ Branch v l' r'- handle x---binary :: Ord v- => ( 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- ( Leaf p , Leaf q ) -> register $ Leaf $ op p q- ( ax, ay ) -> case comp ax ay of- LT -> do- let Branch v l r = ay- l' <- handle x l- r' <- handle x r- register $ Branch v l' r'- GT -> do- let Branch v l r = ax- l' <- handle l y- r' <- handle r y- register $ Branch v l' r'- EQ -> do- let Branch v1 l1 r1 = ax- Branch v2 l2 r2 = ay- v = if v1 == v2 then v1 else error "OBDD.Operation.handle"- l' <- handle l1 l2- r' <- handle r1 r2- register $ Branch v l' r'- handle x y---- | remove variables existentially--- TODO: needs better implementation-exists_many :: Ord v - => Set v- -> OBDD v- -> OBDD v-exists_many vars x =- foldr exists x $ S.toList vars ---- | remove variable existentially--- TODO: needs better implementation-exists :: Ord v- => v- -> OBDD v -> OBDD v-exists var x = - instantiate var False x || instantiate var True x---- | replace variable by value-instantiate :: Ord v => - v -> Bool - -> OBDD v- -> OBDD v-instantiate var val x = make $ do- 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- let t = if val then r else l- handle t- else do- l' <- handle l- r' <- handle r- register $ Branch v l' r'- handle x--comp x y = case (x , y) of- ( Leaf {} , Leaf {} ) -> EQ- ( Branch {} , Leaf {} ) -> GT- ( Leaf {} , Branch {} ) -> LT- ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2-
− OBDD/Property.hs
@@ -1,12 +0,0 @@-module OBDD.Property --( null, satisfiable-, number_of_models-, some_model, all_models-)--where--import qualified Prelude-import OBDD.Data-
+ Setup.hs view
@@ -0,0 +1,1 @@+module Main (main) where import Distribution.Simple ; main = defaultMain
− Setup.lhs
@@ -1,5 +0,0 @@-#!/usr/local/bin/runhaskell--> import Distribution.Simple-> main = defaultMain-
obdd.cabal view
@@ -1,12 +1,24 @@ Name: obdd-Version: 0.2+Version: 0.2.3+Cabal-Version: >= 1.6+Build-type: Simple Synopsis: Ordered Reduced Binary Decision Diagrams Description: Construct, combine and query OBDDs; an efficient representation for formulas in propositional logic+category: Logic License: GPL License-file: LICENSE Author: Johannes Waldmann Maintainer: Johannes Waldmann <waldmann@imn.htwk-leipzig.de>-Build-Depends: base, random, mtl, containers-Build-Type: Simple-Exposed-Modules: OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property++library+ Build-Depends: base==4.*, random, mtl, containers+ Hs-Source-Dirs: src+ Exposed-Modules: OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property+ ghc-options: -funbox-strict-fields+++Source-Repository head+ Type: git+ Location: git://dfa.imn.htwk-leipzig.de/srv/git/obdd/+
+ src/OBDD.hs view
@@ -0,0 +1,24 @@+-- | reduced ordered binary decision diagrams+-- (c) Johannes Waldmann, 2008+--+-- this module is intended to be imported qualified+-- because it overloads some Prelude names.+--+-- for a similar, but much more elaborate project, see+-- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf>+-- but I'm not sure where that source code would be available.++module OBDD ++( OBDD +, module OBDD.Property+, module OBDD.Operation+, module OBDD.Make+) ++where++import OBDD.Data ( OBDD )+import OBDD.Property+import OBDD.Operation+import OBDD.Make
+ src/OBDD/Data.hs view
@@ -0,0 +1,202 @@+{-# language GeneralizedNewtypeDeriving #-}++-- | implementation of reduced ordered binary decision diagrams.++module OBDD.Data ++(+-- * the data type+ OBDD -- abstract+, size+-- * for external use+, null, satisfiable+, number_of_models+, some_model, all_models+-- * for internal use+, Node (..)+, make+, register+, cached, top+, access++)++where++import Data.Map.Strict ( Map )+import qualified Data.Map.Strict as M++import Data.Set ( Set )+import qualified Data.Set as S++import Control.Monad.State.Strict+import qualified System.Random++import Prelude hiding ( null )+import qualified Prelude++newtype Index = Index { unIndex :: Int }+ deriving ( Eq, Ord, Num, Enum, Show )++-- | 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+ , next :: !Index+ , top :: !Index+ , cache :: ! (Map ( Index, Index ) Index) -- ^ inputs and output for binary op+ -- (unary will be simulated by binary)+ }++size = unIndex . next++-- | Number of satisfying assignments with given set of variables.+-- The set of variables must be given since the current OBDD may not contain+-- all variables that were used to construct it, since some nodes may have been removed+-- because they had identical children.+number_of_models :: Ord v => Set v -> OBDD v -> Integer+number_of_models vs o = + let fun o vs = do+ m <- get+ case access o of+ Leaf c -> case c of+ False -> return 0+ True -> return $ 2 ^ length vs+ Branch v l r -> do+ let ( pre, _ : post ) = span (/= v) vs+ case M.lookup ( top o ) m of+ Just x -> return $ ( 2 ^ length pre ) * x+ Nothing -> do+ xl <- fun l post+ xr <- fun r post+ let xlr = xl + xr+ m <- get+ 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+ }++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++-- | does the OBDD have any models?+satisfiable :: OBDD v -> Bool+satisfiable s = 0 < count s ( top s )++-- | does the OBDD not have any models?+null :: OBDD v -> Bool+null s = 0 == count s ( top s )+++-- | randomly select one model, if possible+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+ Branch v l r -> do+ let nonempty_children = do+ ( p, t ) <- [ (False, l), (True, r) ] + guard $ case access t of+ Leaf False -> False+ _ -> True+ return ( p, t )+ (p, t) <- select_one nonempty_children+ Just m <- some_model t+ return $ Just $ M.insert v p m ++-- | 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+ Leaf False -> [ ]+ Branch v l r -> do+ let nonempty_children = do+ ( p, t ) <- [ (False, l), (True, r) ] + guard $ case access t of+ Leaf False -> False+ _ -> True+ return ( p, t )+ (p, t) <- nonempty_children+ m <- all_models t+ return $ M.insert v p m + +select_one :: [a] -> IO a+select_one xs | not ( Prelude.null xs ) = do+ i <- System.Random.randomRIO ( 0, length xs - 1 )+ return $ xs !! i++make :: State ( OBDD v ) Index+ -> OBDD v+make action = + let ( i, s ) = runState action empty + in i `seq` s { top = i }++fresh :: State ( OBDD v ) Index+fresh = do+ s <- get+ let i = next s+ put $ s { next = succ i }+ return i++cached :: Ord v+ => (Index, Index) + -> ( State ( OBDD v ) Index )+ -> State ( OBDD v ) Index+cached (l,r) action = do+ s <- get+ case M.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 }+ return i++register :: Ord v+ => Node v Index+ -> State ( OBDD v ) Index+register n = do+ s <- get+ case M.lookup n ( icore s ) of+ Just i -> return i+ Nothing -> case n of+ Branch v l r | l == r -> return l -- TRICK (?)+ _ -> 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+ }+ return i
+ src/OBDD/Make.hs view
@@ -0,0 +1,24 @@+-- | builds basic OBDDs++module OBDD.Make ++( constant, unit )++where++import OBDD.Data++import Data.Map ( Map )+import qualified Data.Map as M++constant :: Ord v => Bool -> OBDD v+constant b = make $ do+ register $ Leaf b++-- | Variable with given parity+unit :: Ord v => v -> Bool -> OBDD v+unit v p = make $ do+ l <- register $ Leaf $ not p+ r <- register $ Leaf $ p+ register $ Branch v l r+
+ src/OBDD/Operation.hs view
@@ -0,0 +1,125 @@+{-# language ScopedTypeVariables #-}++module OBDD.Operation ++( (&&), (||), not, and, or+, unary, binary+, instantiate+, exists, exists_many+)++where++import OBDD.Data+import OBDD.Make++import Data.Map ( Map )+import qualified Data.Map as M++import Data.Set ( Set )+import qualified Data.Set as S++import Data.List ( foldl' )++import Prelude hiding ( (&&), (||), and, or, not )+import qualified Prelude++( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v+( && ) = binary ( Prelude.&& )++( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v+( || ) = binary ( Prelude.|| )++and :: Ord v => [ OBDD v ] -> OBDD v+and = foldl' ( && ) ( constant True ) ++or :: Ord v => [ OBDD v ] -> OBDD v+or = foldl' ( || ) ( constant False ) +++-- | FIXME this is a silly implementation. Negation should be done+-- by switching values in Leaves (?)+not :: Ord v => OBDD v -> OBDD v +not = unary ( Prelude.not )++unary :: Ord v + => ( Bool -> Bool )+ -> OBDD v -> OBDD v+unary op x = make $ do+ let handle x = cached ( top x, top x ) $ case access x of+ Leaf p -> register $ Leaf $ op p+ Branch v l r -> do+ l' <- handle l+ r' <- handle r+ register $ Branch v l' r'+ handle x+++binary :: Ord v+ => ( 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+ ( Leaf p , Leaf q ) -> register $ Leaf $ op p q+ ( ax, ay ) -> case comp ax ay of+ LT -> do+ let Branch v l r = ay+ l' <- handle x l+ r' <- handle x r+ register $ Branch v l' r'+ GT -> do+ let Branch v l r = ax+ l' <- handle l y+ r' <- handle r y+ register $ Branch v l' r'+ EQ -> do+ let Branch v1 l1 r1 = ax+ Branch v2 l2 r2 = ay+ v = if v1 == v2 then v1 else error "OBDD.Operation.handle"+ l' <- handle l1 l2+ r' <- handle r1 r2+ register $ Branch v l' r'+ handle x y++-- | remove variables existentially+-- TODO: needs better implementation+exists_many :: Ord v + => Set v+ -> OBDD v+ -> OBDD v+exists_many vars x =+ foldr exists x $ S.toList vars ++-- | remove variable existentially+-- TODO: needs better implementation+exists :: Ord v+ => v+ -> OBDD v -> OBDD v+exists var x = + instantiate var False x || instantiate var True x++-- | replace variable by value+instantiate :: Ord v => + v -> Bool + -> OBDD v+ -> OBDD v+instantiate var val x = make $ do+ 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+ let t = if val then r else l+ handle t+ else do+ l' <- handle l+ r' <- handle r+ register $ Branch v l' r'+ handle x++comp x y = case (x , y) of+ ( Leaf {} , Leaf {} ) -> EQ+ ( Branch {} , Leaf {} ) -> GT+ ( Leaf {} , Branch {} ) -> LT+ ( Branch v1 _ _ , Branch v2 _ _ ) -> compare v1 v2+
+ src/OBDD/Property.hs view
@@ -0,0 +1,12 @@+module OBDD.Property ++( null, satisfiable+, number_of_models+, some_model, all_models+)++where++import qualified Prelude+import OBDD.Data+