-- 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. -- -- This is mostly educational. The BDDs do not share nodes and this might -- introduce inefficiencies. -- -- An important (for me, in teaching) feature is that I can immediately -- draw the BDD to an X11 window (via graphviz). For example, to show the -- effect of different variable orderings, try this in ghci: -- -- 
--   import qualified Prelude as P
--   import OBDD
--   let f [] = false; f (x:y:zs) = x && y || f zs
--   display P.$ f P.$ P.map variable [1,2,3,4,5,6]
--   display P.$ f P.$ P.map variable [1,4,2,5,3,6]
--
-- -- If you want better performance, use CUDD Haskell -- bindings, see this example. @package obdd @version 0.6.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] -- | 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. fold :: Ord v => (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a -- | Run action in each node, bottum-up. return the value in the root node. -- Will cache intermediate results. foldM :: (Monad m, Ord v) => (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m 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_fold :: Ord v => Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a full_foldM :: (Monad m, Ord v) => Set 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 dot executable (must be in $PATH) to draw -- a diagram in an X11 window. Will block until this window is closed. -- Window can be closed gracefully by typing q 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 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 -- | 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 -- | 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. fold :: Ord v => (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a -- | Run action in each node, bottum-up. return the value in the root node. -- Will cache intermediate results. foldM :: (Monad m, Ord v) => (Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m 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_fold :: Ord v => Set v -> (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a full_foldM :: (Monad m, Ord v) => Set 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 - 2016 -- -- This module is intended to be imported qualified because it overloads -- some Prelude names. module OBDD -- | assumes total ordering on variables data OBDD v -- | Calls the dot executable (must be in $PATH) to draw -- a diagram in an X11 window. Will block until this window is closed. -- Window can be closed gracefully by typing q when it has -- focus. display :: Show v => OBDD v -> IO () module OBDD.Linopt -- | solve the constrained linear optimisation problem: returns an -- assignment that is a model of the BDD and maximises the sum of weights -- of variables. The set of keys of the weight map *must* be the full set -- of variables. linopt :: (Ord v, Num w, Ord w) => OBDD v -> Map v w -> Maybe (w, Map v Bool)