OBDD.Data

implementation of reduced ordered binary decision diagrams.

the data type

data OBDD v

assumes total ordering on variables

size :: OBDD v -> Int

for external use

null :: OBDD v -> Bool

does the OBDD not have any models?

satisfiable :: OBDD v -> Bool

does the OBDD have any models?

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

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))

randomly select one model, if possible

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

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

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

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

for internal use

data Node v i

Constructors

Leaf !Bool

Branch !v !i !i

Instances

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

Methods

(==) :: Node v i -> Node v i -> Bool

(/=) :: Node v i -> Node v i -> Bool

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

Methods

compare :: Node v i -> Node v i -> Ordering

(<) :: Node v i -> Node v i -> Bool

(<=) :: Node v i -> Node v i -> Bool

(>) :: Node v i -> Node v i -> Bool

(>=) :: Node v i -> Node v i -> Bool

max :: Node v i -> Node v i -> Node v i

min :: Node v i -> Node v i -> 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)