cached

fun cached(other: Unificator, capacity: Int = DEFAULT_CACHE_CAPACITY): Unificator

Decorates other so that its most recently computed Unificator.mgu/Unificator.merge results (and, transitively, Unificator.match/Unificator.unify, which are defined in terms of Unificator.mgu) are memoized in an LRU cache, avoiding recomputation for repeated requests with the same arguments.

If other is already a CachedUnificator, its underlying (non-cached) Unificator is re-wrapped with the new capacity instead of double-caching.

Return

a decorated, cached Unificator

Parameters

other

the Unificator to be made cached

capacity

the maximum amount of entries the cache may store