bdd_fprintstat

void bdd_fprintstat ( FILE *  f  )  Print cache statistics to a file. Prints information about the cache performance to the supplied file f. The information contains the number of accesses to the unique node table, the number of times a node was (not) found there and how many times a hash chain had to traversed. Hit and miss count is also given for the operator caches. See also: bddCacheStat, bdd_cachestats, bdd_printstat

---