OBDD.Operation

Documentation

(&&) :: Ord v => OBDD v -> OBDD v -> OBDD v infixr 3

(||) :: Ord v => OBDD v -> OBDD v -> OBDD v infixr 2

not :: Ord v => OBDD v -> OBDD v

FIXME this is a silly implementation. Negation should be done by switching values in Leaves (?)

and :: Ord v => [OBDD v] -> OBDD v

or :: Ord v => [OBDD v] -> OBDD v

ite :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v

bool :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v

implies :: Ord v => OBDD v -> OBDD v -> OBDD v

equiv :: Ord v => OBDD v -> OBDD v -> OBDD v

xor :: Ord v => OBDD v -> OBDD v -> OBDD v

unary :: Ord v => (Bool -> Bool) -> OBDD v -> OBDD v

binary :: Ord v => (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v

instantiate :: Ord v => v -> Bool -> OBDD v -> OBDD v

replace variable by value

exists :: Ord v => v -> OBDD v -> OBDD v

remove variable existentially TODO: needs better implementation

exists_many :: Ord v => Set v -> OBDD v -> OBDD v

remove variables existentially TODO: needs better implementation

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

Apply function in each node, bottom-up. return the value in the root node. Will cache intermediate results. You might think that count_models = fold (b -> if b then 1 else 0) (v l r -> l + r) but that's not true because a path might omit variables. Use full_fold to fold over interpolated nodes as well.

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

Run action in each node, bottum-up. return the value in the root node. Will cache intermediate results.

full_fold :: Ord v => Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a

Apply function in each node, bottom-up. Also apply to interpolated nodes: when a link from a node to a child skips some variables: for each skipped variable, we run the branch function on an interpolated node that contains this missing variable, and identical children. With this function, number_of_models can be implemented as full_fold vars (bool 0 1) ( const (+) ). And it actually is, see the source.

full_foldM :: (Monad m, Ord v) => Set v -> (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a