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 |
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.
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.
The type of aggregations of BooleanVariable
s.
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
Substitutions.
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
Formula
s 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.
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.
:: b | f |
-> b |
Extracts the variable labelling the topmost node in f.
:: b | f |
-> b |
Extracts the this-node-false-branch of a f.
:: b | f |
-> b |
Extracts the this-node-true-branch of a f.
:: 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.
:: b | f |
-> b |
Finds a satisfying variable assignment for f.
:: 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.
ReorderNone | Switch off variable reordering. |
ReorderSift | Sifting |
ReorderSiftSym | Sifting with identification of symmetric variables |
ReorderStableWindow3 | Window permutation. |
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
.