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-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).   43
   44/** <module> The dif/2 constraint
   45*/
   46
   47%!  dif(+Term1, +Term2) is semidet.
   48%
   49%   Constraint that expresses that  Term1   and  Term2  never become
   50%   identical (==/2). Fails if `Term1 ==   Term2`. Succeeds if Term1
   51%   can  never  become  identical  to  Term2.  In  other  cases  the
   52%   predicate succeeds after attaching constraints   to the relevant
   53%   parts of Term1 and Term2 that prevent   the  two terms to become
   54%   identical.
   55
   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    ).
   96
   97%!  dif_c_c(+X,+Y,!OrNode)
   98%
   99%   Enforce dif(X,Y) that is related to the given OrNode. If X and Y are
  100%   equal we reduce the OrNode.  If  they   cannot  unify  we  are done.
  101%   Otherwise we extend the OrNode with  new pairs and create/extend the
  102%   vardif/2 terms for the left hand side of  the unifier as well as the
  103%   right hand if this is a variable.
  104
  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).
  119
  120
  121%!  dif_c_c_l(+Unifier, +OrNode)
  122%
  123%   Extend OrNode with new elements from the   unifier.  Note that it is
  124%   possible that a unification against the   same variable appears as a
  125%   result of how unifiable acts on  sharing subterms. This is prevented
  126%   by block_contradictions/1.
  127%
  128%   @see test 14 in src/Tests/attvar/test_dif.pl.
  129
  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).
  152
  153%!  add_ornode(+X, +Y, +OrNode)
  154%
  155%   Extend the vardif constraints on X and Y with the OrNode.
  156
  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    ).
  177
  178%!  simplify_ornode(+OrNode) is semidet.
  179%
  180%   Simplify the possible unifications left on the original dif/2 terms.
  181%   There are two reasons for simplification. First   of all, due to the
  182%   way unifiable works we may end up with variables in the unifier that
  183%   do not refer to the original terms,   but  to variables in subterms,
  184%   e.g. `[V1 = f(a, V2), V2 = b]`.   As a result of subsequent unifying
  185%   variables, the unifier may end up   having  multiple entries for the
  186%   same variable, possibly having different values, e.g.,  `[X = a, X =
  187%   b]`.  As  these  can  never  be  satified  both  we  have  prove  of
  188%   inequality.
  189%
  190%   Finally, we remove elements from the list that have become equal. If
  191%   the OrNode is empty, the original terms   are equal and thus we must
  192%   fail.
  193
  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).
  222
  223
  224%!  attr_unify_hook(+VarDif, +Other)
  225%
  226%   If two dif/2 variables are unified  we   must  join the two vardif/2
  227%   terms. To do so, we filter the vardif terms for the ones involved in
  228%   this unification. Those that  are  represent   OrNodes  that  have a
  229%   unification satisfied. For the rest we  remove the unifications with
  230%   _self_, append them and use this as new vardif term.
  231%
  232%   On unification with a value, we recursively call dif_c_c/3 using the
  233%   existing OrNodes.
  234
  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    ->  put_attr(Other, dif, vardif(V1,V2))
  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).
  282
  283%!  or_succeed(+OrNode) is det.
  284%
  285%   The dif/2 constraint related  to  OrNode   is  complete,  i.e., some
  286%   (sub)terms can definitely not become equal.   Next,  we can clean up
  287%   the constraints. We do so by setting   the  OrNode to `-` and remove
  288%   this _dead_ OrNode from every vardif/2 attribute we can find.
  289
  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).
  324
  325
  326%!  or_one_fail(+OrNode) is semidet.
  327%
  328%   Some unification related to OrNode succeeded.   We can decrement the
  329%   `Count` of the OrNode. If this  reaches   0,  the original terms are
  330%   equal and we must fail.
  331
  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)