-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Ordered Reduced Binary Decision Diagrams
--   
--   Construct, combine and query OBDDs; an efficient representation for
--   formulas in propositional logic
@package obdd
@version 0.3.1


-- | implementation of reduced ordered binary decision diagrams.
module OBDD.Data

-- | assumes total ordering on variables
data OBDD v
size :: OBDD v -> Index

-- | does the OBDD not have any models?
null :: OBDD v -> Bool

-- | does the OBDD have any models?
satisfiable :: OBDD v -> Bool

-- | 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.
number_of_models :: Ord v => Set v -> OBDD v -> Integer

-- | randomly select one model, if possible
some_model :: Ord v => OBDD v -> IO (Maybe (Map v Bool))

-- | list of all models (WARNING not using variables that had been deleted)
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 outputs a string in format suitable for input to the <a>dot</a>
--   program from the graphviz suite.
toDot :: Show v => OBDD v -> String
data Node v i
Leaf :: !Bool -> Node v i
Branch :: !v -> !i -> !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)
instance (Eq v, Eq i) => Eq (Node v i)
instance (Ord v, Ord i) => Ord (Node v i)


-- | builds basic OBDDs
module OBDD.Make
constant :: Ord v => Bool -> OBDD v

-- | Variable with given parity
unit :: Ord v => v -> Bool -> OBDD v

module OBDD.Operation
(&&) :: Ord v => OBDD v -> OBDD v -> OBDD v
(||) :: Ord v => OBDD v -> OBDD v -> OBDD v

-- | FIXME this is a silly implementation. Negation should be done by
--   switching values in Leaves (?)
not :: Ord v => OBDD v -> OBDD v
and :: Ord v => [OBDD v] -> OBDD v
or :: Ord 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

-- | replace variable by value
instantiate :: Ord v => v -> Bool -> OBDD v -> OBDD v

-- | remove variable existentially TODO: needs better implementation
exists :: Ord v => v -> OBDD v -> OBDD v

-- | remove variables existentially TODO: needs better implementation
exists_many :: Ord v => Set v -> OBDD v -> OBDD v
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

module OBDD.Property

-- | does the OBDD not have any models?
null :: OBDD v -> Bool

-- | does the OBDD have any models?
satisfiable :: OBDD v -> Bool

-- | 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.
number_of_models :: Ord v => Set v -> OBDD v -> Integer

-- | randomly select one model, if possible
some_model :: Ord v => OBDD v -> IO (Maybe (Map v Bool))

-- | list of all models (WARNING not using variables that had been deleted)
all_models :: Ord v => OBDD v -> [Map v Bool]
size :: OBDD v -> Index


-- | reduced ordered binary decision diagrams (c) Johannes Waldmann, 2008
--   
--   this module is intended to be imported qualified because it overloads
--   some Prelude names.
--   
--   for a similar, but much more elaborate project, see
--   <a>http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf</a>
--   but I'm not sure where that source code would be available.
module OBDD

-- | assumes total ordering on variables
data OBDD v