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).
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, 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).
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).
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 ).
[V1 = f(a, V2), V2 = b]. As a result of subsequent unifying
variables, the unifier may end up having multiple entries for the
same variable, possibly having different values, e.g., [X = a, X =
b]. As these can never be satified both we have prove of
inequality.
Finally, we remove elements from the list that have become equal. If the OrNode is empty, the original terms are equal and thus we must fail.
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).
On unification with a value, we recursively call dif_c_c/3 using the existing OrNodes.
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 ).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).
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).
- and remove
this dead OrNode from every vardif/2 attribute we can find.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).
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)
The dif/2 constraint
*/