Safe Haskell | None |
---|---|
Language | Haskell98 |
implementation of reduced ordered binary decision diagrams.
- data OBDD v
- size :: OBDD v -> Index
- null :: OBDD v -> Bool
- satisfiable :: OBDD v -> Bool
- number_of_models :: Ord v => Set v -> OBDD v -> Integer
- some_model :: Ord v => OBDD v -> IO (Maybe (Map v Bool))
- all_models :: Ord v => OBDD v -> [Map v Bool]
- fold :: Ord v => (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a
- foldM :: (Monad m, Ord v) => (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
- toDot :: Show v => OBDD v -> String
- data Node v i
- make :: State (OBDD v) Index -> OBDD v
- register :: Ord v => Node v Index -> State (OBDD v) Index
- checked_register :: Ord v => Node v Index -> State (OBDD v) Index
- cached :: Ord v => (Index, Index) -> State (OBDD v) Index -> State (OBDD v) Index
- top :: OBDD v -> Index
- access :: OBDD v -> Node v (OBDD v)
the data type
for external use
satisfiable :: OBDD v -> Bool Source
does the OBDD have any models?
number_of_models :: Ord v => Set v -> OBDD v -> Integer Source
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)
toDot :: Show v => OBDD v -> String Source
toDot outputs a string in format suitable for input to the "dot" program from the graphviz suite.