hBDD-0.0.3: An abstraction layer for BDD libraries

Copyright(C) 2002-2005, 2009 University of New South Wales, (C) 2009-2011 Peter Gammie
LicenseLGPL (see COPYING.LIB for details)
Safe HaskellSafe-Inferred




An interface to libraries supporting efficient manipulation of Boolean functions, such as BDDs. It is an evolution of Logical Abstractions in Haskell by Nancy A. Day, John Launchbury and Jeff Lewis, Haskell Workshop, Paris, October 1999.

The purity of this interface may make it difficult to predict when BDDs actually get constructed.

Note the use of neg rather than not to avoid a clash with Prelude.not.


Abstract interface.

class BooleanVariable b where Source

Boolean variables.

Minimal complete definition

bvar, unbvar


bvar :: String -> b Source

A single variable.

bvars :: [String] -> [b] Source

A set of variables, notionally 'adjacent'. What this means is implementation-defined, but the intention is to support (current, next)-state variable pairing.

unbvar :: b -> String Source

Reverse mapping.


class Boolean b where Source

The operators have similar fixities and associativies to the standard boolean operators, but at higher precedence (they bind more strongly).

The overloaded Boolean operations proper. Provides defaults for operations with obvious expansions, such as nand. A minimal instance should define '(/)' and neg.

Minimal complete definition

false, true, (/\), neg


false :: b Source

true :: b Source

(/\) :: b -> b -> b infixr 7 Source

neg :: b -> b Source

nand :: b -> b -> b infixr 8 Source

(\/) :: b -> b -> b infixr 6 Source

nor :: b -> b -> b infixr 8 Source

xor :: b -> b -> b infixr 8 Source

(-->) :: b -> b -> b infixr 5 Source


(<->) :: b -> b -> b infixr 5 Source

If-and-only-if is exclusive nor.


class (Boolean b, BooleanVariable b) => QBF b where Source

Quantified Boolean Formulae (QBF) operations.

Minimal complete definition

mkGroup, exists, forall

Associated Types

data Group b :: * Source

The type of aggregations of BooleanVariables.

Some BDD packages have efficient (reusable) variable aggregation structures.


mkGroup :: [b] -> Group b Source

Construct aggregations.

exists :: Group b -> b -> b Source

Existentially quantify out a given set of variables.

forall :: Group b -> b -> b Source

Universally quantify out a given set of variables.

rel_product :: Group b -> b -> b -> b Source

Computes the relational product of two Boolean formulas:

rel_product qvars f g = exists qvars (f /\ g)


class (Boolean b, BooleanVariable b) => Substitution b where Source


Minimal complete definition

mkSubst, substitute

Associated Types

data Subst b :: * Source


mkSubst :: [(b, b)] -> Subst b Source

Builds a new substitution. The arguments are (Variable, Formula) pairs.

rename :: Subst b -> b -> b Source

Substitutes variables for variables in a Boolean formula. Note that it is the user's responsibility to ensure the Formulas in the substitution are in fact BDD variables, and that the domain and range do not overlap.

substitute :: Subst b -> b -> b Source

Substitutes formulas for variables in a Boolean formula.


Derived boolean operations.

(<--) :: Boolean b => b -> b -> b infixl 5 Source

Reverse implication

conjoin :: Boolean b => [b] -> b Source

Forms the Big Conjunction of a list of Boolean formulas.

disjoin :: Boolean b => [b] -> b Source

Forms the Big Disjunction of a list of Boolean formulas.

fix :: Eq b => b -> (b -> b) -> b Source

Compute the fixpoint of a Boolean function.

fix2 :: Eq b => a -> b -> (a -> b -> (a, b)) -> (a, b) Source

"fix" with state.

BDD-specific operations.

class (Eq b, QBF b, Substitution b) => BDDOps b where Source

Operations provided by BDD representations.

Note that the Eq instance is expected to provide semantic equality on boolean functions, as is typical of BDD packages.


get_bdd_ptr :: b -> IntPtr Source

Return a pointer to the underlying representation.

bif Source


:: b


-> b 

Extracts the variable labelling the topmost node in f.

belse Source


:: b


-> b 

Extracts the this-node-false-branch of a f.

bthen Source


:: b


-> b 

Extracts the this-node-true-branch of a f.

reduce Source


:: b


-> b

g (a care set)

-> b 

Returns a BDD which agrees with f for all valuations for which g is true, and which is hopefully smaller than f.

satisfy Source


:: b


-> b 

Finds a satisfying variable assignment for f.

support Source


:: b


-> [b] 

Finds the set of variables that f depends on.

data ReorderingMethod Source

BDD libraries tend to include some kind of variable reordering heuristics. These are some common ones.



Switch off variable reordering.




Sifting with identification of symmetric variables


Window permutation.

class RenderBool a where Source

A class for the text constants and operators used by sop.


rbTrue :: a Source

rbFalse :: a Source

rbVar :: String -> a Source

rbAnd :: a Source

rbOr :: a Source

rbNeg :: a Source

rbEmpty :: a Source

rbConcat :: a -> a -> a Source


sop :: (BDDOps b, RenderBool a) => b -> a Source

Render a Boolean type as a sum-of-products. This was stolen lock-stock from David Long's calculator example.

countPaths :: BDDOps b => b -> Integer Source

Count the number of paths in a BDD leading to true.