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-2023, 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).
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.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 remove it from the node. If the 76node becomes empty the terms are equal and we must fail. 77 78The following invariants must hold 79 80 - Any variable involved in a dif/2 constraint has an attribute 81 vardif(L1,L2), Where each element of both lists is a term 82 OrNode-Value, L1 represents the values this variable may __not__ 83 become equal to and L2 represents this variable involved in other 84 constraints. I.e, L2 is only used if a dif/2 requires two variables 85 to be different. 86 - An OrNode has an attribute node(Pairs), where Pairs contains the 87 possible unifications. 88- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ 89 90dif_unifiable(X, Y, Us) :- 91 ( current_prolog_flag(occurs_check, error) 92 -> catch(unifiable(X,Y,Us), error(occurs_check(_,_),_), false) 93 ; unifiable(X, Y, Us) 94 ).
dif(X,Y) that is related to the given OrNode. If X and Y are
equal we reduce the OrNode. If they cannot unify we are done.
Otherwise we extend the OrNode with new pairs and create/extend the
vardif/2 terms for the left hand side of the unifier as well as the
right hand if this is a variable.
104dif_c_c(X,Y,OrNode) :-
105 ( dif_unifiable(X, Y, Unifier)
106 -> ( Unifier == []
107 -> or_one_fail(OrNode)
108 ; dif_c_c_l(Unifier, OrNode)
109 )
110 ; or_succeed(OrNode)
111 ).Fails if the recomputed set is empty — that means all pending equations are trivially satisfied and thus the original dif/2 terms are equal, so dif/2 must fail. Calls or_succeed/1 when unifiable/3 itself fails: the pending equations can never all hold, so the two terms are definitely unequal and dif/2 is satisfied.
128dif_c_c_l(_Unifier, OrNode) :- 129 nonvar(OrNode), % dead (or_succeed'd) node 130 !. 131dif_c_c_l(Unifier, OrNode) :- 132 ( get_attr(OrNode, dif, node(OldPairs)) 133 -> true 134 ; OldPairs = [] 135 ), 136 append(Unifier, OldPairs, All), 137 ( All == [] 138 -> true % nothing pending 139 ; eqs_lefts_rights(All, Xs, Ys), 140 ( dif_unifiable(Xs, Ys, NewPairs) 141 -> NewPairs \== [], % [] ⇒ all satisfied ⇒ fail 142 remove_ornode_from_pairs(OldPairs, OrNode), 143 add_ornode_pairs(NewPairs, OrNode), 144 put_attr(OrNode, dif, node(NewPairs)) 145 ; or_succeed(OrNode) 146 ) 147 ). 148 149remove_ornode_from_pairs([], _). 150remove_ornode_from_pairs([X=Y|T], OrNode) :- 151 ( var(X) -> remove_ornode_v1(X, OrNode) ; true ), 152 ( var(Y) -> remove_ornode_v2(Y, OrNode) ; true ), 153 remove_ornode_from_pairs(T, OrNode). 154 155remove_ornode_v1(X, OrNode) :- 156 ( get_attr(X, dif, vardif(V1, V2)) 157 -> filter_out_ornode(V1, OrNode, NV1), 158 ( NV1 == [], V2 == [] 159 -> del_attr(X, dif) 160 ; put_attr(X, dif, vardif(NV1, V2)) 161 ) 162 ; true 163 ). 164 165remove_ornode_v2(Y, OrNode) :- 166 ( get_attr(Y, dif, vardif(V1, V2)) 167 -> filter_out_ornode(V2, OrNode, NV2), 168 ( V1 == [], NV2 == [] 169 -> del_attr(Y, dif) 170 ; put_attr(Y, dif, vardif(V1, NV2)) 171 ) 172 ; true 173 ). 174 175filter_out_ornode([], _, []). 176filter_out_ornode([N-Y|T], OrNode, L) :- 177 ( N == OrNode 178 -> filter_out_ornode(T, OrNode, L) 179 ; L = [N-Y|LT], 180 filter_out_ornode(T, OrNode, LT) 181 ). 182 183add_ornode_pairs([], _). 184add_ornode_pairs([X=Y|T], OrNode) :- 185 add_ornode(X, Y, OrNode), 186 add_ornode_pairs(T, OrNode).
192add_ornode(X,Y,OrNode) :- 193 add_ornode_var1(X,Y,OrNode), 194 ( var(Y) 195 -> add_ornode_var2(X,Y,OrNode) 196 ; true 197 ). 198 199add_ornode_var1(X,Y,OrNode) :- 200 ( get_attr(X,dif,Attr) 201 -> Attr = vardif(V1,V2), 202 put_attr(X,dif,vardif([OrNode-Y|V1],V2)) 203 ; put_attr(X,dif,vardif([OrNode-Y],[])) 204 ). 205 206add_ornode_var2(X,Y,OrNode) :- 207 ( get_attr(Y,dif,Attr) 208 -> Attr = vardif(V1,V2), 209 put_attr(Y,dif,vardif(V1,[OrNode-X|V2])) 210 ; put_attr(Y,dif,vardif([],[OrNode-X])) 211 ).
223attr_unify_hook(vardif(V1, V2), Other) :- 224 live_ornodes(V1, V2, MyOrNodes), 225 ( var(Other), 226 get_attr(Other, dif, vardif(OV1, OV2)) 227 -> live_ornodes(OV1, OV2, TheirOrNodes), 228 append(MyOrNodes, TheirOrNodes, OrNodes0), 229 sort(OrNodes0, OrNodes) % dedup by identity 230 ; OrNodes = MyOrNodes 231 ), 232 recompute_ornodes(OrNodes). 233 234live_ornodes(V1, V2, OrNodes) :- 235 live_ornodes_(V1, L1, T1), 236 live_ornodes_(V2, T1, []), 237 OrNodes = L1. 238 239live_ornodes_([], T, T). 240live_ornodes_([O-_|R], L, T) :- 241 ( var(O) 242 -> L = [O|L1] 243 ; L = L1 244 ), 245 live_ornodes_(R, L1, T). 246 247recompute_ornodes([]). 248recompute_ornodes([O|T]) :- 249 or_one_fail(O), 250 recompute_ornodes(T).
- and remove
this dead OrNode from every vardif/2 attribute we can find.259or_succeed(OrNode) :- 260 ( get_attr(OrNode,dif,Attr) 261 -> Attr = node(Pairs), 262 del_attr(OrNode,dif), 263 OrNode = (-), 264 del_or_dif(Pairs) 265 ; true 266 ). 267 268del_or_dif([]). 269del_or_dif([X=Y|Xs]) :- 270 cleanup_dead_nodes(X), 271 cleanup_dead_nodes(Y), % JW: what about embedded variables? 272 del_or_dif(Xs). 273 274cleanup_dead_nodes(X) :- 275 ( get_attr(X,dif,Attr) 276 -> Attr = vardif(V1,V2), 277 filter_dead_ors(V1,NV1), 278 filter_dead_ors(V2,NV2), 279 ( NV1 == [], NV2 == [] 280 -> del_attr(X,dif) 281 ; put_attr(X,dif,vardif(NV1,NV2)) 282 ) 283 ; true 284 ). 285 286filter_dead_ors([],[]). 287filter_dead_ors([Or-Y|Rest],List) :- 288 ( var(Or) 289 -> List = [Or-Y|NRest] 290 ; List = NRest 291 ), 292 filter_dead_ors(Rest,NRest).
300or_one_fail(OrNode) :- 301 dif_c_c_l([], OrNode). 302 303 304/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 305 The attribute of a variable X is vardif/2. The first argument is a 306 list of pairs. The first component of each pair is an OrNode. The 307 attribute of each OrNode is node/2. The second argument of node/2 308 is a list of equations A = B. If the LHS of the first equation is 309 X, then return a goal, otherwise don't because someone else will. 310- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ 311 312attribute_goals(Var) --> 313 ( { get_attr(Var, dif, vardif(Ors,_)) } 314 -> or_nodes(Ors, Var) 315 ; or_node(Var) 316 ). 317 318or_node(O) --> 319 ( { get_attr(O, dif, node(Pairs)) } 320 -> { eqs_lefts_rights(Pairs, As, Bs) }, 321 mydif(As, Bs), 322 { del_attr(O, dif) } 323 ; [] 324 ). 325 326or_nodes([], _) --> []. 327or_nodes([O-_|Os], X) --> 328 ( { get_attr(O, dif, node(Eqs)) } 329 -> ( { Eqs = [LHS=_|_], LHS == X } 330 -> { eqs_lefts_rights(Eqs, As, Bs) }, 331 mydif(As, Bs), 332 { del_attr(O, dif) } 333 ; [] 334 ) 335 ; [] % or-node already removed 336 ), 337 or_nodes(Os, X). 338 339mydif([X], [Y]) --> !, dif_if_necessary(X, Y). 340mydif(Xs0, Ys0) --> 341 { reverse(Xs0, Xs), reverse(Ys0, Ys), % follow original order 342 X =.. [f|Xs], Y =.. [f|Ys] 343 }, 344 dif_if_necessary(X, Y). 345 346dif_if_necessary(X, Y) --> 347 ( { dif_unifiable(X, Y, _) } 348 -> [dif(X,Y)] 349 ; [] 350 ). 351 352eqs_lefts_rights([], [], []). 353eqs_lefts_rights([A=B|ABs], [A|As], [B|Bs]) :- 354 eqs_lefts_rights(ABs, As, Bs)
The dif/2 constraint