OBDD

Reduced ordered binary decision diagrams, pure Haskell implementation. (c) Johannes Waldmann, 2008 - 2016

This module is intended to be imported qualified because it overloads some Prelude names.

Documentation

data OBDD v

assumes total ordering on variables

Instances

Ord v => Eq (OBDD v)

Defined in OBDD

Methods

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

(/=) :: OBDD v -> OBDD v -> Bool

Ord v => Boolean (OBDD v)

Defined in OBDD.Operation

Methods

bool :: Bool -> OBDD v

true :: OBDD v

false :: OBDD v

(&&) :: OBDD v -> OBDD v -> OBDD v

(||) :: OBDD v -> OBDD v -> OBDD v

(==>) :: OBDD v -> OBDD v -> OBDD v

not :: OBDD v -> OBDD v

and :: Foldable t => t (OBDD v) -> OBDD v

or :: Foldable t => t (OBDD v) -> OBDD v

nand :: Foldable t => t (OBDD v) -> OBDD v

nor :: Foldable t => t (OBDD v) -> OBDD v

all :: Foldable t => (a -> OBDD v) -> t a -> OBDD v

any :: Foldable t => (a -> OBDD v) -> t a -> OBDD v

xor :: OBDD v -> OBDD v -> OBDD v

choose :: OBDD v -> OBDD v -> OBDD v -> OBDD v

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

size :: OBDD v -> Index

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.

satisfiable :: OBDD v -> Bool

does the OBDD have any models?

null :: OBDD v -> Bool

does the OBDD not have any models?

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

randomly select one model, if possible

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

all variables that occur in the nodes

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

list of all paths

models :: Ord k => Set k -> OBDD k -> [Map k Bool]

list of all models (a.k.a. minterms)

module OBDD.Property

module OBDD.Operation

module OBDD.Display

module OBDD.Make

Orphan instances

Ord v => Eq (OBDD v)

Methods

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

(/=) :: OBDD v -> OBDD v -> Bool