-- 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 (there is no
--   persistent BDD base) 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 (type
--   <a>q</a> to close the drawing windows).
--   
--   <pre>
--   import Prelude hiding (not,(&amp;&amp;),(||),and,or,any,all)
--   import OBDD
--   let f [] = false; f (x:y:zs) = x &amp;&amp; y || f zs
--   display $ f $ map variable [1,2,3,4,5,6]
--   display $ f $ map variable [1,4,2,5,3,6]
--   </pre>
--   
--   <a>OBDD</a> implements <a>Ersatz.Boolean</a> which re-defines Boolean
--   operations from the Prelude. The recommended way of using this is
--   shown in the previous example.
--   
--   If you want better performance, use a library with a persistent BDD
--   base, e.g., <a>CUDD</a> <a>Haskell bindings</a>, see <a>this
--   example</a>.
@package obdd
@version 0.8.4


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

-- | all variables that occur in the nodes
variables :: Ord v => OBDD v -> Set v

-- | list of all paths
paths :: Ord v => OBDD v -> [Map v Bool]

-- | list of all models (a.k.a. minterms)
models :: Ord k => Set k -> OBDD k -> [Map k Bool]

-- | randomly select one model, if possible
some_model :: Ord v => OBDD v -> IO (Maybe (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
--   <tt>count_models = fold (b -&gt; if b then 1 else 0) (v l r -&gt; l +
--   r)</tt> but that's not true because a path might omit variables. Use
--   <tt>full_fold</tt> 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 <tt>branch</tt> function on an
--   interpolated node that contains this missing variable, and identical
--   children. With this function, <tt>number_of_models</tt> can be
--   implemented as <tt>full_fold vars (bool 0 1) ( const (+) )</tt>. 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
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
top :: OBDD v -> Index
access :: OBDD v -> Node v (OBDD v)
not_ :: OBDD v -> OBDD v
assocs :: OBDD v -> [(Index, Node v Index)]
instance (GHC.Classes.Ord v, GHC.Classes.Ord i) => GHC.Classes.Ord (OBDD.Data.Node v i)
instance (GHC.Classes.Eq v, GHC.Classes.Eq i) => GHC.Classes.Eq (OBDD.Data.Node v i)

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

-- | list of all paths
paths :: Ord v => OBDD v -> [Map v Bool]

-- | list of all models (a.k.a. minterms)
models :: Ord k => Set k -> OBDD k -> [Map k Bool]
size :: OBDD v -> Index


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

module OBDD.Operation

-- | The normal <a>Bool</a> operators in Haskell are not overloaded. This
--   provides a richer set that are.
--   
--   Instances for this class for product-like types can be automatically
--   derived for any type that is an instance of <a>Generic</a>
class Boolean b

-- | Lift a <a>Bool</a>
bool :: Boolean b => Bool -> b

-- | <pre>
--   <a>true</a> = <a>bool</a> <a>True</a>
--   </pre>
true :: Boolean b => b

-- | <pre>
--   <a>false</a> = <a>bool</a> <a>False</a>
--   </pre>
false :: Boolean b => b

-- | Logical conjunction.
(&&) :: Boolean b => b -> b -> b

-- | Logical disjunction (inclusive or).
(||) :: Boolean b => b -> b -> b

-- | Logical implication.
(==>) :: Boolean b => b -> b -> b

-- | Logical negation
not :: Boolean b => b -> b

-- | The logical conjunction of several values.
and :: (Boolean b, Foldable t) => t b -> b

-- | The logical disjunction of several values.
or :: (Boolean b, Foldable t) => t b -> b

-- | The negated logical conjunction of several values.
--   
--   <pre>
--   <a>nand</a> = <a>not</a> . <a>and</a>
--   </pre>
nand :: (Boolean b, Foldable t) => t b -> b

-- | The negated logical disjunction of several values.
--   
--   <pre>
--   <a>nor</a> = <a>not</a> . <a>or</a>
--   </pre>
nor :: (Boolean b, Foldable t) => t b -> b

-- | The logical conjunction of the mapping of a function over several
--   values.
all :: (Boolean b, Foldable t) => (a -> b) -> t a -> b

-- | The logical disjunction of the mapping of a function over several
--   values.
any :: (Boolean b, Foldable t) => (a -> b) -> t a -> b

-- | Exclusive-or
xor :: Boolean b => b -> b -> b

-- | Choose between two alternatives based on a selector bit.
choose :: Boolean b => b -> b -> b -> b
infixr 2 ||
infixr 3 &&
infixr 0 ==>
equiv :: Ord v => OBDD v -> OBDD v -> OBDD v

-- | FIXME: this function is nonsensical. There is only one interesting
--   unary Boolean function (negation), and it should be handled
--   differently.
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
exists :: Ord v => v -> OBDD v -> OBDD v

-- | remove variables existentially
exists_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v
forall :: Ord v => v -> OBDD v -> OBDD v
forall_many :: (Foldable c, Ord v) => c 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
--   <tt>count_models = fold (b -&gt; if b then 1 else 0) (v l r -&gt; l +
--   r)</tt> but that's not true because a path might omit variables. Use
--   <tt>full_fold</tt> 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 <tt>branch</tt> function on an
--   interpolated node that contains this missing variable, and identical
--   children. With this function, <tt>number_of_models</tt> can be
--   implemented as <tt>full_fold vars (bool 0 1) ( const (+) )</tt>. 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
instance GHC.Classes.Ord v => Ersatz.Bit.Boolean (OBDD.Data.OBDD v)

module OBDD.Display

-- | 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 :: (Ord v, Show v) => OBDD v -> IO ()

-- | same as <tt>display</tt>, but does not show the <tt>False</tt> node
--   and the edges pointing to <tt>False</tt>.
display' :: (Ord v, Show v) => OBDD v -> IO ()

-- | a textual representation of the BDD that is suitable as input to the
--   "dot" program from the graphviz suite.
toDot :: (Ord v, Show v) => Bool -> OBDD v -> Text
fresh :: Monoid b => RWS a b Int Int
mkLabel :: Text -> Text
unquote :: Text -> Text
text :: Show a => a -> Text


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

-- | Apply function in each node, bottom-up. return the value in the root
--   node. Will cache intermediate results. You might think that
--   <tt>count_models = fold (b -&gt; if b then 1 else 0) (v l r -&gt; l +
--   r)</tt> but that's not true because a path might omit variables. Use
--   <tt>full_fold</tt> 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 <tt>branch</tt> function on an
--   interpolated node that contains this missing variable, and identical
--   children. With this function, <tt>number_of_models</tt> can be
--   implemented as <tt>full_fold vars (bool 0 1) ( const (+) )</tt>. 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
size :: OBDD v -> Index

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

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

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

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

-- | all variables that occur in the nodes
variables :: Ord v => OBDD v -> Set v

-- | list of all paths
paths :: Ord v => OBDD v -> [Map v Bool]

-- | list of all models (a.k.a. minterms)
models :: Ord k => Set k -> OBDD k -> [Map k Bool]
instance GHC.Classes.Ord v => GHC.Classes.Eq (OBDD.Data.OBDD v)

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. Keys missing from the weight map, but present in the
--   BDD, get weight zero.
linopt :: (Ord v, Num w, Ord w) => OBDD v -> Map v w -> Maybe (w, Map v Bool)

module OBDD.Cube
type Cube v = Map v Bool
primes :: Ord v => OBDD v -> [Cube v]
nice :: Show v => Cube v -> String
data Check
Sign :: Check
Occurs :: Check
Original :: Check
sign :: Ord a => a -> OBDD (a, Check)
occurs :: Ord a => a -> OBDD (a, Check)
original :: Ord a => a -> OBDD (a, Check)
process :: Ord k => Map (k, Check) Bool -> Map k Bool

-- | O. Coudert , J. C. Madre:
--   <a>http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3330</a>
prime :: Ord v => OBDD v -> OBDD (v, Check)
dnf :: Ord v => OBDD v -> [Cube v]
cnf :: Ord k => OBDD k -> [Map k Bool]
greed :: forall a b. (Ord b, Ord a) => Map a b -> [Set a] -> Set a
clause :: Ord v => Map v Bool -> OBDD v
instance GHC.Show.Show OBDD.Cube.Check
instance GHC.Classes.Ord OBDD.Cube.Check
instance GHC.Classes.Eq OBDD.Cube.Check