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, member/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, U), 109 subunifier(U, OrNode) 110 ) 111 ; or_succeed(OrNode) 112 ). 113 114subunifier([], _). 115subunifier([X=Y|T], OrNode) :- 116 dif_c_c(X, Y, OrNode), 117 subunifier(T, OrNode). 118 119 120%! dif_c_c_l(+Unifier, +OrNode) 121% 122% Extend OrNode with new elements from the unifier. Note that it is 123% possible that a unification against the same variable appears as a 124% result of how unifiable acts on sharing subterms. This is prevented 125% by simplify_ornode/3. 126% 127% @see test 14 in src/Tests/attvar/test_dif.pl. 128 129dif_c_c_l(Unifier, OrNode, U) :- 130 extend_ornode(OrNode, List, Tail), 131 dif_c_c_l_aux(Unifier, OrNode, List0, Tail), 132 ( simplify_ornode(List0, List, U) 133 -> true 134 ; List = List0, 135 or_succeed(OrNode), 136 U = [] 137 ). 138 139extend_ornode(OrNode, List, Vars) :- 140 ( get_attr(OrNode, dif, node(Vars)) 141 -> true 142 ; Vars = [] 143 ), 144 put_attr(OrNode,dif,node(List)). 145 146dif_c_c_l_aux([],_,List,List). 147dif_c_c_l_aux([X=Y|Unifier],OrNode,List,Tail) :- 148 List = [X=Y|Rest], 149 add_ornode(X,Y,OrNode), 150 dif_c_c_l_aux(Unifier,OrNode,Rest,Tail). 151 152%! add_ornode(+X, +Y, +OrNode) 153% 154% Extend the vardif constraints on X and Y with the OrNode. 155 156add_ornode(X,Y,OrNode) :- 157 add_ornode_var1(X,Y,OrNode), 158 ( var(Y) 159 -> add_ornode_var2(X,Y,OrNode) 160 ; true 161 ). 162 163add_ornode_var1(X,Y,OrNode) :- 164 ( get_attr(X,dif,Attr) 165 -> Attr = vardif(V1,V2), 166 put_attr(X,dif,vardif([OrNode-Y|V1],V2)) 167 ; put_attr(X,dif,vardif([OrNode-Y],[])) 168 ). 169 170add_ornode_var2(X,Y,OrNode) :- 171 ( get_attr(Y,dif,Attr) 172 -> Attr = vardif(V1,V2), 173 put_attr(Y,dif,vardif(V1,[OrNode-X|V2])) 174 ; put_attr(Y,dif,vardif([],[OrNode-X])) 175 ). 176 177%! simplify_ornode(+OrNode) is semidet. 178% 179% Simplify the possible unifications left on the original dif/2 terms. 180% There are two reasons for simplification. First of all, due to the 181% way unifiable works we may end up with variables in the unifier that 182% do not refer to the original terms, but to variables in subterms, 183% e.g. `[V1 = f(a, V2), V2 = b]`. As a result of subsequent unifying 184% variables, the unifier may end up having multiple entries for the 185% same variable, possibly having different values, e.g., `[X = a, X = 186% b]`. As these can never be satified both we have prove of 187% inequality. 188% 189% Finally, we remove elements from the list that have become equal. If 190% the OrNode is empty, the original terms are equal and thus we must 191% fail. 192% 193% @tbd The simplification is complicated. Another approach would be to 194% turn `[X1=Y1, X2=Y2, ...]` into `[X1,X2,...]` and `[Y1,Y2,...]` and 195% call unifiable/3 on these lists to either end up with a 196% contradiction (satisfied) or a new unifier. This is a stronger 197% propagation. Seems not so easy though. Both pending constraints and 198% reconnecting to the proper variables need attention. 199 200simplify_ornode(OrNode) :- 201 ( get_attr(OrNode, dif, node(Pairs0)) 202 -> simplify_ornode(Pairs0, Pairs, U), 203 ( Pairs == [], 204 U == [] 205 -> fail 206 ; put_attr(OrNode, dif, node(Pairs)), 207 subunifier(U, OrNode) 208 ) 209 ; true 210 ). 211 212simplify_ornode(List0, List, U) :- 213 sort(1, @=<, List0, Sorted), 214 simplify_ornode_(Sorted, List, U). 215 216simplify_ornode_([], List, U) => 217 List = [], 218 U = []. 219simplify_ornode_([V1=V2|T], List, U), V1 == V2 => 220 simplify_ornode_(T, List, U). 221simplify_ornode_([V1=Val1,V2=Val2|T], List, U), var(V1), V1 == V2 => 222 ( ?=(Val1, Val2) 223 -> Val1 == Val2, 224 simplify_ornode_([V1=Val2|T], List, U) 225 ; U = [Val1=Val2|UT], 226 simplify_ornode_([V2=Val2|T], List, UT) 227 ). 228simplify_ornode_([H|T], List, U) => 229 List = [H|Rest], 230 simplify_ornode_(T, Rest, U). 231 232 233%! attr_unify_hook(+VarDif, +Other) 234% 235% If two dif/2 variables are unified we must join the two vardif/2 236% terms. To do so, we filter the vardif terms for the ones involved in 237% this unification. Those that are represent OrNodes that have a 238% unification satisfied. For the rest we remove the unifications with 239% _self_, append them and use this as new vardif term. 240% 241% On unification with a value, we recursively call dif_c_c/3 using the 242% existing OrNodes. 243 244attr_unify_hook(vardif(V1,V2),Other) :- 245 ( get_attr(Other, dif, vardif(OV1,OV2)) 246 -> ( ( or_nodes_completed(V1) 247 ; or_nodes_completed(V2) 248 ) 249 -> true 250 ; reverse_lookups(V1, Other, OrNodes1, NV1), 251 or_one_fails(OrNodes1), 252 reverse_lookups(OV1, Other, OrNodes2, NOV1), 253 or_one_fails(OrNodes2), 254 remove_obsolete(V2, Other, NV2), 255 remove_obsolete(OV2, Other, NOV2), 256 append(NV1, NOV1, CV1), 257 append(NV2, NOV2, CV2), 258 ( CV1 == [], CV2 == [] 259 -> del_attr(Other, dif) 260 ; put_attr(Other, dif, vardif(CV1,CV2)) 261 ) 262 ) 263 ; var(Other) % unrelated variable 264 -> put_attr(Other, dif, vardif(V1,V2)) 265 ; verify_compounds(V1, Other), % concrete value 266 verify_compounds(V2, Other) 267 ). 268 269%! or_nodes_completed(+List) is semidet. 270% 271% Unification may have made some of the or nodes internally 272% inconsistent. This code checks for that and makes the or node 273% succeed if this is the case. 274 275or_nodes_completed(List) :- 276 member(Or-_Value, List), 277 get_attr(Or, dif, node(Unifiers0)), 278 copy_term_nat(Unifiers0, Unifiers), 279 \+ unify_list(Unifiers), 280 !, 281 or_succeed(Or). 282 283unify_list([]). 284unify_list([A=A|T]) :- 285 unify_list(T). 286 287 288remove_obsolete([], _, []). 289remove_obsolete([N-Y|T], X, L) :- 290 ( Y==X 291 -> remove_obsolete(T, X, L) 292 ; L=[N-Y|RT], 293 remove_obsolete(T, X, RT) 294 ). 295 296reverse_lookups([],_,[],[]). 297reverse_lookups([N-X|NXs],Value,Nodes,Rest) :- 298 ( X == Value 299 -> Nodes = [N|RNodes], 300 Rest = RRest 301 ; Nodes = RNodes, 302 Rest = [N-X|RRest] 303 ), 304 reverse_lookups(NXs,Value,RNodes,RRest). 305 306%! verify_compounds(+Nodes, +Value) 307% 308% Unification to a concrete Value (no variable) 309 310verify_compounds([],_). 311verify_compounds([OrNode-Y|Rest],X) :- 312 ( var(Y) 313 -> true 314 ; OrNode == (-) 315 -> true 316 ; dif_c_c(X,Y,OrNode) 317 ), 318 verify_compounds(Rest,X). 319 320%! or_succeed(+OrNode) is det. 321% 322% The dif/2 constraint related to OrNode is complete, i.e., some 323% (sub)terms can definitely not become equal. Next, we can clean up 324% the constraints. We do so by setting the OrNode to `-` and remove 325% this _dead_ OrNode from every vardif/2 attribute we can find. 326 327or_succeed(OrNode) :- 328 ( get_attr(OrNode,dif,Attr) 329 -> Attr = node(Pairs), 330 del_attr(OrNode,dif), 331 OrNode = (-), 332 del_or_dif(Pairs) 333 ; true 334 ). 335 336del_or_dif([]). 337del_or_dif([X=Y|Xs]) :- 338 cleanup_dead_nodes(X), 339 cleanup_dead_nodes(Y), % JW: what about embedded variables? 340 del_or_dif(Xs). 341 342cleanup_dead_nodes(X) :- 343 ( get_attr(X,dif,Attr) 344 -> Attr = vardif(V1,V2), 345 filter_dead_ors(V1,NV1), 346 filter_dead_ors(V2,NV2), 347 ( NV1 == [], NV2 == [] 348 -> del_attr(X,dif) 349 ; put_attr(X,dif,vardif(NV1,NV2)) 350 ) 351 ; true 352 ). 353 354filter_dead_ors([],[]). 355filter_dead_ors([Or-Y|Rest],List) :- 356 ( var(Or) 357 -> List = [Or-Y|NRest] 358 ; List = NRest 359 ), 360 filter_dead_ors(Rest,NRest). 361 362 363%! or_one_fail(+OrNode) is semidet. 364% 365% Some unification related to OrNode succeeded. 366 367or_one_fail(OrNode) :- 368 simplify_ornode(OrNode). 369 370or_one_fails([]). 371or_one_fails([N|Ns]) :- 372 or_one_fail(N), 373 or_one_fails(Ns). 374 375 376/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 377 The attribute of a variable X is vardif/2. The first argument is a 378 list of pairs. The first component of each pair is an OrNode. The 379 attribute of each OrNode is node/2. The second argument of node/2 380 is a list of equations A = B. If the LHS of the first equation is 381 X, then return a goal, otherwise don't because someone else will. 382- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ 383 384attribute_goals(Var) --> 385 ( { get_attr(Var, dif, vardif(Ors,_)) } 386 -> or_nodes(Ors, Var) 387 ; or_node(Var) 388 ). 389 390or_node(O) --> 391 ( { get_attr(O, dif, node(Pairs)) } 392 -> { eqs_lefts_rights(Pairs, As, Bs) }, 393 mydif(As, Bs), 394 { del_attr(O, dif) } 395 ; [] 396 ). 397 398or_nodes([], _) --> []. 399or_nodes([O-_|Os], X) --> 400 ( { get_attr(O, dif, node(Eqs)) } 401 -> ( { Eqs = [LHS=_|_], LHS == X } 402 -> { eqs_lefts_rights(Eqs, As, Bs) }, 403 mydif(As, Bs), 404 { del_attr(O, dif) } 405 ; [] 406 ) 407 ; [] % or-node already removed 408 ), 409 or_nodes(Os, X). 410 411mydif([X], [Y]) --> !, dif_if_necessary(X, Y). 412mydif(Xs0, Ys0) --> 413 { reverse(Xs0, Xs), reverse(Ys0, Ys), % follow original order 414 X =.. [f|Xs], Y =.. [f|Ys] 415 }, 416 dif_if_necessary(X, Y). 417 418dif_if_necessary(X, Y) --> 419 ( { dif_unifiable(X, Y, _) } 420 -> [dif(X,Y)] 421 ; [] 422 ). 423 424eqs_lefts_rights([], [], []). 425eqs_lefts_rights([A=B|ABs], [A|As], [B|Bs]) :- 426 eqs_lefts_rights(ABs, As, Bs)