Unifier

Whether this Substitution is a failed one

Whether this Substitution is a successful one (i.e., a Unifier)

Applies this Substitution to the given Term, returning null if it is Substitution.Fail

Casts the current Substitution to Fail, if possible, or returns null otherwise

Casts the current Substitution to Unifier, if possible, or returns null otherwise

Conversion from a raw Map<Var, Term> to the Substitution.Unifier type

Casts the current Substitution to Fail, if possible

Casts the current Substitution to Unifier, if possible

Returns a new substitution containing all key-value pairs matching the given predicate.

Returns a new substitution containing all key-value pairs whose key is in variables.

Retrieves the Term bound to the (first) Var whose Var.name equals name, or null if none is found.

Retrieves the original variable name of the provided variable, if any, or null otherwise

Returns a new substitution containing all entries of the original substitution except those entries which variable keys are contained in the given other substitution.

Returns a new substitution without the entry (if any) for variable.

Returns a new substitution containing all entries of the original substitution except those entries which variable keys are contained in the given keys iterable.

Returns a new substitution without the entries (if any) for variable and otherVariables.

Creates a new Substitution that is the composition (a.k.a. union) of this and other. The composition is not guaranteed to be a Substitution.Unifier, even if both arguments are. In fact, the composition algorithm performs the following checks:

Dispatches on the concrete type of this Substitution, invoking unifier if it is a Unifier, fail if it is a Fail, or otherwise if the relevant callback was not provided (null).