Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class Boolean b where
- bool :: Bool -> b
- true :: b
- false :: b
- (&&) :: b -> b -> b
- (||) :: b -> b -> b
- (==>) :: b -> b -> b
- not :: b -> b
- and :: Foldable t => t b -> b
- or :: Foldable t => t b -> b
- nand :: Foldable t => t b -> b
- nor :: Foldable t => t b -> b
- all :: Foldable t => (a -> b) -> t a -> b
- any :: Foldable t => (a -> b) -> t a -> b
- xor :: b -> b -> b
- choose :: b -> b -> b -> b
- equiv :: 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
- instantiate :: Ord v => v -> Bool -> OBDD v -> OBDD v
- exists :: Ord v => v -> OBDD v -> OBDD v
- 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
- 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
- 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
Documentation
The normal Bool
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 Generic
Nothing
Lift a Bool
(&&) :: b -> b -> b infixr 3 #
Logical conjunction.
(||) :: b -> b -> b infixr 2 #
Logical disjunction (inclusive or).
(==>) :: b -> b -> b infixr 0 #
Logical implication.
Logical negation
and :: Foldable t => t b -> b #
The logical conjunction of several values.
or :: Foldable t => t b -> b #
The logical disjunction of several values.
nand :: Foldable t => t b -> b #
nor :: Foldable t => t b -> b #
all :: Foldable t => (a -> b) -> t a -> b #
The logical conjunction of the mapping of a function over several values.
any :: Foldable t => (a -> b) -> t a -> b #
The logical disjunction of the mapping of a function over several values.
Exclusive-or
:: b | False branch |
-> b | True branch |
-> b | Predicate/selector branch |
-> b |
Choose between two alternatives based on a selector bit.
Instances
Boolean Bit | |
Boolean Bool | |
Defined in Ersatz.Bit (&&) :: Bool -> Bool -> Bool # (||) :: Bool -> Bool -> Bool # (==>) :: Bool -> Bool -> Bool # and :: Foldable t => t Bool -> Bool # or :: Foldable t => t Bool -> Bool # nand :: Foldable t => t Bool -> Bool # nor :: Foldable t => t Bool -> Bool # all :: Foldable t => (a -> Bool) -> t a -> Bool # | |
Ord v => Boolean (OBDD v) Source # | |
Defined in OBDD.Operation (&&) :: OBDD v -> OBDD v -> OBDD v # (||) :: OBDD v -> OBDD v -> OBDD v # (==>) :: OBDD v -> 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 # |
unary :: Ord v => (Bool -> Bool) -> OBDD v -> OBDD v Source #
FIXME: this function is nonsensical. There is only one interesting unary Boolean function (negation), and it should be handled differently.
exists_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v Source #
remove variables existentially
fold :: Ord v => (Bool -> a) -> (v -> a -> a -> a) -> OBDD v -> a Source #
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 Source #
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 Source #
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 Source #
Orphan instances
Ord v => Boolean (OBDD v) Source # | |
(&&) :: OBDD v -> OBDD v -> OBDD v # (||) :: OBDD v -> OBDD v -> OBDD v # (==>) :: OBDD v -> 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 # |