Package-level declarations

Skeletal Unificator implementation, providing a complete, equation-based unification algorithm (in the style of Martelli & Montanari's): both mgu and merge repeatedly decompose their operands into Equations and simplify them (structurally comparing Terms, applying resulting variable assignments to the remaining equations) until either a contradiction is found (failure) or no equation can be simplified further (success).

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.

An equation between two logic Terms, lhs = rhs, as built and progressively simplified while computing a Substitution (see AbstractUnificator).

Marks a type that carries its own Unificator, to be used whenever unification is needed in that context (e.g. an execution/solving context choosing which unification strategy governs its resolution).

Unifies pairs of Terms, computing the most general unifier (MGU) that makes them syntactically equal, if any exists.

Creates an Equation with this as left-hand side and that as right-hand side (see Equation.of).

Transforms this Substitution's bindings into the equivalent list of Equation.LeftAssignments.

Creates a Substitution out of an Iterable of Equations, each assigning a Var to a Term (see Equation.toAssignmentPair). Returns Substitution.failed if two equations disagree on the same Var's binding.