Data.Boolean

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

Boolean variables.

Minimal complete definition

bvar, unbvar

Methods

bvar :: String -> b

A single variable.

bvars :: [String] -> [b]

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

Reverse mapping.

Instances

BooleanVariable BF

class Boolean b where

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

Methods

false :: b

true :: b

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

neg :: b -> b

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

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

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

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

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

Implication

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

If-and-only-if is exclusive nor.

Instances

Boolean Bool

Boolean BF

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

Quantified Boolean Formulae (QBF) operations.

Minimal complete definition

mkGroup, exists, forall

Associated Types

data Group b :: *

The type of aggregations of BooleanVariables.

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

Methods

mkGroup :: [b] -> Group b

Construct aggregations.

exists :: Group b -> b -> b

Existentially quantify out a given set of variables.

forall :: Group b -> b -> b

Universally quantify out a given set of variables.

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

Computes the relational product of two Boolean formulas:

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

Instances

QBF BF

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

Substitutions.

Minimal complete definition

mkSubst, substitute

Associated Types

data Subst b :: *

Methods

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

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

rename :: Subst b -> b -> b

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

Substitutes formulas for variables in a Boolean formula.

Instances

Substitution BF

Derived boolean operations.

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

Reverse implication

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

Forms the Big Conjunction of a list of Boolean formulas.

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

Forms the Big Disjunction of a list of Boolean formulas.

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

Compute the fixpoint of a Boolean function.

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

"fix" with state.

BDD-specific operations.

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

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.

Methods

get_bdd_ptr :: b -> IntPtr

Return a pointer to the underlying representation.

bif

Arguments

:: b

f

-> b

Extracts the variable labelling the topmost node in f.

belse

Arguments

:: b

f

-> b

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

bthen

Arguments

:: b

f

-> b

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

reduce

Arguments

:: b

f

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

Arguments

:: b

f

-> b

Finds a satisfying variable assignment for f.

support

Arguments

:: b

f

-> [b]

Finds the set of variables that f depends on.

data ReorderingMethod

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

Constructors

ReorderNone

Switch off variable reordering.

ReorderSift

Sifting

ReorderSiftSym

Sifting with identification of symmetric variables

ReorderStableWindow3

Window permutation.

Instances

Eq ReorderingMethod

Ord ReorderingMethod

Show ReorderingMethod

class RenderBool a where

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

Methods

rbTrue :: a

rbFalse :: a

rbVar :: String -> a

rbAnd :: a

rbOr :: a

rbNeg :: a

rbEmpty :: a

rbConcat :: a -> a -> a

Instances

RenderBool ShowS

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

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

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