-
Notifications
You must be signed in to change notification settings - Fork 7
Description
By default JFactory#FLUSH_CACHE_ON_GC is true, meaning that the operation cache is flushed every time GC is invoked. By setting FLUSH_CACHE_ON_GC to false, JavaBDD will instead perform cache cleanup, which preserves all cache entries whose BDDs are not garbage collected. However, cache cleanup does not correctly consider certain cache entries. For example, the instance and current fields of saturation related cache entries are handled as if they were BDDs, meaning that valid cache entries may be deleted. Moreover, the BddCacheDataI#d and BddCacheDataI#e fields are not considered at all, while they are used by relnextUnion/relnextIntersection/relprevUnion/relprevIntersection. Hence invalid cache entries might be kept. Cache cleanup should thus be fixed.