Data.DecisionDiagram.BDD

Reduced Ordered Binary Decision Diagrams (ROBDD).

References:

• Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986, doi: 10.1109/TC.1986.1676819. https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

The BDD type

data BDD a where

Reduced ordered binary decision diagram representing boolean function

Bundled Patterns

pattern F :: BDD a

pattern T :: BDD a

pattern Branch :: Int -> BDD a -> BDD a -> BDD a

Smart constructor that takes the BDD reduction rules into account

Instances

Eq (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

(==) :: BDD a -> BDD a -> Bool

(/=) :: BDD a -> BDD a -> Bool

Read (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

readsPrec :: Int -> ReadS (BDD a)

readList :: ReadS [BDD a]

readPrec :: ReadPrec (BDD a)

readListPrec :: ReadPrec [BDD a]

Show (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

showsPrec :: Int -> BDD a -> ShowS

show :: BDD a -> String

showList :: [BDD a] -> ShowS

Hashable (BDD a)

Defined in Data.DecisionDiagram.BDD

Methods

hashWithSalt :: Int -> BDD a -> Int

hash :: BDD a -> Int

Item ordering

class ItemOrder a where

Methods

compareItem :: proxy a -> Int -> Int -> Ordering

Instances

ItemOrder DescOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy DescOrder -> Int -> Int -> Ordering

ItemOrder AscOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy AscOrder -> Int -> Int -> Ordering

data AscOrder

Instances

ItemOrder AscOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy AscOrder -> Int -> Int -> Ordering

data DescOrder

Instances

ItemOrder DescOrder

Defined in Data.DecisionDiagram.BDD.Internal.ItemOrder

Methods

compareItem :: proxy DescOrder -> Int -> Int -> Ordering

withDefaultOrder :: forall r. (forall a. ItemOrder a => Proxy a -> r) -> r

Currently the default order is AscOrder

withAscOrder :: forall r. (Proxy AscOrder -> r) -> r

withDescOrder :: forall r. (Proxy DescOrder -> r) -> r

withCustomOrder :: forall r. (Int -> Int -> Ordering) -> (forall a. ItemOrder a => Proxy a -> r) -> r

Boolean operations

true :: BDD a

True

false :: BDD a

False

var :: Int -> BDD a

A variable \(x_i\)

notB :: BDD a -> BDD a

Negation of a boolean function

(.&&.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 3

Conjunction of two boolean function

(.||.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 2

Disjunction of two boolean function

xor :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a

XOR

(.=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infixr 1

Implication

(.<=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a infix 1

Equivalence

ite :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a

If-then-else

andB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a

Conjunction of a list of BDDs.

orB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a

Disjunction of a list of BDDs.

Quantification

forAll :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Universal quantification (∀)

exists :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Existential quantification (∃)

existsUnique :: forall a. ItemOrder a => Int -> BDD a -> BDD a

Unique existential quantification (∃!)

forAllSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Universal quantification (∀) over a set of variables

existsSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Existential quantification (∃) over a set of variables

existsUniqueSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a

Unique existential quantification (∃!) over a set of variables

Query

support :: BDD a -> IntSet

All the variables that this BDD depends on.

evaluate :: (Int -> Bool) -> BDD a -> Bool

Evaluate a boolean function represented as BDD under the valuation given by (Int -> Bool), i.e. it lifts a valuation function from variables to BDDs.

Restriction / Cofactor

restrict :: forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a

Compute \(F_x \) or \(F_{\neg x} \).

restrictSet :: forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a

Compute \(F_{\{x_i = v_i\}_i} \).

restrictLaw :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a

Compute generalized cofactor of F with respect to C.

Note that C is the first argument.

Substition / Composition

subst :: forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a

subst x N M computes substitution \(M_{x = N}\).

This operation is also known as Composition.

substSet :: forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a

Simultaneous substitution

Fold

fold :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b

Fold over the graph structure of the BDD.

It takes values for substituting false (F) and true (T), and a function for substiting non-terminal node (Branch).

fold' :: b -> b -> (Int -> b -> b -> b) -> BDD a -> b

Strict version of fold

Conversion from/to graphs

type Graph = IntMap Node

data Node

Constructors

NodeF

NodeT

NodeBranch !Int Int Int

Instances

Eq Node

Defined in Data.DecisionDiagram.BDD

Methods

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

(/=) :: Node -> Node -> Bool

Read Node

Defined in Data.DecisionDiagram.BDD

Methods

readsPrec :: Int -> ReadS Node

readList :: ReadS [Node]

readPrec :: ReadPrec Node

readListPrec :: ReadPrec [Node]

Show Node

Defined in Data.DecisionDiagram.BDD

Methods

showsPrec :: Int -> Node -> ShowS

show :: Node -> String

showList :: [Node] -> ShowS

toGraph :: BDD a -> (Graph, Int)

Convert a BDD into a pointed graph

toGraph' :: Traversable t => t (BDD a) -> (Graph, t Int)

Convert multiple BDDs into a graph

fromGraph :: (Graph, Int) -> BDD a

Convert a pointed graph into a BDD

fromGraph' :: Graph -> IntMap (BDD a)

Convert nodes of a graph into BDDs