main

Demonstrates wrapping an it.unibo.tuprolog.unify.Unificator with a memoizing decorator via Unificator.cached.

The cached unificator behaves exactly like the wrapped one (here, it.unibo.tuprolog.unify.Unificator.default) but remembers the outcome of up to capacity distinct unification requests, avoiding recomputing mgu, match and unify calls for term pairs seen before. This is useful when the same unification is likely to be repeated many times during resolution, at the cost of the extra memory needed for the cache.

Running this example prints {X_0=abraham}, true, and father(abraham, isaac), exactly as the uncached it.unibo.tuprolog.unify.Unificator.default would.

Demonstrates defining a custom unification strategy by extending it.unibo.tuprolog.unify.AbstractUnificator and overriding AbstractUnificator.checkTermsEquality, the hook used to decide whether two non-variable, non-compound terms are considered equal.

The custom unificator treats two numeric terms as equal whenever their absolute values match, falling back to plain equality (==) for every other kind of term. As a result, f(1) and f(-1) are found to match even though 1 and -1 are not structurally equal, showing how AbstractUnificator can be extended to implement domain-specific notions of "sameness" beyond standard Prolog unification.

Running this example prints true (the terms match) and f(1) (the unified term, using the value carried by the first argument).

Demonstrates the three ways of asking it.unibo.tuprolog.unify.Unificator.default whether two terms unify, on a case where unification fails.

The struct father(abraham, isaac) is unified against the template father(isaac, abraham): the two constant arguments are swapped, so no substitution can make the two terms equal. Unificator.mgu returns a it.unibo.tuprolog.core.Substitution.Fail (for which Substitution.isFailed is true), Unificator.match returns false, and Unificator.unify returns null. Contrast this with the Success example in this same package, which runs the same three operations on terms that do unify.

Running this example prints true (is a Fail), true (isFailed), false (match), and null (unify).

Demonstrates the infix extension functions mguWith, matches and unifyWith, which offer a term-centric, operator-like syntax over it.unibo.tuprolog.unify.Unificator.default as an alternative to calling mgu/match/unify directly on a Unificator instance.

The same unification performed in the Success example of this package (father(abraham, isaac) against father(X, isaac)) is expressed here as term mguWith template, term matches template and term unifyWith template, which reads more naturally when the default unificator is all that is needed.

Running this example prints {X_0=abraham}, true, and father(abraham, isaac).

Demonstrates why the occurs check matters, by deliberately disabling it via occurCheckEnabled = false on Unificator.mgu.

Unifying g(X, Y) with g(f(X), a) requires binding X to f(X), a term that contains X itself. Standard (sound) unification rejects this as a cyclic, infinite term via the occurs check; here the check is switched off, so the unifier happily returns the unsound binding {X -> f(X), Y -> a}, which is marked WRONG in the inline comment because X occurs in its own binding. This illustrates the soundness/performance trade-off exposed by the occurCheckEnabled parameter: it defaults to true on Unificator.mgu, and only explicitly disabling it (as done here) exposes this kind of unsound, self-referential binding.

Running this example prints {X_0=f(X_0), Y_1=a}.

Demonstrates the three ways of asking it.unibo.tuprolog.unify.Unificator.default whether two terms unify, on a case where unification succeeds.

The struct father(abraham, isaac) is unified against the template father(X, isaac). Since X can be bound to abraham while the rest of the structure matches, unification succeeds: Unificator.mgu returns the most general unifier {X -> abraham}, Unificator.match returns true, and Unificator.unify returns the unified term father(abraham, isaac). Contrast this with the Failure example in this same package, which runs the same three operations on terms that do not unify.

Running this example prints {X_0=abraham}, true, and father(abraham, isaac).