Lines Matching refs:function
110 In Version~1 there was a function, called
269 Initialisation is done with the ML function
309 The function
320 The function
333 using the function \t{stats}
393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE.
421 dynamically. The function
430 The function
478 \Muddy{} provides a function for general purpose simultaneous
504 Variables can be renamed using the function \t{replace} that takes
519 {\t{FALSE}} using the function \t{restrict} that takes
573 The ML function
590 The function \t{appall} universally quantifies the result of the
665 The number of nodes in a BDD is computed by the function
679 \Buddy's representation into an ML vector). Thus the ML function
680 provided by \Muddy{} invokes \Buddy's \t{nodecount} function directly
684 function
694 The function
703 a function that counts the number of valuations of a BDD using
733 The ML function
770 The function
961 first component is the \emph{destructor} (a function pointer) and the
968 using the function
1158 There is also a single oracle function
2072 \hbc{GenTermToTermBdd : (term -> \termbddty) -> varmap -> term -> \termbddty}{Scan a term and construct a term\_bdd using the primitive operations when applicable, and a supplied function on leaves when all else fails.}
2211 Fails if \texttt{GenTermToTermBdd} fails on $t2$ with the supplied leaf function.}
2255 and the function reportfn is applied to the iteration level and current