unify/it.unibo.tuprolog.unify/CachedUnificator

CachedUnificator

class CachedUnificator(val decorated: Unificator, cacheCapacity: Int) : Unificator

A Unificator decorator that memoizes the results of mgu and merge calls made on decorated, in a shared LRU cache of at most cacheCapacity entries, so that repeated calls with the same arguments (including the same occurCheckEnabled flag) are served from the cache instead of being recomputed.

Since Unificator.match and Unificator.unify are, by default, defined in terms of Unificator.mgu, they too benefit from the cache transitively — no separate caching is performed for them.

Cache keys are built from term1/term2 (or the two Substitutions, for merge) compared via Term.equals/ Substitution.equals; two structurally equal but distinct term/substitution instances therefore share a cache entry. This class is safe for concurrent use from multiple threads: the underlying cache synchronizes its access.

Instances are normally created through Unificator.cached rather than directly, since that factory also avoids double-wrapping an already-cached Unificator.

Parameters

decorated

the Unificator whose results are being cached

cacheCapacity

the maximum number of entries the LRU cache may hold, shared between mgu and merge

Constructors

CachedUnificator

constructor(decorated: Unificator, cacheCapacity: Int)

Properties

context

open override val context: Substitution

Delegates to decorated's context.

decorated

val decorated: Unificator

Functions

match

open fun match(term1: Term, term2: Term): Boolean

Tells whether term1 and term2 match each other, that is, whether mgu would succeed for them. Performs unification with occurs-check enabled.

open fun match(term1: Term, term2: Term, occurCheckEnabled: Boolean): Boolean

Tells whether term1 and term2 match each other, that is, whether mgu would succeed for them, optionally enabling occurs-check.

merge

open override fun merge(substitution1: Substitution, substitution2: Substitution, occurCheckEnabled: Boolean): Substitution

Returns the cached result for (substitution1, substitution2, occurCheckEnabled), computing and caching it if absent. Shares the same underlying LRU cache (and thus the same cacheCapacity budget) as mgu.

open fun merge(substitution1: Substitution, substitution2: Substitution): Substitution

Merges substitution1 and substitution2, with occurs-check enabled.

mgu

open override fun mgu(term1: Term, term2: Term, occurCheckEnabled: Boolean = true): Substitution

Returns the cached result for (term1, term2, occurCheckEnabled), computing and caching it if absent.

open fun mgu(term1: Term, term2: Term): Substitution

Calculates the Most General Unifier of term1 and term2, with occurs-check enabled.

unify

open fun unify(term1: Term, term2: Term): Term?

Unifies term1 and term2 if possible, with occurs-check enabled.

open fun unify(term1: Term, term2: Term, occurCheckEnabled: Boolean): Term?

Unifies term1 and term2 if possible, optionally enabling occurs-check.