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-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).
  40
  41/** <module> The dif/2 constraint
  42*/
  43
  44%!  dif(+Term1, +Term2) is semidet.
  45%
  46%   Constraint that expresses that  Term1   and  Term2  never become
  47%   identical (==/2). Fails if `Term1 ==   Term2`. Succeeds if Term1
  48%   can  never  become  identical  to  Term2.  In  other  cases  the
  49%   predicate succeeds after attaching constraints   to the relevant
  50%   parts of Term1 and Term2 that prevent   the  two terms to become
  51%   identical.
  52
  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).