úÎ;°7˜D      !"#$%&'()*+,-./0123456789:;<=>?@ABCM(C) 2002-2005, 2009 University of New South Wales, (C) 2009-2011 Peter Gammie"LGPL (see COPYING.LIB for details) Safe-Inferred24=K&5A class for the text constants and operators used by 5. gBDD libraries tend to include some kind of variable reordering heuristics. These are some common ones. Window permutation. 2Sifting 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.2Return 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 %D 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.LSome BDD packages have efficient (reusable) variable aggregation structures.Construct aggregations.4Existentially quantify out a given set of variables.2Universally 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 standard boolean operators, but at higher precedence (they bind more strongly).mThe 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 implication1'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.4"fix" 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 ffffg (a care set)ff !"#$%&'()*+,-./0123456EF7  !"#$%&'()*+,-./01234567!"#$%&'()*+,-./ 01234 56   !"#$% &'()*+,-./0123456EF(*+,-./0M(C) 2002-2005, 2009 University of New South Wales, (C) 2009-2011 Peter Gammie"LGPL (see COPYING.LIB for details) Safe-Inferred24=K7,An abstract syntax tree-ish instance of the %, interface, sometimes useful for debugging. Note the D instance is not semantic equality.789:;<=>?@ABCGHIJKLMNO 789:;<=>?@ABC 7CBA@?>=<;:987 CBA@?>=<;:98KJGMLHINOP      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTU hBDD-0.0.3 Data.BooleanData.Boolean.BF RenderBoolrbTruerbFalserbVarrbAndrbOrrbNegrbEmptyrbConcatReorderingMethodReorderStableWindow3ReorderSiftSym ReorderSift ReorderNoneBDDOps get_bdd_ptrbifbelsebthenreducesatisfysupport SubstitutionSubstmkSubstrename substituteQBFGroupmkGroupexistsforall rel_productBooleanVariablebvarbvarsunbvarBooleanfalsetrue/\negnand\/norxor--><-><--conjoindisjoinfixfix2sop countPathsBFBFsubstBFforallBFexistsBFnegBFiff BFimpliesBFxorBForBFandBFvarBFfalseBFtrueghc-prim GHC.ClassesEq$fRenderBool(->) $fBooleanBoolMkBFpairMkGroup unMkGroupTFCo:R:SubstBF$fSubstitutionBFTFCo:R:GroupBF$fQBFBF $fBooleanBF$fBooleanVariableBF