View source with raw comments or as raw
    1/*  Part of SWI-Prolog
    2
    3    Author:        Tom Schrijvers, Markus Triska and Jan Wielemaker
    4    E-mail:        Tom.Schrijvers@cs.kuleuven.ac.be
    5    WWW:           http://www.swi-prolog.org
    6    Copyright (c)  2004-2021, K.U.Leuven
    7                              SWI-Prolog Solutions b.v.
    8    All rights reserved.
    9
   10    Redistribution and use in source and binary forms, with or without
   11    modification, are permitted provided that the following conditions
   12    are met:
   13
   14    1. Redistributions of source code must retain the above copyright
   15       notice, this list of conditions and the following disclaimer.
   16
   17    2. Redistributions in binary form must reproduce the above copyright
   18       notice, this list of conditions and the following disclaimer in
   19       the documentation and/or other materials provided with the
   20       distribution.
   21
   22    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   23    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   24    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   25    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   26    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   27    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   28    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   29    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   30    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   31    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   32    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   33    POSSIBILITY OF SUCH DAMAGE.
   34*/
   35
   36:- module(dif,
   37          [ dif/2                               % +Term1, +Term2
   38          ]).   39:- autoload(library(lists),[append/3,reverse/2]).   40
   41
   42:- set_prolog_flag(generate_debug_info, false).

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.
   56dif(X,Y) :-
   57    ?=(X,Y),
   58    !,
   59    X \== Y.
   60dif(X,Y) :-
   61    dif_c_c(X,Y,_).
   62
   63/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   64The constraint is helt in  an   attribute  `dif`. A constrained variable
   65holds a term  vardif(L1,L2)  where  `L1`   is  a  list  OrNode-Value for
   66constraints on this variable  and  `L2`   is  the  constraint list other
   67variables have on me.
   68
   69The `OrNode` is a term node(Pairs), where `Pairs` is a of list Var=Value
   70terms representing the pending unifications. The  original dif/2 call is
   71represented by a single OrNode.
   72
   73If a unification related to an  OrNode   fails  the terms are definitely
   74unequal and thus we can kill all   pending constraints and succeed. If a
   75unequal related to an OrNode succeeds we   decrement  the `Count` of the
   76node. If the count  reaches  0  all   unifications  of  the  OrNode have
   77succeeded, the original terms are equal and thus we need to fail.
   78
   79The following invariants must hold
   80
   81  - Any variable involved in a dif/2 constraint has an attribute
   82    vardif(L1,L2), Where each element of both lists is a term
   83    OrNode-Value, L1 represents the values this variable may __not__
   84    become equal to and L2 represents this variable involved in other
   85    constraints.  I.e, L2 is only used if a dif/2 requires two variables
   86    to be different.
   87  - An OrNode has an attribute node(Pairs), where Pairs contains the
   88    possible unifications.
   89- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
   90
   91dif_unifiable(X, Y, Us) :-
   92    (    current_prolog_flag(occurs_check, error)
   93    ->   catch(unifiable(X,Y,Us), error(occurs_check(_,_),_), false)
   94    ;    unifiable(X, Y, Us)
   95    ).
 dif_c_c(+X, +Y, !OrNode)
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.
  105dif_c_c(X,Y,OrNode) :-
  106    (   dif_unifiable(X, Y, Unifier)
  107    ->  (   Unifier == []
  108        ->  or_one_fail(OrNode)
  109        ;   dif_c_c_l(Unifier,OrNode, U),
  110            subunifier(U, OrNode)
  111        )
  112    ;   or_succeed(OrNode)
  113    ).
  114
  115subunifier([], _).
  116subunifier([X=Y|T], OrNode) :-
  117    dif_c_c(X, Y, OrNode),
  118    subunifier(T, OrNode).
 dif_c_c_l(+Unifier, +OrNode)
Extend OrNode with new elements from the unifier. Note that it is possible that a unification against the same variable appears as a result of how unifiable acts on sharing subterms. This is prevented by block_contradictions/1.
See also
- test 14 in src/Tests/attvar/test_dif.pl.
  130dif_c_c_l(Unifier, OrNode, U) :-
  131    extend_ornode(OrNode, List, Tail),
  132    dif_c_c_l_aux(Unifier, OrNode, List0, Tail),
  133    (   simplify_ornode(List0, List, U)
  134    ->  true
  135    ;   List = List0,
  136        or_succeed(OrNode),
  137        U = []
  138    ).
  139
  140extend_ornode(OrNode, List, Vars) :-
  141    (   get_attr(OrNode, dif, node(Vars))
  142    ->  true
  143    ;   Vars = []
  144    ),
  145    put_attr(OrNode,dif,node(List)).
  146
  147dif_c_c_l_aux([],_,List,List).
  148dif_c_c_l_aux([X=Y|Unifier],OrNode,List,Tail) :-
  149    List = [X=Y|Rest],
  150    add_ornode(X,Y,OrNode),
  151    dif_c_c_l_aux(Unifier,OrNode,Rest,Tail).
 add_ornode(+X, +Y, +OrNode)
