|Did you know ...||Search Documentation:|
|dif.pl -- The dif/2 constraint|
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(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.
[V1 = f(a, V2), V2 = b]. As a result of subsequent unifying variables, the unifier may end up having multiple entries for the same variable, possibly having different values, e.g.,
[X = a, X = b]. As these can never be satified both we have prove of inequality.
Finally, we remove elements from the list that have become equal. If the OrNode is empty, the original terms are equal and thus we must fail.
On unification with a value, we recursively call dif_c_c/3 using the existing OrNodes.
-and remove this dead OrNode from every vardif/2 attribute we can find.