| Copyright | (C) 2002-2005, 2009 University of New South Wales, (C) 2009-2011 Peter Gammie |
|---|---|
| License | LGPL (see COPYING.LIB for details) |
| Safe Haskell | Safe-Inferred |
| Language | Haskell98 |
Data.Boolean
Description
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.
- class BooleanVariable b where
- class Boolean b where
- class (Boolean b, BooleanVariable b) => QBF b where
- class (Boolean b, BooleanVariable b) => Substitution b where
- (<--) :: Boolean b => b -> b -> b
- conjoin :: Boolean b => [b] -> b
- disjoin :: Boolean b => [b] -> b
- fix :: Eq b => b -> (b -> b) -> b
- fix2 :: Eq b => a -> b -> (a -> b -> (a, b)) -> (a, b)
- class (Eq b, QBF b, Substitution b) => BDDOps b where
- data ReorderingMethod
- class RenderBool a where
- sop :: (BDDOps b, RenderBool a) => b -> a
- countPaths :: BDDOps b => b -> Integer
Abstract interface.
class BooleanVariable b where Source
Boolean variables.
Methods
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.
Reverse mapping.
Instances
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.
class (Boolean b, BooleanVariable b) => QBF b where Source
Quantified Boolean Formulae (QBF) operations.
Associated Types
The type of aggregations of BooleanVariables.
Some BDD packages have efficient (reusable) variable aggregation structures.
Methods
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
Substitutions.
Minimal complete definition
Methods
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.
Instances
Derived boolean operations.
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.
Methods
get_bdd_ptr :: b -> IntPtr Source
Return a pointer to the underlying representation.
Arguments
| :: b | f |
| -> b |
Extracts the variable labelling the topmost node in f.
Arguments
| :: b | f |
| -> b |
Extracts the this-node-false-branch of a f.
Arguments
| :: b | f |
| -> b |
Extracts the this-node-true-branch of a f.
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.
Arguments
| :: b | f |
| -> b |
Finds a satisfying variable assignment for f.
Arguments
| :: b | f |
| -> [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.
Constructors
| ReorderNone | Switch off variable reordering. |
| ReorderSift | Sifting |
| ReorderSiftSym | Sifting with identification of symmetric variables |
| ReorderStableWindow3 | Window permutation. |
class RenderBool a where Source
A class for the text constants and operators used by sop.
Methods
Instances
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.