The CIF data-based synthesis BDD library operation ratio size should be inverted
From the code of CifDataSynthesisApp
:
double bddCacheRatio = BddOpCacheRatioOption.getCacheRatio();
...
bddCacheSize = (int)(bddTableSize * bddCacheRatio);
...
factory.setCacheRatio(bddCacheRatio);
Note how the cache ratio is used here as a fraction of the BDD node table size.
It is provided to the factory via setCacheRatio
. JFactory.setCacheRatio
is defined as:
public double setCacheRatio(double x) {
return bdd_setcacheratio((int)x);
}
This means that 1.0
becomes 1
and everything below 1.0
becomes 0
.
The cache ratio is used in JFactory.bdd_operator_noderesize
:
void bdd_operator_noderesize() {
if (cacheratio > 0) {
int newcachesize = bddnodesize / cacheratio;
BddCache_resize(applycache, newcachesize);
...
}
}
Here, if the cache ratio is zero, it is not resized (it stays at the initial fixed size).
Interestingly, we use a *
, while here a /
is used. It seems we invert the meaning of the cache ratio.
The factory interprets it as the number of times that the cache is smaller than the node table, while we interpret it as the fraction of the node table.