Safe Haskell | Safe-Infered |
---|
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 whereSource
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
.
Implication
If-and-only-if is exclusive nor.
class (Boolean b, BooleanVariable b) => QBF b whereSource
Quantified Boolean Formulae (QBF) operations.
The type of aggregations of BooleanVariable
s.
Some BDD packages have efficient (reusable) variable aggregation structures.
mkGroup :: [b] -> Group bSource
Construct aggregations.
exists :: Group b -> b -> bSource
Existentially quantify out a given set of variables.
forall :: Group b -> b -> bSource
Universally quantify out a given set of variables.
rel_product :: Group b -> b -> b -> bSource
Computes the relational product of two Boolean
formulas:
rel_product qvars f g = exists qvars (f /\ g)
class (Boolean b, BooleanVariable b) => Substitution b whereSource
Substitutions.
mkSubst :: [(b, b)] -> Subst bSource
Builds a new substitution. The arguments are
(Variable, Formula)
pairs.
rename :: Subst b -> b -> bSource
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 -> bSource
Substitutes formulas for variables in a Boolean
formula.
Derived boolean operations.
BDD-specific operations.
class (Eq b, QBF b, Substitution b) => BDDOps b whereSource
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 -> IntPtrSource
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 -> aSource
Render a Boolean
type as a sum-of-products. This was stolen
lock-stock from David Long's calculator example.
countPaths :: BDDOps b => b -> IntegerSource
Count the number of paths in a BDD leading to true
.