úÎ84:D      !"#$%&'()*+,-./0123456789:;<=>?@ABC Safe-Infered&5A class for the text constants and operators used by 5. ?BDD libraries tend to include some kind of variable reordering ) heuristics. These are some common ones. Window permutation. 3Sifting with identification of symmetric variables Sifting  Switch off variable reordering. ,Operations provided by BDD representations. Note that the D! instance is expected to provide semantic ? equality on boolean functions, as is typical of BDD packages. 3Return a pointer to the underlying representation. 4Extracts 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.  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. Substitutions. -Builds a new substitution. The arguments are  (Variable, Formula) pairs. )Substitutes variables for variables in a % 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. (Substitutes formulas for variables in a % formula. .Quantified Boolean Formulae (QBF) operations. The type of aggregations of !s. MSome BDD packages have efficient (reusable) variable aggregation structures. Construct aggregations. 5Existentially quantify out a given set of variables. 3Universally quantify out a given set of variables. 'Computes the relational product of two % formulas: (rel_product qvars f g = exists qvars (f /\ g)!Boolean variables. "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. $Reverse mapping. %=The operators have similar fixities and associativies to the A 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 * . A minimal  instance should define '(/)' and ). . Implication /!If-and-only-if is exclusive nor. 0Reverse implication 1'Forms the Big Conjunction of a list of % formulas. 2'Forms the Big Disjunction of a list of % formulas. 3Compute the fixpoint of a Boolean function. 4fix with state. 5 Render a %, type as a sum-of-products. This was stolen  lock-stock from David Long's calculator example. 6.Count the number of paths in a BDD leading to '. 9 f f f f g (a care set) f f  !"#$%&'()*+,-./0123456EF7  !"#$%&'()*+,-./01234567!"#$%&'()*+,-./ 01234 56   !"#$% &'()*+,-./0123456EF Safe-Infered7,An abstract syntax tree-ish instance of the % interface, ! sometimes useful for debugging.  Note the D instance is not semantic equality. 789:;<=>?@ABCGHIJ 789:;<=>?@ABC 7CBA@?>=<;:987 CBA@?>=<;:98GHIJK      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOP hBDD-0.0.2 Data.BooleanData.Boolean.BF RenderBoolrbTruerbFalserbVarrbAndrbOrrbNegrbEmptyrbConcatReorderingMethodReorderStableWindow3ReorderSiftSym ReorderSift ReorderNoneBDDOps get_bdd_ptrbifbelsebthenreducesatisfysupport SubstitutionSubstmkSubstrename substituteQBFGroupmkGroupexistsforall rel_productBooleanVariablebvarbvarsunbvarBooleanfalsetrue/\negnand\/norxor--><-><--conjoindisjoinfixfix2sop countPathsBFBFsubstBFforallBFexistsBFnegBFiff BFimpliesBFxorBForBFandBFvarBFfalseBFtrueghc-prim GHC.ClassesEq$fRenderBool(->) $fBooleanBool$fSubstitutionBF$fQBFBF $fBooleanBF$fBooleanVariableBF