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). 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 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 ). 95 96%! dif_c_c(+X,+Y,!OrNode) 97% 98% Enforce dif(X,Y) that is related to the given OrNode. If X and Y are 99% equal we reduce the OrNode. If they cannot unify we are done. 100% Otherwise we extend the OrNode with new pairs and create/extend the 101% vardif/2 terms for the left hand side of the unifier as well as the 102% right hand if this is a variable. 103 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 ). 112 113 114%! dif_c_c_l(+Unifier, +OrNode) 115% 116% Combine the incoming unifier with the OrNode's current pending set, 117% then recompute the most-general unifier for the whole using 118% unifiable/3 over the accumulated left- and right-hand-side lists. 119% That gives canonical propagation and avoids the infinite oscillation 120% pair-wise simplification hits on cyclic terms. 121% 122% Fails if the recomputed set is empty — that means all pending 123% equations are trivially satisfied and thus the original dif/2 terms 124% are equal, so dif/2 must fail. Calls or_succeed/1 when unifiable/3 125% itself fails: the pending equations can never all hold, so the two 126% terms are definitely unequal and dif/2 is satisfied. 127 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). 187 188%! add_ornode(+X, +Y, +OrNode) 189% 190% Extend the vardif constraints on X and Y with the OrNode. 191 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 ). 212 213%! attr_unify_hook(+VarDif, +Other) 214% 215% Called after the attributed variable has been unified with Other. 216% Collects every OrNode this variable (and, for a var-var unification, 217% Other) is involved in and recomputes each one's MGU. The rebuild 218% inside dif_c_c_l/2 keeps the OrNode's pending list, this variable's 219% vardif and Other's vardif consistent — the current bindings show 220% through variable dereferencing when eqs_lefts_rights/3 walks the 221% pending list. 222 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). 251 252%! or_succeed(+OrNode) is det. 253% 254% The dif/2 constraint related to OrNode is complete, i.e., some 255% (sub)terms can definitely not become equal. Next, we can clean up 256% the constraints. We do so by setting the OrNode to `-` and remove 257% this _dead_ OrNode from every vardif/2 attribute we can find. 258 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). 293 294 295%! or_one_fail(+OrNode) is semidet. 296% 297% Recompute the MGU for OrNode's pending set without adding any new 298% equations. Fails when the set becomes empty (dif/2 fails). 299 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)