obdd-0.3.1: Ordered Reduced Binary Decision Diagrams

Safe HaskellNone




implementation of reduced ordered binary decision diagrams.


the data type

data OBDD v Source

assumes total ordering on variables

size :: OBDD v -> IndexSource

for external use

null :: OBDD v -> BoolSource

does the OBDD not have any models?

satisfiable :: OBDD v -> BoolSource

does the OBDD have any models?

number_of_models :: Ord v => Set v -> OBDD v -> IntegerSource

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.

some_model :: Ord v => OBDD v -> IO (Maybe (Map v Bool))Source

randomly select one model, if possible

all_models :: Ord v => OBDD v -> [Map v Bool]Source

list of all models (WARNING not using variables that had been deleted)

fold :: Ord v => (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> aSource

foldM :: (Monad m, Ord v) => (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m aSource

toDot :: Show v => OBDD v -> StringSource

toDot outputs a string in format suitable for input to the dot program from the graphviz suite.

for internal use

data Node v i Source


Leaf !Bool 
Branch !v !i !i 


(Eq v, Eq i) => Eq (Node v i) 
(Ord v, Ord i) => Ord (Node v i) 

make :: State (OBDD v) Index -> OBDD vSource

register :: Ord v => Node v Index -> State (OBDD v) IndexSource

checked_register :: Ord v => Node v Index -> State (OBDD v) IndexSource

cached :: Ord v => (Index, Index) -> State (OBDD v) Index -> State (OBDD v) IndexSource

top :: OBDD v -> IndexSource

access :: OBDD v -> Node v (OBDD v)Source