BuDDy: bdd_file

bddfilehandler bdd_file_hook ( bddfilehandler handler )

Specifies a printing callback handler.

A printing callback handler for use with BDDs is used to convert the BDD variable number into something readable by the end user. Typically the handler will print a string name instead of the number. A handler could look like this:

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

The handler can then be passed to BuDDy like this:

 bdd_file_hook(printhandler);

No default handler is supplied. The argument handler may be NULL if no handler is needed.

Returns:: The old handler.

See also:: bdd_printset, bdd_strm_hook, fdd_file_hook