BuDDy: bdd_blockfile

bddfilehandler bdd_blockfile_hook ( bddfilehandler handler )

Specifies a printing callback handler.

A printing callback handler is used to convert the variable block identifiers into something readable by the end user. Use bdd_blockfile_hook to pass a handler to BuDDy. A typical handler could look like this:

 void printhandler(FILE *o, int * block)
 { 
   extern char **blocknames; 
   fprintf(o, "%s", blocknames[block]); 
 }

The handler is then called from bdd_printorder and bdd_reorder (depending on the verbose level) with the block numbers returned by bdd_addvarblock as arguments. No default handler is supplied. The argument handler may be NULL if no handler is needed.

Returns:: The old handler.

See also:: bdd_printorder