An interface to libraries supporting efficient manipulation of
Boolean functions, such as BDDs. It is an evolution of
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
- 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
A single variable.
A set of variables, notionally 'adjacent'. What this means is implementation-defined, but the intention is to support (current, next)-state variable pairing.
The operators have similar fixities and associativies to the standard boolean operators, but at higher precedence (they bind more strongly).
If-and-only-if is exclusive nor.
Quantified Boolean Formulae (QBF) operations.
The type of aggregations of
Some BDD packages have efficient (reusable) variable aggregation structures.
Existentially quantify out a given set of variables.
Universally quantify out a given set of variables.
Computes the relational product of two
rel_product qvars f g = exists qvars (f /\ g)
Builds a new substitution. The arguments are
(Variable, Formula) pairs.
Substitutes variables for variables in a
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.
Substitutes formulas for variables in a
Derived boolean operations.
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.
Return a pointer to the underlying representation.
Extracts the variable labelling the topmost node in f.
Extracts the this-node-false-branch of a f.
Extracts the this-node-true-branch of a f.
g (a care set)
Returns a BDD which agrees with f for all valuations for which g is true, and which is hopefully smaller than f.
Finds a satisfying variable assignment for f.
Finds the set of variables that f depends on.
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
A class for the text constants and operators used by
Boolean type as a sum-of-products. This was stolen
lock-stock from David Long's calculator example.