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).
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 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 ).
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.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).
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).
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 ).
[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.
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).
On unification with a value, we recursively call dif_c_c/3 using the existing OrNodes.
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).
- and remove
this dead OrNode from every vardif/2 attribute we can find.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).
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)
The dif/2 constraint
*/