-- 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.5.0


-- | 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 "dot"
--   program from the graphviz suite.
toDot :: (Show v) => OBDD v -> String

-- | Calls the <tt>dot</tt> executable (must be in <tt>$PATH</tt>) to draw
--   a diagram in an X11 window. Will block until this window is closed.
--   Window can be closed gracefully by typing <tt>q</tt> when it has
--   focus.
display :: Show v => OBDD v -> IO ()
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 (GHC.Classes.Ord i, GHC.Classes.Ord v) => GHC.Classes.Ord (OBDD.Data.Node v i)
instance (GHC.Classes.Eq i, GHC.Classes.Eq v) => GHC.Classes.Eq (OBDD.Data.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
variable :: Ord v => v -> OBDD v
false :: Ord v => OBDD v
true :: Ord v => OBDD v

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

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

-- | 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
instance GHC.Show.Show OBDD.Operation.Symmetricity

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, pure Haskell implementation.
--   (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

-- | Calls the <tt>dot</tt> executable (must be in <tt>$PATH</tt>) to draw
--   a diagram in an X11 window. Will block until this window is closed.
--   Window can be closed gracefully by typing <tt>q</tt> when it has
--   focus.
display :: Show v => OBDD v -> IO ()

module OBDD.Linopt
type Item v w = (w, [(v, Bool)])

-- | solve the constrained linear optimisation problem: returns an
--   assignment that is a model of the BDD and maximises the sum of weights
--   of variables.
linopt :: (Ord v, Num w, Ord w) => OBDD v -> Map v w -> Maybe (w, Map v Bool)
fill :: (Ord v, Num w) => Map v w -> v -> Item v w -> Item v w
noadd :: (Ord v, Num w) => Map v w -> v -> Item v w -> Item v w
add :: (Ord v, Num w) => Map v w -> v -> Item v w -> Item v w