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-2022, 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 simplify_ornode/3. 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-U \== []-[], 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_([V1=V2|T], List, U), V1 == V2 => 211 simplify_ornode_(T, List, U). 212simplify_ornode_([V1=Val1,V2=Val2|T], List, U), var(V1), V1 == V2 => 213 ( ?=(Val1, Val2) 214 -> Val1 == Val2, 215 simplify_ornode_([V1=Val2|T], List, U) 216 ; U = [Val1=Val2|UT], 217 simplify_ornode_([V2=Val2|T], List, UT) 218 ). 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)