View source with formatted 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-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).   42
   43/** <module> The dif/2 constraint
   44*/
   45
   46%!  dif(+Term1, +Term2) is semidet.
   47%
   48%   Constraint that expresses that  Term1   and  Term2  never become
   49%   identical (==/2). Fails if `Term1 ==   Term2`. Succeeds if Term1
   50%   can  never  become  identical  to  Term2.  In  other  cases  the
   51%   predicate succeeds after attaching constraints   to the relevant
   52%   parts of Term1 and Term2 that prevent   the  two terms to become
   53%   identical.
   54
   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        ;   dif_c_c_l(Unifier,OrNode)
   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    ;   O = N,
   85        Vars = []
   86    ),
   87    put_attr(OrNode,dif,node(O,List)).
   88
   89dif_c_c_l_aux([],_,List,List).
   90dif_c_c_l_aux([X=Y|Unifier],OrNode,List,Tail) :-
   91    List = [X=Y|Rest],
   92    add_ornode(X,Y,OrNode),
   93    dif_c_c_l_aux(Unifier,OrNode,Rest,Tail).
   94
   95add_ornode(X,Y,OrNode) :-
   96    add_ornode_var1(X,Y,OrNode),
   97    (   var(Y)
   98    ->  add_ornode_var2(X,Y,OrNode)
   99    ;   true
  100    ).
  101
  102add_ornode_var1(X,Y,OrNode) :-
  103    (   get_attr(X,dif,Attr)
  104    ->  Attr = vardif(V1,V2),
  105        put_attr(X,dif,vardif([OrNode-Y|V1],V2))
  106    ;   put_attr(X,dif,vardif([OrNode-Y],[]))
  107    ).
  108
  109add_ornode_var2(X,Y,OrNode) :-
  110    (   get_attr(Y,dif,Attr)
  111    ->  Attr = vardif(V1,V2),
  112        put_attr(Y,dif,vardif(V1,[OrNode-X|V2]))
  113    ;   put_attr(Y,dif,vardif([],[OrNode-X]))
  114    ).
  115
  116attr_unify_hook(vardif(V1,V2),Other) :-
  117    (   var(Other)
  118    ->  reverse_lookups(V1,Other,OrNodes1,NV1),
  119        or_one_fails(OrNodes1),
  120        get_attr(Other,dif,OAttr),
  121        OAttr = vardif(OV1,OV2),
  122        reverse_lookups(OV1,Other,OrNodes2,NOV1),
  123        or_one_fails(OrNodes2),
  124        remove_obsolete(V2,Other,NV2),
  125        remove_obsolete(OV2,Other,NOV2),
  126        append(NV1,NOV1,CV1),
  127        append(NV2,NOV2,CV2),
  128        (   CV1 == [], CV2 == []
  129        ->  del_attr(Other,dif)
  130        ;   put_attr(Other,dif,vardif(CV1,CV2))
  131        )
  132    ;   verify_compounds(V1,Other),
  133        verify_compounds(V2,Other)
  134    ).
  135
  136remove_obsolete([], _, []).
  137remove_obsolete([N-Y|T], X, L) :-
  138    (   Y==X
  139    ->  remove_obsolete(T, X, L)
  140    ;   L=[N-Y|RT],
  141        remove_obsolete(T, X, RT)
  142    ).
  143
  144reverse_lookups([],_,[],[]).
  145reverse_lookups([N-X|NXs],Value,Nodes,Rest) :-
  146    (   X == Value
  147    ->  Nodes = [N|RNodes],
  148        Rest = RRest
  149    ;   Nodes = RNodes,
  150        Rest = [N-X|RRest]
  151    ),
  152    reverse_lookups(NXs,Value,RNodes,RRest).
  153
  154verify_compounds([],_).
  155verify_compounds([OrNode-Y|Rest],X) :-
  156    (   var(Y)
  157    ->  true
  158    ;   OrNode == (-)
  159    ->  true
  160    ;   dif_c_c(X,Y,OrNode)
  161    ),
  162    verify_compounds(Rest,X).
  163
  164%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  165or_succeed(OrNode) :-
  166    (   attvar(OrNode)
  167    ->  get_attr(OrNode,dif,Attr),
  168        Attr = node(_Counter,Pairs),
  169        del_attr(OrNode,dif),
  170        OrNode = (-),
  171        del_or_dif(Pairs)
  172    ;   true
  173    ).
  174
  175or_one_fails([]).
  176or_one_fails([N|Ns]) :-
  177    or_one_fail(N),
  178    or_one_fails(Ns).
  179
  180or_one_fail(OrNode) :-
  181    (   attvar(OrNode)
  182    ->  get_attr(OrNode,dif,Attr),
  183        Attr = node(Counter,Pairs),
  184        NCounter is Counter - 1,
  185        (   NCounter == 0
  186        ->  fail
  187        ;   put_attr(OrNode,dif,node(NCounter,Pairs))
  188        )
  189    ;   fail
  190    ).
  191
  192del_or_dif([]).
  193del_or_dif([X=Y|Xs]) :-
  194    cleanup_dead_nodes(X),
  195    cleanup_dead_nodes(Y),
  196    del_or_dif(Xs).
  197
  198cleanup_dead_nodes(X) :-
  199    (   attvar(X)
  200    ->  get_attr(X,dif,Attr),
  201        Attr = vardif(V1,V2),
  202        filter_dead_ors(V1,NV1),
  203        filter_dead_ors(V2,NV2),
  204        (   NV1 == [], NV2 == []
  205        ->  del_attr(X,dif)
  206        ;   put_attr(X,dif,vardif(NV1,NV2))
  207        )
  208    ;   true
  209    ).
  210
  211filter_dead_ors([],[]).
  212filter_dead_ors([Or-Y|Rest],List) :-
  213    (   var(Or)
  214    ->  List = [Or-Y|NRest]
  215    ;   List = NRest
  216    ),
  217    filter_dead_ors(Rest,NRest).
  218
  219/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  220   The attribute of a variable X is vardif/2. The first argument is a
  221   list of pairs. The first component of each pair is an OrNode. The
  222   attribute of each OrNode is node/2. The second argument of node/2
  223   is a list of equations A = B. If the LHS of the first equation is
  224   X, then return a goal, otherwise don't because someone else will.
  225- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
  226
  227attribute_goals(Var) -->
  228    (   { get_attr(Var, dif, vardif(Ors,_)) }
  229    ->  or_nodes(Ors, Var)
  230    ;   or_node(Var)
  231    ).
  232
  233or_node(O) -->
  234    (   { get_attr(O, dif, node(_, Pairs)) }
  235    ->  { eqs_lefts_rights(Pairs, As, Bs) },
  236        mydif(As, Bs),
  237        { del_attr(O, dif) }
  238    ;   []
  239    ).
  240
  241or_nodes([], _)       --> [].
  242or_nodes([O-_|Os], X) -->
  243    (   { get_attr(O, dif, node(_, Eqs)) }
  244    ->  (   { Eqs = [LHS=_|_], LHS == X }
  245        ->  { eqs_lefts_rights(Eqs, As, Bs) },
  246            mydif(As, Bs),
  247            { del_attr(O, dif) }
  248        ;   []
  249        )
  250    ;   [] % or-node already removed
  251    ),
  252    or_nodes(Os, X).
  253
  254mydif([X], [Y]) --> !, dif_if_necessary(X, Y).
  255mydif(Xs0, Ys0) -->
  256    { reverse(Xs0, Xs), reverse(Ys0, Ys), % follow original order
  257      X =.. [f|Xs], Y =.. [f|Ys]
  258    },
  259    dif_if_necessary(X, Y).
  260
  261dif_if_necessary(X, Y) -->
  262    (   { dif_unifiable(X, Y, _) }
  263    ->  [dif(X,Y)]
  264    ;   []
  265    ).
  266
  267eqs_lefts_rights([], [], []).
  268eqs_lefts_rights([A=B|ABs], [A|As], [B|Bs]) :-
  269    eqs_lefts_rights(ABs, As, Bs)