dif.pl -- The dif/2 constraint

dif(+Term1, +Term2) is semidet: Constraint that expresses that Term1 and Term2 never become identical (==/2). Fails if Term1 == Term2. Succeeds if Term1 can never become identical to Term2. In other cases the predicate succeeds after attaching constraints to the relevant parts of Term1 and Term2 that prevent the two terms to become identical.
dif_c_c(+X, +Y, !OrNode)[private]: Enforce dif(X,Y) that is related to the given OrNode. If X and Y are equal we reduce the OrNode. If they cannot unify we are done. Otherwise we extend the OrNode with new pairs and create/extend the vardif/2 terms for the left hand side of the unifier as well as the right hand if this is a variable.
dif_c_c_l(+Unifier, +OrNode)[private]: Combine the incoming unifier with the OrNode's current pending set, then recompute the most-general unifier for the whole using unifiable/3 over the accumulated left- and right-hand-side lists. That gives canonical propagation and avoids the infinite oscillation pair-wise simplification hits on cyclic terms.
Fails if the recomputed set is empty — that means all pending equations are trivially satisfied and thus the original dif/2 terms are equal, so dif/2 must fail. Calls or_succeed/1 when unifiable/3 itself fails: the pending equations can never all hold, so the two terms are definitely unequal and dif/2 is satisfied.
add_ornode(+X, +Y, +OrNode)[private]: Extend the vardif constraints on X and Y with the OrNode.
attr_unify_hook(+VarDif, +Other)[private]: Called after the attributed variable has been unified with Other. Collects every OrNode this variable (and, for a var-var unification, Other) is involved in and recomputes each one's MGU. The rebuild inside dif_c_c_l/2 keeps the OrNode's pending list, this variable's vardif and Other's vardif consistent — the current bindings show through variable dereferencing when eqs_lefts_rights/3 walks the pending list.
or_succeed(+OrNode) is det[private]: The dif/2 constraint related to OrNode is complete, i.e., some (sub)terms can definitely not become equal. Next, we can clean up the constraints. We do so by setting the OrNode to - and remove this dead OrNode from every vardif/2 attribute we can find.
or_one_fail(+OrNode) is semidet[private]: Recompute the MGU for OrNode's pending set without adding any new equations. Fails when the set becomes empty (dif/2 fails).