Extend the vardif constraints on X and Y with the OrNode.
  157add_ornode(X,Y,OrNode) :-
  158    add_ornode_var1(X,Y,OrNode),
  159    (   var(Y)
  160    ->  add_ornode_var2(X,Y,OrNode)
  161    ;   true
  162    ).
  163
  164add_ornode_var1(X,Y,OrNode) :-
  165    (   get_attr(X,dif,Attr)
  166    ->  Attr = vardif(V1,V2),
  167        put_attr(X,dif,vardif([OrNode-Y|V1],V2))
  168    ;   put_attr(X,dif,vardif([OrNode-Y],[]))
  169    ).
  170
  171add_ornode_var2(X,Y,OrNode) :-
  172    (   get_attr(Y,dif,Attr)
  173    ->  Attr = vardif(V1,V2),
  174        put_attr(Y,dif,vardif(V1,[OrNode-X|V2]))
  175    ;   put_attr(Y,dif,vardif([],[OrNode-X]))
  176    ).
 simplify_ornode(+OrNode) is semidet
Simplify the possible unifications left on the original dif/2 terms. There are two reasons for simplification. First of all, due to the way unifiable works we may end up with variables in the unifier that do not refer to the original terms, but to variables in subterms, e.g. [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.

  194simplify_ornode(OrNode) :-
  195    (   get_attr(OrNode, dif, node(Pairs0))
  196    ->  simplify_ornode(Pairs0, Pairs, U),
  197        Pairs \== [],
  198        put_attr(OrNode, dif, node(Pairs)),
  199        subunifier(U, OrNode)
  200    ;   true
  201    ).
  202
  203simplify_ornode(List0, List, U) :-
  204    sort(1, @=<, List0, Sorted),
  205    simplify_ornode_(Sorted, List, U).
  206
  207simplify_ornode_([], List, U) =>
  208    List = [],
  209    U = [].
  210simplify_ornode_([Var=Val1,Var=Val2|T], List, U), var(Var) =>
  211    (   ?=(Val1, Val2)
  212    ->  Val1 == Val2,
  213        simplify_ornode_([Var=Val2|T], List, U)
  214    ;   U = [Val1=Val2|UT],
  215        simplify_ornode_([Var=Val2|T], List, UT)
  216    ).
  217simplify_ornode_([V1=V2|T], List, U), V1 == V2 =>
  218    simplify_ornode_(T, List, U).
  219simplify_ornode_([H|T], List, U) =>
  220    List = [H|Rest],
  221    simplify_ornode_(T, Rest, U).
 attr_unify_hook(+VarDif, +Other)
If two dif/2 variables are unified we must join the two vardif/2 terms. To do so, we filter the vardif terms for the ones involved in this unification. Those that are represent OrNodes that have a unification satisfied. For the rest we remove the unifications with self, append them and use this as new vardif term.

On unification with a value, we recursively call dif_c_c/3 using the existing OrNodes.

  235attr_unify_hook(vardif(V1,V2),Other) :-
  236    (   get_attr(Other, dif, vardif(OV1,OV2))
  237    ->  reverse_lookups(V1, Other, OrNodes1, NV1),
  238        or_one_fails(OrNodes1),
  239        reverse_lookups(OV1, Other, OrNodes2, NOV1),
  240        or_one_fails(OrNodes2),
  241        remove_obsolete(V2, Other, NV2),
  242        remove_obsolete(OV2, Other, NOV2),
  243        append(NV1, NOV1, CV1),
  244        append(NV2, NOV2, CV2),
  245        (   CV1 == [], CV2 == []
  246        ->  del_attr(Other, dif)
  247        ;   put_attr(Other, dif, vardif(CV1,CV2))
  248        )
  249    ;   var(Other)			% unrelated variable
  250    ->  true
  251    ;   verify_compounds(V1, Other),
  252        verify_compounds(V2, Other)
  253    ).
  254
  255remove_obsolete([], _, []).
  256remove_obsolete([N-Y|T], X, L) :-
  257    (   Y==X
  258    ->  remove_obsolete(T, X, L)
  259    ;   L=[N-Y|RT],
  260        remove_obsolete(T, X, RT)
  261    ).
  262
  263reverse_lookups([],_,[],[]).
  264reverse_lookups([N-X|NXs],Value,Nodes,Rest) :-
  265    (   X == Value
  266    ->  Nodes = [N|RNodes],
  267        Rest = RRest
  268    ;   Nodes = RNodes,
  269        Rest = [N-X|RRest]
  270    ),
  271    reverse_lookups(NXs,Value,RNodes,RRest).
  272
  273verify_compounds([],_).
  274verify_compounds([OrNode-Y|Rest],X) :-
  275    (   var(Y)
  276    ->  true
  277    ;   OrNode == (-)
  278    ->  true
  279    ;   dif_c_c(X,Y,OrNode)
  280    ),
  281    verify_compounds(Rest,X).
 or_succeed(+OrNode) is det
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.
  290or_succeed(OrNode) :-
  291    (   get_attr(OrNode,dif,Attr)
  292    ->  Attr = node(Pairs),
  293        del_attr(OrNode,dif),
  294        OrNode = (-),
  295        del_or_dif(Pairs)
  296    ;   true
  297    ).
  298
  299del_or_dif([]).
  300del_or_dif([X=Y|Xs]) :-
  301    cleanup_dead_nodes(X),
  302    cleanup_dead_nodes(Y),              % JW: what about embedded variables?
  303    del_or_dif(Xs).
  304
  305cleanup_dead_nodes(X) :-
  306    (   get_attr(X,dif,Attr)
  307    ->  Attr = vardif(V1,V2),
  308        filter_dead_ors(V1,NV1),
  309        filter_dead_ors(V2,NV2),
  310        (   NV1 == [], NV2 == []
  311        ->  del_attr(X,dif)
  312        ;   put_attr(X,dif,vardif(NV1,NV2))
  313        )
  314    ;   true
  315    ).
  316
  317filter_dead_ors([],[]).
  318filter_dead_ors([Or-Y|Rest],List) :-
  319    (   var(Or)
  320    ->  List = [Or-Y|NRest]
  321    ;   List = NRest
  322    ),
  323    filter_dead_ors(Rest,NRest).
 or_one_fail(+OrNode) is semidet
Some unification related to OrNode succeeded. We can decrement the Count of the OrNode. If this reaches 0, the original terms are equal and we must fail.
  332or_one_fail(OrNode) :-
  333    simplify_ornode(OrNode).
  334
  335or_one_fails([]).
  336or_one_fails([N|Ns]) :-
  337    or_one_fail(N),
  338    or_one_fails(Ns).
  339
  340
  341/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  342   The attribute of a variable X is vardif/2. The first argument is a
  343   list of pairs. The first component of each pair is an OrNode. The
  344   attribute of each OrNode is node/2. The second argument of node/2
  345   is a list of equations A = B. If the LHS of the first equation is
  346   X, then return a goal, otherwise don't because someone else will.
  347- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
  348
  349attribute_goals(Var) -->
  350    (   { get_attr(Var, dif, vardif(Ors,_)) }
  351    ->  or_nodes(Ors, Var)
  352    ;   or_node(Var)
  353    ).
  354
  355or_node(O) -->
  356    (   { get_attr(O, dif, node(Pairs)) }
  357    ->  { eqs_lefts_rights(Pairs, As, Bs) },
  358        mydif(As, Bs),
  359        { del_attr(O, dif) }
  360    ;   []
  361    ).
  362
  363or_nodes([], _)       --> [].
  364or_nodes([O-_|Os], X) -->
  365    (   { get_attr(O, dif, node(Eqs)) }
  366    ->  (   { Eqs = [LHS=_|_], LHS == X }
  367        ->  { eqs_lefts_rights(Eqs, As, Bs) },
  368            mydif(As, Bs),
  369            { del_attr(O, dif) }
  370        ;   []
  371        )
  372    ;   [] % or-node already removed
  373    ),
  374    or_nodes(Os, X).
  375
  376mydif([X], [Y]) --> !, dif_if_necessary(X, Y).
  377mydif(Xs0, Ys0) -->
  378    { reverse(Xs0, Xs), reverse(Ys0, Ys), % follow original order
  379      X =.. [f|Xs], Y =.. [f|Ys]
  380    },
  381    dif_if_necessary(X, Y).
  382
  383dif_if_necessary(X, Y) -->
  384    (   { dif_unifiable(X, Y, _) }
  385    ->  [dif(X,Y)]
  386    ;   []
  387    ).
  388
  389eqs_lefts_rights([], [], []).
  390eqs_lefts_rights([A=B|ABs], [A|As], [B|Bs]) :-
  391    eqs_lefts_rights(ABs, As, Bs)