bdd_setcacheratio

int bdd_setcacheratio ( int  r  )  Sets the cache ratio for the operator caches. The ratio between the number of nodes in the nodetable and the number of entries in the operator cachetables is called the cache ratio. So a cache ratio of say, four, allocates one cache entry for each four unique node entries. This value can be set with bdd_setcacheratio to any positive value. When this is done the caches are resized instantly to fit the new ratio. The default is a fixed cache size determined at initialization time. Returns: The previous cache ratio or a negative number on error. See also: bdd_init

---