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-2016, K.U.Leuven
    7    All rights reserved.
    8
    9    Redistribution and use in source and binary forms, with or without
   10    modification, are permitted provided that the following conditions
   11    are met:
   12
   13    1. Redistributions of source code must retain the above copyright
   14       notice, this list of conditions and the following disclaimer.
   15
   16    2. Redistributions in binary form must reproduce the above copyright
   17       notice, this list of conditions and the following disclaimer in
   18       the documentation and/or other materials provided with the
   19       distribution.
   20
   21    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   22    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   23    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   24    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   25    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   26    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   27    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   28    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   29    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   30    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   31    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   32    POSSIBILITY OF SUCH DAMAGE.
   33*/
   34
   35:- module(dif,
   36          [ dif/2                               % +Term1, +Term2
   37          ]).   38:- use_module(library(lists)).   39:- set_prolog_flag(generate_debug_info, false).

 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.

   53dif(X,Y) :-
   54    X \== Y,
   55    dif_c_c(X,Y,_).
   56
   57dif_unifiable(X, Y, Us) :-
   58    (    current_prolog_flag(occurs_check, error) ->
   59         catch(unifiable(X,Y,Us), error(occurs_check(_,_),_), false)
   60    ;    unifiable(X, Y, Us)
   61    ).
   62
   63dif_c_c(X,Y,OrNode) :-
   64    (       dif_unifiable(X, Y, Unifier) ->
   65            ( Unifier == [] ->
   66                    or_one_fail(OrNode)
   67            ;
   68                    dif_c_c_l(Unifier,OrNode)
   69            )
   70    ;
   71            or_succeed(OrNode)
   72    ).
   73
   74
   75dif_c_c_l(Unifier,OrNode) :-
   76    length(Unifier,N),
   77    extend_ornode(OrNode,N,List,Tail),
   78    dif_c_c_l_aux(Unifier,OrNode,List,Tail).
   79
   80extend_ornode(OrNode,N,List,Vars) :-
   81    ( get_attr(OrNode,dif,Attr) ->
   82            Attr = node(M,Vars),
   83            O is N + M - 1
   84    ;
   85            O = N,
   86            Vars = []
   87    ),
   88    put_attr(OrNode,dif,node(O,List)).
   89
   90dif_c_c_l_aux([],_,List,List).
   91dif_c_c_l_aux([X=Y|Unifier],OrNode,List,Tail) :-
   92    List = [X=Y|Rest],
   93    add_ornode(X,Y,OrNode),
   94    dif_c_c_l_aux(Unifier,OrNode,Rest,Tail).
   95
   96add_ornode(X,Y,OrNode) :-
   97    add_ornode_var1(X,Y,OrNode),
   98    ( var(Y) ->
   99            add_ornode_var2(X,Y,OrNode)
  100    ;
  101            true
  102    ).
  103
  104add_ornode_var1(X,Y,OrNode) :-
  105    ( get_attr(X,dif,Attr) ->
  106            Attr = vardif(V1,V2),
  107            put_attr(X,dif,vardif([OrNode-Y|V1],V2))
  108    ;
  109            put_attr(X,dif,vardif([OrNode-Y],[]))
  110    ).
  111
  112add_ornode_var2(X,Y,OrNode) :-
  113    ( get_attr(Y,dif,Attr) ->
  114            Attr = vardif(V1,V2),
  115            put_attr(Y,dif,vardif(V1,[OrNode-X|V2]))
  116    ;
  117            put_attr(Y,dif,vardif([],[OrNode-X]))
  118    ).
  119
  120attr_unify_hook(vardif(V1,V2),Other) :-
  121    ( var(Other) ->
  122            reverse_lookups(V1,Other,OrNodes1,NV1),
  123            or_one_fails(OrNodes1),
  124            get_attr(Other,dif,OAttr),
  125            OAttr = vardif(OV1,OV2),
  126            reverse_lookups(OV1,Other,OrNodes2,NOV1),
  127            or_one_fails(OrNodes2),
  128            remove_obsolete(V2,Other,NV2),
  129            remove_obsolete(OV2,Other,NOV2),
  130            append(NV1,NOV1,CV1),
  131            append(NV2,NOV2,CV2),
  132            ( CV1 == [], CV2 == [] ->
  133                    del_attr(Other,dif)
  134            ;
  135                    put_attr(Other,dif,vardif(CV1,CV2))
  136            )
  137    ;
  138            verify_compounds(V1,Other),
  139            verify_compounds(V2,Other)
  140    ).
  141
  142remove_obsolete([], _, []).
  143remove_obsolete([N-Y|T], X, L) :-
  144    (   Y==X ->
  145        remove_obsolete(T, X, L)
  146    ;   L=[N-Y|RT],
  147        remove_obsolete(T, X, RT)
  148    ).
  149
  150reverse_lookups([],_,[],[]).
  151reverse_lookups([N-X|NXs],Value,Nodes,Rest) :-
  152    ( X == Value ->
  153            Nodes = [N|RNodes],
  154            Rest = RRest
  155    ;
  156            Nodes = RNodes,
  157            Rest = [N-X|RRest]
  158    ),
  159    reverse_lookups(NXs,Value,RNodes,RRest).
  160
  161verify_compounds([],_).
  162verify_compounds([OrNode-Y|Rest],X) :-
  163    ( var(Y) ->
  164            true
  165    ; OrNode == (-) ->
  166            true
  167    ;
  168            dif_c_c(X,Y,OrNode)
  169    ),
  170    verify_compounds(Rest,X).
  171
  172%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  173or_succeed(OrNode) :-
  174    ( attvar(OrNode) ->
  175            get_attr(OrNode,dif,Attr),
  176            Attr = node(_Counter,Pairs),
  177            del_attr(OrNode,dif),
  178            OrNode = (-),
  179            del_or_dif(Pairs)
  180    ;
  181            true
  182    ).
  183
  184or_one_fails([]).
  185or_one_fails([N|Ns]) :-
  186    or_one_fail(N),
  187    or_one_fails(Ns).
  188
  189or_one_fail(OrNode) :-
  190    ( attvar(OrNode) ->
  191            get_attr(OrNode,dif,Attr),
  192            Attr = node(Counter,Pairs),
  193            NCounter is Counter - 1,
  194            ( NCounter == 0 ->
  195                    fail
  196            ;
  197                    put_attr(OrNode,dif,node(NCounter,Pairs))
  198            )
  199    ;
  200            fail
  201    ).
  202
  203del_or_dif([]).
  204del_or_dif([X=Y|Xs]) :-
  205    cleanup_dead_nodes(X),
  206    cleanup_dead_nodes(Y),
  207    del_or_dif(Xs).
  208
  209cleanup_dead_nodes(X) :-
  210    ( attvar(X) ->
  211            get_attr(X,dif,Attr),
  212            Attr = vardif(V1,V2),
  213            filter_dead_ors(V1,NV1),
  214            filter_dead_ors(V2,NV2),
  215            ( NV1 == [], NV2 == [] ->
  216                    del_attr(X,dif)
  217            ;
  218                    put_attr(X,dif,vardif(NV1,NV2))
  219            )
  220    ;
  221            true
  222    ).
  223
  224filter_dead_ors([],[]).
  225filter_dead_ors([Or-Y|Rest],List) :-
  226    ( var(Or) ->
  227            List = [Or-Y|NRest]
  228    ;
  229            List = NRest
  230    ),
  231    filter_dead_ors(Rest,NRest).
  232
  233/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  234   The attribute of a variable X is vardif/2. The first argument is a
  235   list of pairs. The first component of each pair is an OrNode. The
  236   attribute of each OrNode is node/2. The second argument of node/2
  237   is a list of equations A = B. If the LHS of the first equation is
  238   X, then return a goal, otherwise don't because someone else will.
  239- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
  240
  241attribute_goals(Var) -->
  242    (   { get_attr(Var, dif, vardif(Ors,_)) } ->
  243        or_nodes(Ors, Var)
  244    ;   or_node(Var)
  245    ).
  246
  247or_node(O) -->
  248    (   { get_attr(O, dif, node(_, Pairs)) } ->
  249        { eqs_lefts_rights(Pairs, As, Bs) },
  250        mydif(As, Bs),
  251        { del_attr(O, dif) }
  252    ;   []
  253    ).
  254
  255or_nodes([], _)       --> [].
  256or_nodes([O-_|Os], X) -->
  257    (   { get_attr(O, dif, node(_, Eqs)) } ->
  258        (   { Eqs = [LHS=_|_], LHS == X } ->
  259            { eqs_lefts_rights(Eqs, As, Bs) },
  260            mydif(As, Bs),
  261            { del_attr(O, dif) }
  262        ;   []
  263        )
  264    ;   [] % or-node already removed
  265    ),
  266    or_nodes(Os, X).
  267
  268mydif([X], [Y]) --> !, dif_if_necessary(X, Y).
  269mydif(Xs0, Ys0) -->
  270    { reverse(Xs0, Xs), reverse(Ys0, Ys), % follow original order
  271      X =.. [f|Xs], Y =.. [f|Ys] },
  272    dif_if_necessary(X, Y).
  273
  274dif_if_necessary(X, Y) -->
  275    (   { dif_unifiable(X, Y, _) } ->
  276        [dif(X,Y)]
  277    ;   []
  278    ).
  279
  280eqs_lefts_rights([], [], []).
  281eqs_lefts_rights([A=B|ABs], [A|As], [B|Bs]) :-
  282    eqs_lefts_rights(ABs, As, Bs)