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:- autoload(library(lists),[append/3,reverse/2]).   39
   40
   41:- 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.

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