OBDD.Operation

Documentation

class Boolean b where

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

Methods

bool :: Bool -> b

Lift a Bool

true :: b

true = bool True

false :: b

false = bool False

(&&) :: b -> b -> b infixr 3

Logical conjunction.

(||) :: b -> b -> b infixr 2

Logical disjunction (inclusive or).

(==>) :: b -> b -> b infixr 0

Logical implication.

not :: b -> b

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

The negated logical conjunction of several values.

nand = not . and

nor :: Foldable t => t b -> b

The negated logical disjunction of several values.

nor = not . or

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.

xor :: b -> b -> b

Exclusive-or

choose

Arguments

:: b

False branch

-> b

True branch

-> b

Predicate/selector branch

-> b

Choose between two alternatives based on a selector bit.

Instances

Boolean Bool

Methods

bool :: Bool -> Bool

true :: Bool

false :: Bool

(&&) :: Bool -> Bool -> Bool

(||) :: Bool -> Bool -> Bool

(==>) :: Bool -> Bool -> Bool

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

any :: Foldable t => (a -> Bool) -> t a -> Bool

xor :: Bool -> Bool -> Bool

choose :: Bool -> Bool -> Bool -> Bool

Boolean Bit

Methods

bool :: Bool -> Bit

true :: Bit

false :: Bit

(&&) :: Bit -> Bit -> Bit

(||) :: Bit -> Bit -> Bit

(==>) :: Bit -> Bit -> Bit

not :: Bit -> Bit

and :: Foldable t => t Bit -> Bit

or :: Foldable t => t Bit -> Bit

nand :: Foldable t => t Bit -> Bit

nor :: Foldable t => t Bit -> Bit

all :: Foldable t => (a -> Bit) -> t a -> Bit

any :: Foldable t => (a -> Bit) -> t a -> Bit

xor :: Bit -> Bit -> Bit

choose :: Bit -> Bit -> Bit -> Bit

equiv :: Ord v => OBDD v -> OBDD v -> OBDD v

unary :: Ord v => (Bool -> Bool) -> OBDD v -> OBDD v

FIXME: this function is nonsensical. There is only one interesting unary Boolean function (negation), and it should be handled differently.

binary :: Ord v => (Bool -> Bool -> Bool) -> OBDD v -> OBDD v -> OBDD v

instantiate :: Ord v => v -> Bool -> OBDD v -> OBDD v

replace variable by value

exists :: Ord v => v -> OBDD v -> OBDD v

remove variable existentially

exists_many :: (Foldable c, Ord v) => c v -> OBDD v -> OBDD v

remove variables existentially

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

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

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

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

Orphan instances

Ord v => Boolean (OBDD v)

Methods

bool :: Bool -> OBDD v

true :: OBDD v

false :: OBDD v

(&&) :: OBDD v -> OBDD v -> OBDD v

(||) :: OBDD v -> OBDD v -> OBDD v

(==>) :: OBDD v -> OBDD v -> OBDD v

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

xor :: OBDD v -> OBDD v -> OBDD v

choose :: OBDD v -> OBDD v -> OBDD v -> OBDD v