1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2% BEGIN LICENSE BLOCK 3% Version: CMPL 1.1 4% 5% The contents of this file are subject to the Cisco-style Mozilla Public 6% License Version 1.1 (the "License"); you may not use this file except 7% in compliance with the License. You may obtain a copy of the License 8% at www.eclipse-clp.org/license. 9% 10% Software distributed under the License is distributed on an "AS IS" 11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 12% the License for the specific language governing rights and limitations 13% under the License. 14% 15% The Original Code is The Cardinal Constraint Solver for ECLiPSe. 16% The Initial Developer of the Original Code is Francisco M.C.A. Azevedo. 17% Portions created by the Initial Developer are Copyright (C) 1999-2004. 18% All Rights Reserved. 19% 20% Contributor(s): Francisco M. C. A. Azevedo <fa@di.fct.unl.pt>. 21% 22% Alternatively, the contents of this file may be used under the terms of 23% either of the GNU General Public License Version 2 or later (the "GPL"), 24% or the GNU Lesser General Public License Version 2.1 or later (the "LGPL"), 25% in which case the provisions of the GPL or the LGPL are applicable instead 26% of those above. If you wish to allow use of your version of this file only 27% under the terms of either the GPL or the LGPL, and not to allow others to 28% use your version of this file under the terms of the MPL, indicate your 29% decision by deleting the provisions above and replace them with the notice 30% and other provisions required by the GPL or the LGPL. If you do not delete 31% the provisions above, a recipient may use your version of this file under 32% the terms of any one of the MPL, the GPL or the LGPL. 33% END LICENSE BLOCK 34% 35% cardinal.ecl By Francisco Azevedo 1999-2004 (for ECLiPSe) 36% 37% Set constraints (including 'complement') with great cardinality processing. 38% 39%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 40 41 42:- module(cardinal). 43 44:- comment(categories, ["Constraints"]). 45:- comment(summary, "Finite Set Constraints Library"). 46:- comment(author, "Francisco Azevedo, CENTRIA"). 47:- comment(status, evolving). 48 49:- export 50 op(650, xfx, `= ), `= /2, 51 op(650, xfx, `/=), `/= /2, %different/2 52 op(650, xfx, `$ ), `$ /2, %disjoint/2 53 op(650, xfx, `@ ), `@ /2, %member_set/2 54 op(650, xfx, `-@), `-@ /2, %not_in_set/2 55 op(650, xfx, `::), `:: /2, %set/4 56 op(550, xfx, `>=), `>= /2, %contains/2 57 op(500, yfx, `\/), %my_set_union/3 58 op(400, yfx, `/\), %my_set_intersection/3 59 op(300, yfx, `\ ), %my_set_difference/3 60 cardinality/2, 61 domain/2, 62 domain/3, 63 glb/2, 64 poss/2, 65 glb_poss/3, 66 lub/4, 67 lub/2, 68% union_att/2, 69% union_att/3, 70 union_var/2, 71 minimum/2, 72 maximum/2, 73 set/4, 74 sets/4, 75 complement/2, 76 complement/3, 77 set_labeling/1, 78 set_labeling/2, 79 refine/2, 80 card_labeling/1, 81 all_union/2, 82 all_disjoint/1, 83%For Conjunto compatibility: 84 op(650, fx, # ), (#) /2, 85 op(650, xfx, `<> ), `<> /2, 86 op(650, xfx, in ), in /2, 87 op(650, xfx, notin ), notin/2, 88 op(650, xfx, `< ), `< /2, 89 op(300, yfx, \ ) 90 . 91 92:- local 93 is_list/1. % shallow list check 94 95:-lib(fd). 96:-lib(lists). 97 98 99:- export struct(cardinal(domain,cardinality,minimum,maximum,union,bounded,glb,lub,bound)). 100/* 101domain: set domain in the form [Glb:NIn,Poss:NMax] 102cardinality: FD (integer) variable 103minimum: FD (integer) variable or unused 104maximum: FD (integer) variable or unused 105union: [U,GlbU+PossU,Singles,Lengths] or unused 106 U: set variable 107 GlbU: ordered list with assured union elements 108 PossU: ordered list with possible union elements with counters (X:N) 109 Singles: elements where N=1 in PossU 110 Lengths: possible lengths of set elements with counters (Len:N) in decreasing order 111bounded, glb, 112lub, bound: suspension lists 113*/ 114 115:-comment(include, cardinal_comments). 116:- include([cardinal_util,cardinal_functions]). 117 118 119:- meta_attribute(cardinal, [unify:my_unify_sets_handler/2, 120 print:my_print_set_handler/2]). 121 122 123 124S1 `>= S2 :- contains(S1,S2). 125S1 `/= S2 :- different(S1,S2). 126S1 `$ S2 :- disjoint(S1,S2). 127X `@ S :- member_set(X,S). 128X `-@ S :- not_in_set(X,S). 129S `:: Glb+Poss:Card :- !, set(S,Glb,Poss,[cardinality:Card]). 130S `:: Glb+Poss :- set(S,Glb,Poss,[]). 131S `:: Glb..Lub :- set_without(Lub,Glb,Poss), set(S,Glb,Poss,[]). 132Set1 `= Exp2 :- var(Set1), !, eval_exp(Exp2, Set1). 133Exp1 `= Set2 :- var(Set2), !, eval_exp(Exp1, Set2). 134Exp1 `= Exp2 :- ground(Exp2), !, eval_exp(Exp2, S), eval_exp(Exp1, S). 135Exp1 `= Exp2 :- ground(Exp1), !, eval_exp(Exp1, S), eval_exp(Exp2, S). 136Exp1 `= Exp2 :- eval_exp(Exp1, S1), eval_exp(Exp2, S2), S1=S2. 137%For Conjunto compatibility: 138S1 `<> S2 :- disjoint(S1,S2). 139X in S :- member_set(X,S). 140X notin S :- not_in_set(X,S). 141S1 `< S2 :- contains(S2,S1). 142 143%------- 144% 'Global' constraints: 145% 146all_union([],U):- !, U=[]. 147all_union([S],U):- !, U=S. 148all_union(L, U):- halve(L,L1,L2), 149 (is_my_set(U) -> lub(U,Lub), sets([U1,U2],[],Lub,[]) ; true), 150 all_union(L1,U1), all_union(L2,U2), my_set_union(U1,U2,U). 151 152 153all_disjoint(Sets):- 154 all_disjoint(Sets, Lubs, Cards), 155 all_sets_union(Lubs, [],LubsUnion), 156 length(LubsUnion, NMax), 157 sum_cards(Cards, SumCards), 158 SumCards #<= NMax. 159 160all_disjoint([], [], []). 161all_disjoint([H|T], [Lub|Lubs], [Card|Cards]):- 162 disjoint_set(T, H), 163 lub(H, Lub), cardinality(H, Card), 164 all_disjoint(T, Lubs, Cards). 165 166disjoint_set([], _). 167disjoint_set([H|T], S):- H `$ S, disjoint_set(T, S). 168 169 170sets([],_,_,_). 171sets([H|T],Glb,Poss,Functions):- set(H,Glb,Poss,Functions), sets(T,Glb,Poss,Functions). 172 173% End of 'global' constraints. 174%--- 175 176eval_exp(Exp, Set):- var(Exp), !, Set=Exp. 177eval_exp(Exp, Set):- is_list(Exp), !, sort(Exp, OrderedList), Set=OrderedList. 178eval_exp(Exp1 `\/ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_union(S1,S2,S). 179eval_exp(Exp1 `/\ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_intersection(S1,S2,S). 180eval_exp(Exp1 `\ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_difference(S1,S2,S). 181eval_exp(Exp1 \/ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_union(S1,S2,S). 182eval_exp(Exp1 /\ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_intersection(S1,S2,S). 183eval_exp(Exp1 \ Exp2, S):- !, eval_exp(Exp1,S1), eval_exp(Exp2,S2), my_set_difference(S1,S2,S). 184 185 186 187%-------- 188% Labeling predicates. 189% 190set_labeling(Var):- meta(Var), !, set_labeling(up, [Var]). 191set_labeling(Vars):- set_labeling(up, Vars). 192 193set_labeling(_,[]). 194set_labeling(UpDown, [H|T]):- nonvar(H), !, set_labeling(UpDown, T). 195set_labeling(UpDown, [H|T]):- 196 refine(UpDown, H), 197 set_labeling(UpDown, [H|T]). 198 199refine(up, S):- 200 domain(S, [Glb:NIn,[X|Poss]:NMax]), val(X,VX), 201 (NIn1 is NIn+1, insert(Glb, VX, Glb1), set_domain(S, [Glb1:NIn1,Poss:NMax]) 202 ;NMax1 is NMax-1, set_poss(S, Poss,NMax1) 203 ). 204refine(down, S):- 205 domain(S, [Glb:NIn,[X|Poss]:NMax]), val(X,VX), 206 (NMax1 is NMax-1, set_poss(S, Poss,NMax1) 207 ;NIn1 is NIn+1, insert(Glb, VX, Glb1), set_domain(S, [Glb1:NIn1,Poss:NMax]) 208 ). 209 210card_labeling([]). 211card_labeling([H|T]):- 212 cardinality(H, C), 213 indomain(C), 214 card_labeling(T). 215% 216% End of Labeling predicates. 217%-------- 218 219 220 221 222%-------- 223% my_print_set_handler(+Set, +Att) 224%Operation : printing the attribute 225% 226%Handler : handler(?Meta, -Attribute) 227% 228%Description : Printing the attribute in printf/2, 3 when the m option is specified. Meta is the attributed variable being 229%printed, Attribute is the term which will be printed as a value for this attribute, qualified by the attribute name. If no 230%handler is specified for an attribute, it will not be printed. If there is only one attribute with an associated print handler, 231%the attribute value is not qualified with the attribute name. 232%-- 233my_print_set_handler(Set, Set):- nonvar(Set), !. 234my_print_set_handler(SetVar, Info):- get_attribute(cardinal, SetVar, Info). 235 236 237 238get_attribute(cardinal, _{cardinal:Attribute}, A):- -?-> A = Attribute. 239 240is_my_set(S):- get_attribute(cardinal, S, Att), nonvar(Att), !. 241is_my_set(S):- nonvar(S), is_list(S). 242 243 244%-------- 245% Setting cardinal attributes: 246% full domain or just poss, and respective suspension lists; union; minimum, maximum 247%-- 248 249t_set_domain(set_domain(Set, Domain), 250 (Domain = [Glb:_,[]:_] -> Set=Glb 251 ;get_attribute(cardinal, Set, Att) -> 252 Att = cardinal with [domain:[OldGlb:OldNIn,OldPoss:OldNMax],cardinality:C], 253 setarg(domain of cardinal, Att, Domain), 254 Domain = [Glb:NIn,Poss:NMax], 255 (OldNIn==NIn -> 256 (OldNMax==NMax -> true 257 ;check_union_lub(Att, NIn, OldPoss,OldNMax, Poss,NMax), 258 schedule_suspensions(lub of cardinal, Att), 259 schedule_suspensions(bounded of cardinal, Att), 260 C #<= NMax 261 ) 262 ;check_union_glb(Att, OldGlb, Glb), 263 (OldNMax==NMax -> C #>= NIn 264 ;check_union_lub(Att, NIn, OldPoss,OldNMax, Poss,NMax), 265 C #>= NIn, C #<= NMax, 266 schedule_suspensions(lub of cardinal, Att) 267 ), 268 schedule_suspensions(glb of cardinal, Att), 269 schedule_suspensions(bounded of cardinal, Att), 270 wake 271 ) 272 ;Domain = [Set:_,_] 273 )). 274:-inline(set_domain/2, t_set_domain/2). 275set_domain(Set, Domain):- set_domain(Set, Domain). %inlined 276 277 278 279t_set_poss(set_poss(Set, Poss, NMax), 280 (get_attribute(cardinal, Set, Att) -> 281 Att = cardinal with [domain:[Glb:NIn,OldPoss:OldNMax],cardinality:C], 282 (Poss==[] -> Set=Glb 283 ;OldNMax==NMax -> setarg(domain of cardinal, Att, [Glb:NIn,Poss:NMax]) %neccessary for sets with union function, when attaching lengths to poss elements. 284 ;setarg(domain of cardinal, Att, [Glb:NIn,Poss:NMax]), 285 check_union_lub(Att, NIn, OldPoss,OldNMax, Poss,NMax), 286 C #<= NMax, 287 schedule_suspensions(lub of cardinal, Att), 288 schedule_suspensions(bounded of cardinal, Att), 289 wake 290 ) 291 ;Poss=[] 292 )). 293:-inline(set_poss/3, t_set_poss/2). 294set_poss(Set, Poss, NMax):- set_poss(Set, Poss, NMax). %inlined 295 296 297 298t_set_cardinality(set_cardinality(Set, Card), 299 (get_attribute(cardinal, Set, Att) -> setarg(cardinality of cardinal, Att, Card) 300 ;length(Set, Card) 301 )). 302:-inline(set_cardinality/2, t_set_cardinality/2). 303set_cardinality(Set, Card):- set_cardinality(Set, Card). %inlined 304 305 306 307t_set_union(set_union(Set, UnionData), 308 (get_attribute(cardinal, Set, Att) -> setarg(union of cardinal, Att, UnionData) 309 ;all_sets_union(Set, [],U), UnionData=[U|_] 310 )). 311:-inline(set_union/2, t_set_union/2). 312set_union(Set, UnionData):- set_union(Set, UnionData). %inlined 313 314 315t_set_minimum(set_minimum(Set, Min), 316 (get_attribute(cardinal, Set, Att) -> setarg(minimum of cardinal, Att, Min) 317 ;Set=[Min|_] 318 )). 319:-inline(set_minimum/2, t_set_minimum/2). 320set_minimum(Set, Min):- set_minimum(Set, Min). %inlined 321 322 323t_set_maximum(set_maximum(Set, Max), 324 (get_attribute(cardinal, Set, Att) -> setarg(maximum of cardinal, Att, Max) 325 ;reverse(Set, [Max|_]) 326 )). 327:-inline(set_maximum/2, t_set_maximum/2). 328set_maximum(Set, Max):- set_maximum(Set, Max). %inlined 329 330% End of predicates for setting cardinal attributes. 331%------------- 332 333 334%-------- 335% set_info(+Set, +Cardinality, -Info) 336% Info is a set structure (cardinal with [domain:[Glb:NIn,Poss:NMax],cardinality:N]) 337% corresponding to Set. 338% If Set is an attributted variable, then Info is its set attributte. 339% If Set is ground, Info is constructed accordingly. 340%-- 341set_info(S, _, Info):- get_attribute(cardinal, S, Att), !, Info=Att. 342set_info(S, Card, cardinal with [domain:[S:N,[]:N],cardinality:N]):- var(Card),!,length(S,N). 343set_info(S, Card, cardinal with [domain:[S:Card,[]:Card],cardinality:Card]). 344 345set_info(Set, Info):- set_info(Set, _, Info). 346 347 348assure_set(S, S, Info):- get_attribute(cardinal, S, Info), !. 349assure_set(S, SS, cardinal with [domain:[SS:N,[]:N],cardinality:N]):- 350 is_list(S), sort(S,SS), length(SS, N), !. 351 352 353%-------- 354% Getting cardinal attributes: 355% cardinality, domain, bounds; minimum, maximum; union 356%-- 357 358#(Exp, C):- eval_exp(Exp, S), set_info(S, _, cardinal with cardinality:C). 359cardinality(S, C):- set_info(S, _, cardinal with cardinality:C). 360domain(S, Card, D):- set_info(S, Card, cardinal with domain:D). 361domain(S, D):- set_info(S, _, cardinal with domain:D). 362glb_poss(S, Glb, Poss):- set_info(S, n, cardinal with domain:[Glb:_,Poss:_]). 363glb(S, G):- set_info(S, n, cardinal with domain:[G:_,_]). 364poss(S, P):- set_info(S, n, cardinal with domain:[_,P:_]). 365lub(S, Glb,Poss, Lub):- glb_poss(S,Glb,Poss), lub(Glb,Poss,Lub). 366 367t_lub(lub(S, Lub), lub(S,_,_,Lub)). 368:-inline(lub/2, t_lub/2). 369lub(S, Lub):- lub(S, Lub). %inlined 370 371minimum(S, Min):- 372 get_attribute(cardinal, S, cardinal with minimum:MinAtt), !, 373 (free(MinAtt) -> minimum_function(Min,S) ; Min = MinAtt). 374minimum([Min|_], Min). 375 376maximum(S, Max):- 377 get_attribute(cardinal, S, cardinal with maximum:MaxAtt), !, 378 (free(MaxAtt) -> maximum_function(Max,S) ; Max = MaxAtt). 379maximum(S, Max):- reverse(S, [Max|_]). 380 381%union_att(+SetVar, +UnionVar, -UnionAttribute) 382union_att(S, _, U):- 383 get_attribute(cardinal, S, cardinal with union:UnionAtt), !, 384 (free(UnionAtt) -> U = [Union|_], union_function(Union,S), union_att(S, Union, U) 385 ;U = UnionAtt 386 ). 387union_att(S, U, [U,U+[],[],[]]):- var(U), !, all_sets_union(S, [],U). 388 %INEFFICIENT. When S is ground, attributes are lost 389union_att(_, U, [U,U+[],[],[]]). 390 391t_union_att(union_att(S,U), union_att(S,_,U)). 392:-inline(union_att/2, t_union_att/2). 393union_att(S,U):- union_att(S,U). %inlined 394 395%t_union_var(union_var(S,U), union_att(S,_,[U|_])). 396%:-inline(union_var/2, t_union_var/2). 397%union_var(S,U):- union_var(S,U). %inlined 398union_var(S,U):- union_att(S,_,[U|_]). 399 400% End of predicates for getting cardinal attributes. 401%------------- 402 403 404 405%-------- 406% set_equality(+SetVar, +Glb,+Poss) 407% Constrain bounds of SetVar when equalled to a set with bounds Glb and Poss. 408%-- 409t_set_equality(set_equality(S, GlbArg,PossArg), 410 (glb_poss(S, Glb1,Poss1), 411 verify_inclusion(GlbArg, Glb1,Poss1, Glb2), %Glb2 is the rest of Glb1 (Glb1\GlbArg) 412 verify_inclusion(Glb2, [],PossArg, _), %no need to check inclusion of Glb2 in GlbArg 413 set_union(GlbArg, Glb2, In, 0,NIn), 414 set_intersection(Poss1, PossArg, Poss, NIn,NMax), 415 set_domain(S, [In:NIn,Poss:NMax]) 416 )). 417 418:-inline(set_equality/3, t_set_equality/2). 419 420set_equality(S, GlbArg,PossArg):- set_equality(S, GlbArg,PossArg). %inlined 421 422 423%-------- 424% my_unify_sets_handler(+Set, +Att) 425% Handler for sets unification. A set with attributte Att was unified with Set. 426% Corresponds to the set equality constraint. 427%-- 428my_unify_sets_handler(_, Att):- var(Att), !. 429my_unify_sets_handler(Set, Att):- 430 nonvar(Set), !, 431 sorted_length(Set, N), !, 432 Att = cardinal with [domain:[Glb:NIn,Poss:NMax],cardinality:C], 433 verify_inclusion(Set, Glb,Poss, []), 434 setarg(domain of cardinal, Att, [Set:N,[]:N]), 435 (N == NIn -> true ; check_union_glb(Att, Glb, Set)), 436 (N == NMax -> true ; check_union_lub(Att, NIn, Poss,NMax, [],N)), 437 (N == NIn -> true ; schedule_suspensions(glb of cardinal, Att)), 438 (N == NMax -> true ; schedule_suspensions(lub of cardinal, Att)), 439 C #= N, 440 schedule_suspensions(bound of cardinal, Att), 441 schedule_suspensions(bounded of cardinal, Att). 442my_unify_sets_handler(SetVar, Att):- 443 set_info(SetVar, AttVar), 444 merge_suspension_lists(glb of cardinal, Att, glb of cardinal, AttVar), 445 merge_suspension_lists(lub of cardinal, Att, lub of cardinal, AttVar), 446 merge_suspension_lists(bounded of cardinal, Att, bounded of cardinal, AttVar), 447 merge_suspension_lists(bound of cardinal, Att, bound of cardinal, AttVar), 448 Att = cardinal with [domain:[Glb:_,Poss:_],cardinality:C1, 449 minimum:Min1,maximum:Max1,union:Union1], 450 AttVar = cardinal with [cardinality:C2,minimum:Min2,maximum:Max2,union:Union2], 451 schedule_suspensions(bound of cardinal, AttVar), 452 C1 #= C2, Min1 = Min2, Max1 = Max2, %may wake 453 ((var(Union1) ; var(Union2)) -> Union1=Union2 454 ;Union1 = [UVar1|_], 455 Union2 = [UVar2|_], 456 UVar1 = UVar2 457 ), 458 set_equality(SetVar, Glb,Poss). 459 460 461 462%-------- 463% set(?Set, ?Glb,?Poss, +Functions) 464% Set variable declaration: 465% Set is constrained by bounds Glb and Poss, and has a list of Functions, 466% including Cardinality, which can be a finite domain variable or its domain. 467%-- 468set(S, Glb,Possible, Functions):- 469 ground(S), !, 470 sort(S, Set), 471 (ground(Glb), ground(Possible) -> 472 sort(Glb, SGlb), sort(Possible, SPossible), 473 verify_inclusion(SGlb, Set,[], RestSet), % SGlb contained in Set 474 set_without(RestSet, SPossible, []) % Set contained in Glb U Possible 475 ; (var(Glb) -> Glb=Set ; sort(Glb,Set)), 476 (var(Possible) -> Possible=[] ; true) 477 ), 478 check_ground_functions(Functions, Set). 479set(S, Glb,Possible, Functions):- 480 is_my_set(S), !, 481 (ground(Glb), ground(Possible) -> 482 my_setof(X, (member(X,Glb),ground(X)), GlbArg), 483 my_setof(Y, (member(Y,Possible),ground(Y), 484 \+ my_member(Y,GlbArg)), PossArg), 485 set_equality(S, GlbArg,PossArg) 486 ; glb_poss(S, Glb1,Poss1), 487 (var(Glb) -> Glb=Glb1 ; sort(Glb,Glb1)), 488 (var(Possible) -> Possible=Poss1 ; sort(Possible,Poss1)) 489 ), 490 check_new_functions(Functions, S). 491set(S, Glb,Possible, Functions):- 492 (ground(Glb) -> true ; writeln('Non-ground glb'), fail), 493 my_setof(X, member(X,Glb), In), 494 length(In, NIn), 495 (ground(Possible) -> true ; writeln('Non-ground lub'), fail), 496 my_setof(Y, (member(Y,Possible), \+ my_member(Y,In)), Poss), 497 length(Poss, NPoss), 498 NMax is NIn+NPoss, 499 SetAtt = cardinal with [domain:[In:NIn,Poss:NMax], cardinality:_, 500 minimum:_, maximum:_, union:_], 501 add_attribute(S, SetAtt, cardinal), 502 init_suspension_list(bounded of cardinal, SetAtt), 503 init_suspension_list(glb of cardinal, SetAtt), 504 init_suspension_list(lub of cardinal, SetAtt), 505 init_suspension_list(bound of cardinal, SetAtt), 506 check_functions(Functions, S). 507 508 509 510 511 512%-------- 513% different(?Set1, ?Set2) 514% Constraint: Set1 and Set2 are different sets. 515%-- 516different(S1, S2):- 517 ground(S1), ground(S2), !, 518 is_list(S1), is_list(S2), 519 (member(X,S1), \+ member(X,S2) ; member(X,S2), \+ member(X,S1)), !. 520different(S1, S2):- 521 assure_set(S1, Set1, _), 522 assure_set(S2, Set2, _), 523 not_same_set(Set1,Set2). 524 525not_same_set(S1,S2):- S1 \== S2, 526 (var(S1) -> suspend(not_same_set(S1,S2), 3, S1->cardinal:bound) 527 ;var(S2) -> suspend(not_same_set(S1,S2), 3, S2->cardinal:bound) 528 ;true 529 ). 530 531 532 533 534%-------- 535% disjoint(?Set1, ?Set2) 536% Constraint: Set1 and Set2 are disjoint sets. 537%-- 538disjoint(S1, S2):- 539 ground(S1), ground(S2), !, 540 assure_set(S1,Set1,_), assure_set(S2,Set2,_), 541 set_intersection(Set1,Set2,[]). 542disjoint(S1, S2):- 543 assure_set(S1, Set1, cardinal with [domain:[Glb1:_,_],cardinality:C1]), 544 assure_set(S2, Set2, cardinal with [domain:[Glb2:_,_],cardinality:C2]), 545 set_intersection(Glb1,Glb2,[]), 546 suspend_and_call(poss_without_glb(Set1,C1,Set2,SuspP1), 3,Set2->cardinal:glb, SuspP1), 547 suspend_and_call(poss_without_glb(Set2,C2,Set1,SuspP2), 3,Set1->cardinal:glb, SuspP2), 548 %These poss_without_glb/4 suspensions should have higher priority (lower number) 549 %than the check_special_disjoint/3 demon suspension below. 550 suspend_and_call(check_special_disjoint(Set1, Set2, [SuspP1,SuspP2,SuspC]), 4, 551 [Set1,Set2]->cardinal:bound, SuspC), %lower priority than both poss_without_glb/4 above 552 lub(Set1,Lub1), lub(Set2,Lub2), 553 set_union(Lub1,Lub2, _, 0,U), 554 C1+C2 #<= U. 555 556:- demon poss_without_glb/4. 557poss_without_glb(S1,C1, S2, Susp):- 558 set_info(S1, C1, cardinal with domain:[_:NIn1,Poss1:_]), 559 glb(S2, Glb2), 560 set_without(Poss1, Glb2, NewPoss1, 0,NNewPoss1), 561 NewNMax1 is NIn1+NNewPoss1, 562 set_poss(S1, NewPoss1,NewNMax1), 563 (var(S2) -> true ; kill_suspension(Susp)). 564 565:-demon check_special_disjoint/3. 566check_special_disjoint(S1, S2, Susps):- S1==S2, !, kill_suspensions(Susps), S1=[]. 567check_special_disjoint(S1, S2, Susps):- (nonvar(S1) ; nonvar(S2)), !, kill_suspensions(Susps). 568check_special_disjoint(_,_,_). 569 570 571 572 573 574%-------- 575% contains(+Set1, ?Set2) 576% Constraint: Set1 contains (>=) Set2. 577%-- 578contains(S1, S2):- 579 ground(S1), ground(S2), !, 580 is_list(S1), is_list(S2), 581 \+ (member(X,S2), \+ member(X,S1)). 582contains(S1, S2):- 583 is_my_set(S2), !, 584 assure_set(S1, Set1, cardinal with cardinality:C1), 585 assure_set(S2, Set2, cardinal with cardinality:C2), 586 C1 #>= C2, 587 suspend_and_call(include_elements(Set2,Set1,C1,SuspI), 3, Set2->cardinal:glb, SuspI), 588 %This include_elements/4 suspension should have higher priority (lower number) 589 %than the lub_union/4 demon suspension of the union constraint 590 %and the lub_arg1_diff/4 predicate suspension of set_difference constraint. 591 suspend_and_call(limit_elements(Set2,C2,Set1,C1,SuspE), 3, Set1->cardinal:lub, SuspE), 592 suspend_and_call(check_inclusion(Set2,Set1,[SuspI,SuspE,SuspC]), 4, 593 [Set1,Set2]->cardinal:bound, SuspC). %lower priority than both suspensions above 594contains(S1, S2):- 595 assure_set(S1, Set1, cardinal with domain:[Glb1:_,Poss1:_]), 596 lub(Glb1, Poss1, Lub1), 597 set(S2, [],Lub1, []), 598 contains(Set1, S2). 599 600:- demon include_elements/4. 601include_elements(In, Container,CC, Susp):- 602 domain(Container, CC, [GlbC:NInC,PossC:NMaxC]), 603 glb(In, GlbI), 604 include_elements(_, GlbI, GlbC,PossC, GlbC1, PossC1, NInC,NInC1), 605 set_domain(Container, [GlbC1:NInC1,PossC1:NMaxC]), 606 (var(In) -> true ; kill_suspension(Susp)). 607 608:- demon limit_elements/5. 609limit_elements(In,CIn, Container,CC, Susp):- 610 domain(Container, CC, [GlbC:_,PossC:_]), 611 domain(In, CIn, [_:NInI,PossI:_]), 612 limit_elements(PossI, GlbC,PossC, NewPossI, NInI,NewNMaxI), 613 set_poss(In, NewPossI,NewNMaxI), 614 (var(Container) -> true ; kill_suspension(Susp)). 615 616:- demon check_inclusion/3. 617check_inclusion(In, Container, Susps):- 618 (In==Container ; nonvar(In) ; nonvar(Container)), !, 619 kill_suspensions(Susps). 620check_inclusion(_, _, _). 621 622 623 624%-------- 625% include_elements(?Bound, +Set, +Glb,+Poss, -NewGlb,-NewPoss, +NIn,-NewNIn) 626% 627% Definitely Include elements of Set in set represented by Glb and Poss, 628% These elements must be already in Glb or be removed from Poss to Glb, 629% yielding NewGlb and NewPoss. NIn is Glb's length, NewNIn is NewGlb's length. 630% All sets are ordered lists. 631% Bound just indicates which of Glb or Poss is tried to find the first 632% element of Set. It is there so that in the end of last clause (when we know 633% that it must be searched in Poss) we can call include_elements(poss,... 634% and only the "poss" clauses will be considered, without unnecessary 635% unifications and comparisons (@<). 636%-- 637include_elements(nil, [], Glb,Poss, Glb,Poss, N,N):- !. 638include_elements(glb, [H|T], [H|GlbIn],PossIn, [H|GlbOut],PossOut, Ni,No):- 639 !, include_elements(_, T, GlbIn,PossIn, GlbOut,PossOut, Ni,No). 640include_elements(glb, [H|T], [X|GlbIn],PossIn, [X|GlbOut],PossOut, Ni,No):- 641 X @< H, !, include_elements(_, [H|T], GlbIn,PossIn, GlbOut,PossOut, Ni,No). 642include_elements(poss, [H|T], GlbIn,[HP|PossIn], [H|GlbOut],PossOut, Ni,No):- 643 val(HP,H), !, N1 is Ni+1, 644 include_elements(_, T, GlbIn,PossIn, GlbOut,PossOut, N1,No). 645include_elements(poss, [H|T], GlbIn,[HP|PossIn], GlbOut,[HP|PossOut], Ni,No):- 646 val(HP,ValHP), ValHP @< H, !, 647 include_elements(poss, [H|T], GlbIn,PossIn, GlbOut,PossOut, Ni,No). 648 649 650%-------- 651% limit_elements(+InitialSet, +Set1,+Set2, -FinalSet,+Ni,-No) 652% FinalSet = InitialSet /\ (Set1 \/ Set2) 653% FinalSet is InitialSet without elements that are not present 654% neither in Set1 nor in Set2. Its cardinality is No-Ni. 655% All sets are ordered lists. 656%-- 657limit_elements([], _,_, [],N,N). 658limit_elements([H|T], Glb,Poss, Lo,Ni,No):- 659 val(H,VH), 660 remove(VH, Glb, _, Glb1, Res1), 661 (Res1==true -> N1 is Ni+1, Lo=[H|L], 662 limit_elements(T, Glb1,Poss, L,N1,No) 663 ; remove(H, Poss, _, Poss1, Res2), 664 (Res2==true -> N1 is Ni+1, Lo=[H|L], 665 limit_elements(T, Glb1,Poss1, L,N1,No) 666 ; limit_elements(T, Glb1,Poss1, Lo,Ni,No) 667 ) 668 ). 669 670 671 672 673 674%-------- 675% member_set(?Element, +Set) 676% Constraint: Element E Set. 677%-- 678member_set(X, S):- 679 ground(X), !, 680 assure_set(S, Set, cardinal with domain:[Glb:NIn,Poss:NMax]), 681 remove(X, Glb, _GlbButX, Front, Tail, Result), 682 (Result = true -> true 683 ; remove(X, Poss, NewPoss), 684 Front = NewGlb-Diff, 685 Diff = [X|Tail], 686 NIn1 is NIn+1, 687 set_domain(Set, [NewGlb:NIn1,NewPoss:NMax]) 688 ). 689member_set(X, S):- nonvar(S), S=[Elem], !, X=Elem. 690member_set(X, S):- suspend(member_set(X,S), 3, [X,S]->inst). 691 692 693%-------- 694% not_in_set(?Element, +Set) 695% Constraint: Element is not in Set. 696%-- 697not_in_set(X, S):- 698 ground(X), !, 699 assure_set(S, Set, cardinal with domain:[Glb:_,Poss:NMax]), 700 \+ my_member(X, Glb), 701 (remove(X, Poss, NewPoss) -> NMax1 is NMax-1, set_poss(Set, NewPoss,NMax1) 702 ;true 703 ). 704not_in_set(X, S):- suspend(not_in_set(X,S), 3, X->inst). 705 706 707 708 709 710%-------- 711% my_set_union(?Set1, ?Set2, ?SetUnion) 712% Constraint: SetUnion is the union of Set1 and Set2 (i.e. Set1 U Set2). 713%-- 714my_set_union(Set1, Set2, Set3):- 715 is_my_set(Set3), !, 716 assure_set(Set3, S3, cardinal with cardinality:C3), 717 contains(S3, Set1), 718 contains(S3, Set2), 719 assure_set(Set1, S1, cardinal with cardinality:C1), 720 assure_set(Set2, S2, cardinal with cardinality:C2), 721 (special_union(S1,S2,S3, Goal) -> call(Goal) 722 ;C3 #<= C1+C2, 723 suspend_and_call(lub_union(S1,S2,S3,SuspL), 4, [S1,S2]->cardinal:lub, SuspL), 724 %lub_union/4 demon suspension should have lower priority (higher number) 725 %than contains/2 suspensions, namely the include_elements/4 demon. 726 suspend_and_call(min_card_union(S1,S2,C2,C3,Susp_m1), 5, 727 [S1->cardinal:glb,S2->cardinal:lub], Susp_m1), 728 suspend_and_call(min_card_union(S2,S1,C1,C3,Susp_m2), 5, 729 [S1->cardinal:lub,S2->cardinal:glb], Susp_m2), 730 suspend_and_call(glb_arg_union(S1,S2,C2,S3,Susp_g1), 5, [S1,S3]->inst, Susp_g1), %[S1->cardinal:lub,S3->cardinal:glb] 731 suspend_and_call(glb_arg_union(S2,S1,C1,S3,Susp_g2), 5, [S2,S3]->inst, Susp_g2), %[S2->cardinal:lub,S3->cardinal:glb] 732 suspend_and_call(check_special_union(S1,S2,S3,[SuspC,SuspL,Susp_m1,Susp_m2,Susp_g1,Susp_g2]), 733 2, [S1,S2]->cardinal:bound, SuspC), 734 lub(S1, Glb1,_Poss1, Lub1), 735 lub(S2, Glb2,_Poss2, Lub2), 736 set_intersection(Glb1, Glb2, _, 0,NGI), 737 set_intersection(Lub1, Lub2, _, 0,NLI), 738 C1::DC1, 739 C2::DC2, 740 set_without(Glb1, Lub2, _, 0,N12), 741 set_without(Glb2, Lub1, _, 0,N21), 742 or_card_dom(DC1,DC2, NGI,NLI, N12,N21, [],CDom), 743 C3::CDom 744 ). 745my_set_union(S1, S2, S3):- 746 assure_set(S1, Set1, cardinal with domain:[Glb1:_,Poss1:_]), 747 assure_set(S2, Set2, cardinal with domain:[Glb2:_,Poss2:_]), 748 set_union(Glb1, Glb2, Glb1u2), %(Poss1 \ Glb2) U (Poss2 \ Glb1) = 749 set_without(Poss1, Glb2, Poss3_1), % (Lub1 \ (Glb1 U Glb2)) U 750 set_without(Poss2, Glb1, Poss3_2), % (Lub2 \ (Glb1 U Glb2)) = 751 set_union(Poss3_1, Poss3_2, Poss3), % (Lub1 U Lub2) \ (Glb1 U Glb2) = 752 val_list(Poss3, ValPoss3), 753 set(S3, Glb1u2,ValPoss3, []), % Lub3 \ Glb3 = Poss3 754 my_set_union(Set1, Set2, S3). 755 756 757:-demon check_special_union/4. 758check_special_union(S1,S2,S3, Susps):- 759 special_union(S1,S2,S3, Goal), !, 760 kill_suspensions(Susps), 761 call(Goal). 762check_special_union(_,_,_, _). 763 764special_union(S1,S2,S3, true):- (S1==S3 ; S2==S3), !. 765special_union(S1,S2,S3, S2=S3):- S1==[], !. 766special_union(S1,S2,S3, S1=S3):- S2==[], !. 767special_union(S1,S2,S3, S3=S1):- S1==S2, !. 768special_union(S1,S2,S3, (set_union(S1,S2,U),S3=U)):- nonvar(S1), nonvar(S2), !. 769special_union(S1,S2,S3, S3=S2):- 770 nonvar(S1), glb(S2, Glb2), 771 set_without(S1, Glb2, []), !. % S2 >= S1 772special_union(S1,S2,S3, S3=S1):- 773 nonvar(S2), glb(S1, Glb1), 774 set_without(S2, Glb1, []), !. % S1 >= S2 775 776 777:-demon min_card_union/5. 778min_card_union(S1, S2,C2, C3, Susp):- 779 glb(S1, Glb1), 780 glb(S2,Glb2), poss(S2,Poss2), 781 set_without(Glb1, Glb2, Glb1_Glb2), 782 set_without(Glb1_Glb2, Poss2, _Glb1_U2, 0,NIn3_1), 783 C3 #>= C2+NIn3_1, 784 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 785 786%It is assumed that Glb1 and Glb2 are already included in Glb3, thanks to `>= constraints. 787:-demon lub_union/4. 788lub_union(S1, S2, S3, Susp):- 789 wake, %Force higher priority scheduled suspensions to execute 790 poss(S1, Poss1), 791 poss(S2, Poss2), 792 domain(S3, [_:NIn3,Poss3:_]), 793 limit_elements(Poss3, Poss1,Poss2, NewPoss3,0,NNewPoss3), 794 NewNMax3 is NIn3+NNewPoss3, 795 set_poss(S3, NewPoss3,NewNMax3), 796 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 797 798:-demon glb_arg_union/5. 799glb_arg_union(S1, S2,C2, S3, Susp):- 800 glb_poss(S1, Glb1,Poss1), 801 glb(S3, Glb3), 802 set_without(Glb3, Glb1, Glb3_1), 803 set_without(Glb3_1, Poss1, Glb3_Lub1), 804 include_elements(Glb3_Lub1, S2,C2, _), 805 ((var(S1);var(S3)) -> true ; kill_suspension(Susp)). 806 807 808%-------------- 809%or_card_dom(+DomainCX, +DomainCY, +NGI,+NLI, +NXY,+NYX, +DomainIn,-DomainOut) 810% For the union of sets X and Y, DomainCX is the domain of #X, 811%DomainCY is the domain of #Y, NGI=#(GlbX /\ GlbY), NLI=#(LubX /\ LubY), 812%NXY=#(GlbX\LubY), NYX=#(GlbY\LubX), DomainIn is the list of possible ranges for 813%the domain of #(X\/Y) so far, and DomainOut is the final one. 814%-- 815or_card_dom([],_, _,_, _,_, D,D):- !. 816or_card_dom(DCX,DCY, NGI,NLI, NXY,NYX, Di,Do):- 817 remove_range(DCX, RX, TX), 818 ocd(DCY, RX, NGI,NLI, NXY,NYX, Di,D1), 819 or_card_dom(TX,DCY, NGI,NLI, NXY,NYX, D1,Do). 820 821%-------------- 822%ocd(+DomainCY, +RangeX, +NGI,+NLI, +NXY,+NYX, +DomainIn,-DomainOut) 823% For the union of sets X and Y, DomainCY is the domain of #Y, 824%RangeX is a range from the domain of #X, NGI=#(GlbX /\ GlbY), NLI=#(LubX /\ LubY), 825%NXY=#(GlbX\LubY), NYX=#(GlbY\LubX), DomainIn is the list of possible ranges for 826%the domain of #(X\/Y) so far, and DomainOut is the final one. 827%-- 828ocd([],_, _,_, _,_, D,D):- !. 829ocd(DCY,AX..BX, NGI,NLI, NXY,NYX, Di,Do):- 830 remove_range(DCY, AY..BY, TY), 831 AZ1 is max(AX+NYX,AY+NXY), 832 AZ is max(AZ1,AX+AY-NLI), 833 BZ is BX+BY-NGI, 834 (BZ >= AZ -> D1=[AZ..BZ|Di] ; D1=Di), 835 ocd(TY,AX..BX, NGI,NLI, NXY,NYX, D1,Do). 836 837 838 839 840 841 842%-------- 843% my_set_intersection(?Set1, ?Set2, ?SetIntersection) 844% Constraint: SetIntersection is the intersection of Set1 and Set2 (i.e. Set1/\Set2). 845%-- 846my_set_intersection(Set1, Set2, Set3):- 847 is_my_set(Set3), !, 848 assure_set(Set3, S3, cardinal with cardinality:C3), 849 contains(Set1, S3), 850 contains(Set2, S3), 851 assure_set(Set1, S1, cardinal with cardinality:C1), 852 assure_set(Set2, S2, cardinal with cardinality:C2), 853 suspend_and_call(glb_intersection(S1,S2,S3,C3,SuspG), 4, 854 [S1,S2]->cardinal:glb, SuspG), 855 suspend_and_call(max_card_intersection(S1,C1,S2,C3,SuspM1), 5, 856 [S1->cardinal:glb,S2->cardinal:lub], SuspM1), 857 suspend_and_call(max_card_intersection(S2,C2,S1,C3,SuspM2), 5, 858 [S1->cardinal:lub,S2->cardinal:glb], SuspM2), 859 suspend_and_call(min_card_intersection(S2,S1,S3,SuspMin), 6, 860 [S1,S2]->cardinal:lub, SuspMin), 861 suspend_and_call(lub_arg_intersection(S1,S2,C2,S3,SuspL1), 5, 862 [S1,S3]->inst, SuspL1), %[S1->cardinal:glb,S3->cardinal:lub] 863 suspend_and_call(lub_arg_intersection(S2,S1,C1,S3,SuspL2), 5, 864 [S2,S3]->inst, SuspL2), %[S2->cardinal:glb,S3->cardinal:lub] 865 suspend_and_call(check_special_intersection(S1,S2,S3,[SuspC,SuspG,SuspM1,SuspM2,SuspMin,SuspL1,SuspL2]), 866 2, [S1,S2]->cardinal:bound, SuspC), 867 lub(S1, Glb1,_Poss1, Lub1), 868 lub(S2, Glb2,_Poss2, Lub2), 869 set_union(Lub1, Lub2, _, 0,NU), 870 C1::DC1, 871 C2::DC2, 872 set_without(Glb1, Lub2, _, 0,N12), 873 set_without(Glb2, Lub1, _, 0,N21), 874 and_card_dom(DC1,DC2, NU, N12,N21, [],CDom), 875 C3::CDom. 876my_set_intersection(S1, S2, S3):- 877 assure_set(S1, Set1, cardinal with domain:[Glb1:_,Poss1:_]), 878 assure_set(S2, Set2, cardinal with domain:[Glb2:_,Poss2:_]), 879 set_intersection(Glb1, Glb2, Glb3), 880 lub(Glb1, Poss1, Lub1), 881 lub(Glb2, Poss2, Lub2), 882 set_intersection(Lub1, Lub2, Lub3), 883 set_without(Lub3, Glb3, Poss3), 884 set(S3, Glb3,Poss3, []), %set(S3, Glb3,Poss3, _,_), 885 my_set_intersection(Set1, Set2, S3). 886 887 888:-demon check_special_intersection/4. 889check_special_intersection(S1,S2,S3, Susps):- (S1==S3 ; S2==S3), !, kill_suspensions(Susps). 890check_special_intersection(S1,S2,S3, Susps):- (S1==[] ; S2==[]), !, kill_suspensions(Susps), S3=[]. 891check_special_intersection(S1,S2,S3, Susps):- S1==S2, !, kill_suspensions(Susps), S3=S1. 892check_special_intersection(S1,S2,S3, Susps):- 893 nonvar(S1), nonvar(S2), !, kill_suspensions(Susps), set_intersection(S1,S2,I), S3=I. 894check_special_intersection(S1,S2,S3, Susps):- 895 nonvar(S1), glb(S2, Glb2), poss(S2, Poss2), 896 verify_inclusion(Glb2, S1,[], S1_Glb2), % 897 set_without(Poss2, S1_Glb2, []), !, % S1 >= S2 898 kill_suspensions(Susps), S3=S2. 899check_special_intersection(S1,S2,S3, Susps):- 900 nonvar(S2), glb(S1, Glb1), poss(S1, Poss1), 901 verify_inclusion(Glb1, S2,[], S2_Glb1), % 902 set_without(Poss1, S2_Glb1, []), !, % S2 >= S1 903 kill_suspensions(Susps), S3=S1. 904check_special_intersection(_,_,_, _). 905 906 907:-demon max_card_intersection/5. 908max_card_intersection(S1,C1, S2, C3, Susp):- 909 glb(S1, Glb1), 910 glb(S2, Glb2), poss(S2, Poss2), 911 set_without(Glb1, Glb2, Glb1_Glb2), 912 set_without(Glb1_Glb2, Poss2, _Glb1_U2, 0,NIn1_2), 913 C3 #<= C1-NIn1_2, 914 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 915 916:-demon min_card_intersection/4. 917min_card_intersection(S1, S2, S3, Susp):- 918 set_info(S1, cardinal with [domain:[_,_:NMax1],cardinality:C1]), 919 set_info(S2, cardinal with [domain:[_,_:NMax2],cardinality:C2]), 920 set_info(S3, cardinal with [domain:[_,_:NMax3],cardinality:C3]), 921 C3 #>= C1+C2-(NMax1+NMax2-NMax3), 922 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 923 924:-demon glb_intersection/5. 925glb_intersection(S1, S2, S3,C3, Susp):- 926 glb(S1, Glb1), 927 glb(S2, Glb2), 928 set_intersection(Glb1, Glb2, Glb1i2), 929 include_elements(Glb1i2, S3,C3, _), 930 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 931 932:-demon lub_arg_intersection/5. 933lub_arg_intersection(S1, S2,C2, S3, Susp):- 934 glb(S1, Glb1), 935 glb(S3, Glb3), poss(S3, Poss3), 936 set_without(Glb1, Glb3, Glb1_3), 937 set_without(Glb1_3, Poss3, Glb1_Lub3), 938 exclude_elements(Glb1_Lub3, S2,C2), 939 ((var(S1);var(S3)) -> true ; kill_suspension(Susp)). 940 941exclude_elements(Elements, Set,CS):- 942 set_info(Set, CS, cardinal with domain:[Glb:NIn,Poss:_]), 943 set_intersection(Elements, Glb, []), 944 set_without(Poss, Elements, NewPoss, 0,NNewPoss), 945 NewNMax is NIn+NNewPoss, 946 set_poss(Set, NewPoss,NewNMax). 947 948 949%-------------- 950%and_card_dom(+DomainCX, +DomainCY, +NU, +NXY,+NYX, +DomainIn,-DomainOut) 951% For the intersection of sets X and Y, DomainCX is the domain of #X, 952%DomainCY is the domain of #Y, NU=#(LubX \/ LubY), NXY=#(GlbX\LubY), 953%NYX=#(GlbY\LubX), DomainIn is the list of possible ranges for the domain 954%of #(X/\Y) so far, and DomainOut is the final one. 955%-- 956and_card_dom([],_, _, _,_, D,D):- !. 957and_card_dom(DCX,DCY, NU, NXY,NYX, Di,Do):- 958 remove_range(DCX, RX, TX), 959 acd(DCY, RX, NU, NXY,NYX, Di,D1), 960 and_card_dom(TX,DCY, NU, NXY,NYX, D1,Do). 961 962%-------------- 963%acd(+DomainCY, +RangeX, +NU, +NXY,+NYX, +DomainIn,-DomainOut) 964% For the intersection of sets X and Y, DomainCY is the domain of #Y, 965%RangeX is a range from the domain of #X, NU=#(LubX \/ LubY), NXY=#(GlbX\LubY), 966%NYX=#(GlbY\LubX), DomainIn is the list of possible ranges for the domain 967%of #(X/\Y) so far, and DomainOut is the final one. 968%-- 969acd([],_, _, _,_, D,D):- !. 970acd(DCY,AX..BX, NU, NXY,NYX, Di,Do):- 971 remove_range(DCY, AY..BY, TY), 972 AZ is AX+AY-NU, 973 BZ is min(BX-NXY,BY-NYX), 974 (BZ >= AZ -> D1=[AZ..BZ|Di] ; D1=Di), 975 acd(TY,AX..BX, NU, NXY,NYX, D1,Do). 976 977%-------------- 978%remove_range(+Domain, -Range, -Rest) 979% Remove a Range from a cardinality Domain. Single and consecutive elements 980%are converted in ranges (A..B). Rest is Domain without Range. 981%-- 982remove_range([A..B|T], A..B, T):- !. 983remove_range([R], R..R, []):- !. 984remove_range([H,M..N|T], H..H, [M..N|T]):- !. 985remove_range([A,B|T], A..B, T):- A =:= B-1, !. 986remove_range([A,B|T], A..A, [B|T]). 987 988 989 990 991 992 993 994%-------- 995% my_set_difference(?Set1, ?Set2, ?SetDifference) 996% Constraint: SetDifference is the difference between Set1 and Set2 (i.e. Set1\Set2). 997%-- 998my_set_difference(Set1, Set2, Set3):- 999 is_my_set(Set3), !, 1000 assure_set(Set3, S3, cardinal with cardinality:C3), 1001 contains(Set1, S3), 1002 disjoint(Set2, S3), 1003 assure_set(Set1, S1, cardinal with cardinality:C1), 1004 assure_set(Set2, S2, cardinal with cardinality:C2), 1005 C3 #>= C1-C2, 1006 suspend_and_call(glb_difference(S1,S2,S3,C3,SuspG), 4, 1007 [S1->cardinal:glb,S2->cardinal:lub], SuspG), 1008 suspend_and_call(glb_arg2_diff(S1,S2,C2,S3,SuspG2), 7, 1009 [S1->cardinal:glb,S3->cardinal:lub], SuspG2), 1010 suspend_and_call(max_card_difference_glb(S1,C1,S2,C3,SuspDG), 5, 1011 [[S1,S2]->cardinal:glb], SuspDG), %,C1->fd:max,C3->fd:min 1012 suspend_and_call(max_card_difference_lub(S1,S2,C3,SuspDL), 7, 1013 [[S1,S2]->cardinal:lub], SuspDL), %,[C2,C3]->fd:min 1014 suspend_and_call(check_special_difference(S1,S2,S3,[SuspC,SuspG,SuspG2,SuspDG,SuspDL,SuspL1]), 1015 2, [S1,S2]->cardinal:bound, SuspC), 1016 (var(S3) -> suspend(lub_arg1_diff(S1,C1,S2,S3), 5, [S3->inst], SuspL1) ; true), 1017 %Priority must be lower (higher number) than suspension of contains(S1,S3) (which inserts Glb3 in Glb1) 1018 lub_arg1_diff(S1,C1,S2,S3), 1019 lub(S1, Glb1,_Poss1, Lub1), 1020 lub(S2, Glb2,_Poss2, Lub2), 1021 set_union(Lub1, Lub2, _, 0,NU), 1022 C1::DC1, 1023 C2::DC2, 1024 set_intersection(Glb1, Glb2, _, 0,NGI), 1025 set_intersection(Lub1, Lub1, _, 0,NLI), 1026 diff_card_dom(DC1,DC2, NU, NGI,NLI, [],CDom), 1027 C3::CDom. 1028my_set_difference(S1, S2, S3):- 1029 assure_set(S1, Set1, cardinal with domain:[Glb1:_,Poss1:_]), 1030 assure_set(S2, Set2, cardinal with domain:[Glb2:_,Poss2:_]), 1031 lub(Glb1, Poss1, Lub1), 1032 lub(Glb2, Poss2, Lub2), 1033 set_without(Glb1, Lub2, Glb3), 1034 set_without(Lub1, Glb2, Lub3), 1035 set_without(Lub3, Glb3, Poss3), 1036 set(S3, Glb3,Poss3, []), 1037 my_set_difference(Set1, Set2, S3). 1038 1039:-demon check_special_difference/4. 1040check_special_difference(S1,_S,S3, Susps):- S1==[], !, kill_suspensions(Susps), S3=[]. 1041check_special_difference(S1,S2,S3, Susps):- S2==[], !, kill_suspensions(Susps), S1=S3. 1042check_special_difference(S1,S2,S3, Susps):- S1==S2, !, kill_suspensions(Susps), S3=[]. 1043check_special_difference(S1,_S,S3, Susps):- S1==S3, !, kill_suspensions(Susps). 1044check_special_difference(S1,S2,S3, Susps):- 1045 nonvar(S1), nonvar(S2), !, kill_suspensions(Susps), set_without(S1,S2,W), S3=W. 1046check_special_difference(S1,S2,S3, Susps):- 1047 nonvar(S1), glb_poss(S2, Glb2, Poss2), 1048 set_intersection(Glb2, S1, []), 1049 set_intersection(Poss2, S1, []), !, % disjoint(S1,S2) 1050 kill_suspensions(Susps), S3=S1. 1051check_special_difference(S1,S2,S3, Susps):- 1052 nonvar(S2), glb_poss(S1, Glb1, Poss1), 1053 set_intersection(Glb1, S2, []), 1054 set_intersection(Poss1, S2, []), !, % disjoint(S1,S2) 1055 kill_suspensions(Susps), S3=S1. 1056check_special_difference(_,_,_, _). 1057 1058:-demon glb_difference/5. 1059glb_difference(S1, S2, S3,C3, Susp):- 1060 glb(S1, Glb1), 1061 glb_poss(S2, Glb2, Poss2), 1062 set_without(Glb1, Glb2, Glb1_2), 1063 set_without(Glb1_2, Poss2, Glb1_Lub2), 1064 include_elements(Glb1_Lub2, S3,C3, _), 1065 ((var(S1);var(S2)) -> true ; kill_suspension(Susp)). 1066 1067:-demon glb_arg2_diff/5. 1068glb_arg2_diff(S1, S2,C2, S3, Susp):- 1069 glb(S1, Glb1), 1070 glb_poss(S3, Glb3, Poss3), 1071 set_without(Glb1, Glb3, Glb1_3), 1072 set_without(Glb1_3, Poss3, Glb1_Lub3), 1073 include_elements(Glb1_Lub3, S2,C2, _), 1074 ((var(S1);var(S3)) -> true ; kill_suspension(Susp)). 1075 1076:-demon max_card_difference_glb/5. 1077max_card_difference_glb(S1,C1, S2, C3, Susp):- 1078 glb(S1, Glb1), 1079 glb(S2, Glb2), 1080 set_intersection(Glb1, Glb2, _Glb1i2, 0,NIn1i2), 1081 C3 #<= C1-NIn1i2, 1082 ((var(S1);var(S2);var(C1);var(C3)) -> true ; kill_suspension(Susp)). 1083 1084:-demon max_card_difference_lub/4. 1085max_card_difference_lub(S1, S2, C3, Susp):- 1086 lub(S1, Lub1), 1087 lub(S2, Lub2), 1088 set_union(Lub1, Lub2, _, 0,NU), 1089 C3 #<= NU-C2, 1090 ((var(S1);var(S2);var(C2);var(C3)) -> true ; kill_suspension(Susp)). 1091 1092%It is assumed that Glb3 is already included in Glb1, thanks to the `>= constraint. 1093lub_arg1_diff(S1,C1, S2, S3):- 1094 wake, %Force higher priority scheduled suspensions to execute 1095 domain(S1, C1, [_:NIn1,Poss1:_]), 1096 poss(S3, Poss3), 1097 lub(S2, Lub2), 1098 limit_elements(Poss1, Lub2,Poss3, NewPoss1,NIn1,NewNMax1), 1099 set_poss(S1, NewPoss1,NewNMax1). 1100 1101 1102 1103%-------------- 1104%diff_card_dom(+DomainCX, +DomainCY, +NU, +NGI,+NLI, +DomainIn,-DomainOut) 1105% For the difference X\Y of sets X and Y, DomainCX is the domain of #X, 1106%DomainCY is the domain of #Y, NU=#(LubX \/ LubY), NGI=#(GlbX /\ GlbY), 1107%NLI=#(LubX /\ LubY), DomainIn is the list of possible ranges for 1108%the domain of #(X\Y) so far, and DomainOut is the final one. 1109%-- 1110diff_card_dom([],_, _, _,_, D,D):- !. 1111diff_card_dom(DCX,DCY, NU, NGI,NLI, Di,Do):- 1112 remove_range(DCX, RX, TX), 1113 dcd(DCY, RX, NU, NGI,NLI, Di,D1), 1114 diff_card_dom(TX,DCY, NU, NGI,NLI, D1,Do). 1115 1116%-------------- 1117%dcd(+DomainCY, +RangeX, +NU, +NGI,+NLI, +DomainIn,-DomainOut) 1118% For the difference X\Y of sets X and Y, DomainCY is the domain of #Y, 1119%RangeX is a range from the domain of #X, NU=#(LubX \/ LubY), NGI=#(GlbX /\ GlbY), 1120%NLI=#(LubX /\ LubY), DomainIn is the list of possible ranges for the domain of 1121%#(X\Y) so far, and DomainOut is the final one. 1122%-- 1123dcd([],_, _, _,_, D,D):- !. 1124dcd(DCY,AX..BX, NU, NGI,NLI, Di,Do):- 1125 remove_range(DCY, AY..BY, TY), 1126 AZ is max(AX-BY,AX-NLI), 1127 BZ is min(BX-NGI,NU-AY), 1128 (BZ >= AZ -> D1=[AZ..BZ|Di] ; D1=Di), 1129 dcd(TY,AX..BX, NU, NGI,NLI, D1,Do). 1130 1131 1132 1133 1134%-------------- 1135%complement(+Set, +Complement) 1136% Constraint: Complement is the complementary set of Set. 1137% (The universe is taken as the union of their LUBs.) 1138%-- 1139complement(X, NotX):- 1140 (is_my_set(X) -> true ; X=[]), 1141 (is_my_set(NotX) -> true ; NotX=[]), 1142 assure_set(X, SetX, cardinal with domain:[GlbX:_,PossX:_]), 1143 lub(GlbX, PossX, LubX), 1144 assure_set(NotX, SetNX, cardinal with domain:[GlbNX:_,PossNX:_]), 1145 lub(GlbNX, PossNX, LubNX), 1146 set_union(LubX, LubNX, Universe), 1147 complement_sets(SetX, Universe, SetNX). 1148 1149 1150%-------------- 1151%complement(?Set, +Universe, ?Complement) 1152% Constraint: Complement is the complementary set of Set (with respect to Universe.) 1153%-- 1154complement(X, Universe, NotX):- 1155 \+ is_my_set(NotX), !, 1156 (is_my_set(X) -> true ; set(X, [],Universe, [])), 1157 assure_set(X, SetX, cardinal with domain:[GlbX:_,PossX:_]), 1158 lub(GlbX, PossX, LubX), 1159 set_without(Universe, LubX, GlbNotX), 1160 set_without(Universe, GlbX, LubNotX), 1161 set_without(LubNotX, GlbNotX, PossNotX), 1162 set(NotX, GlbNotX,PossNotX, []), 1163 complement_sets(SetX, Universe, NotX). 1164complement(X, Universe, NotX):- 1165 \+ is_my_set(X), !, 1166 assure_set(NotX, SetNX, cardinal with domain:[GlbNX:_,PossNX:_]), 1167 lub(GlbNX, PossNX, LubNX), 1168 set_without(Universe, LubNX, GlbX), 1169 set_without(Universe, GlbNX, LubX), 1170 set_without(LubX, GlbX, PossX), 1171 set(X, GlbX,PossX, []), 1172 complement_sets(X, Universe, SetNX). 1173complement(X, Universe, NotX):- 1174 assure_set(X, SetX, _), 1175 assure_set(NotX, SetNX, _), 1176 complement_sets(SetX, Universe, SetNX). 1177 1178%-------------- 1179%complement_sets(?Set, +Universe, ?Complement) 1180% Set and Complement are assured sets. 1181%-- 1182complement_sets(X, U, N):- 1183 check_special_complement(X,U,N), 1184 cardinality(X, CX), 1185 cardinality(N, CN), 1186 length(U, CU), 1187 CN #= CU-CX, 1188 CN::DCN, 1189 rev_dom(DCN, CU, [],RDCN), 1190 CX::RDCN, 1191 CX::NewCX, 1192 rev_dom(NewCX, CU, [],RDCX), 1193 CN::RDCX, 1194 domain(X, CX, [GlbX:NInX,PossX:_]), 1195 remove_set(GlbX, U, U1-[]), 1196 domain(N, CN, [GlbN:NInN,PossN:_]), 1197 remove_set(GlbN, U1, U2-[]), 1198 set_intersection(PossX, U2, PossXU, 0,NPX), 1199 NMaxX is NInX+NPX, 1200 set_poss(X, PossXU, NMaxX), 1201 set_intersection(PossN, U2, PossNU, 0,NPN), 1202 NMaxN is NInN+NPN, 1203 set_poss(N, PossNU, NMaxN), 1204 complement_constraint(X, N, U2). 1205 1206 1207check_special_complement(X,U,N):- 1208 (X==N -> U=[] 1209 ;var(X) -> suspend(check_special_complement(X,U,N), 4, X->cardinal:bound) 1210 ;var(N) -> suspend(check_special_complement(X,U,N), 4, N->cardinal:bound) 1211 ;true 1212 ). 1213 1214complement_constraint(X, N, U):- 1215 glb_poss(X, GlbXnb, PossXnb), 1216 glb_poss(N, GlbNnb, PossNnb), 1217 not_bounds(U, GlbXnb,PossXnb, GlbNnb,PossNnb, NewU, 1218 NewGlbX-[],NewPossX-[], NewGlbN-[],NewPossN-[]), 1219 length(NewGlbX, NGX), length(NewPossX, NPX), 1220 NMaxX is NGX+NPX, 1221 set_domain(X, [NewGlbX:NGX,NewPossX:NMaxX]), 1222 length(NewGlbN, NGN), length(NewPossN, NPN), 1223 NMaxN is NGN+NPN, 1224 set_domain(N, [NewGlbN:NGN,NewPossN:NMaxN]), 1225 (var(X) -> suspend(complement_constraint(X,N,NewU), 2, [X,N]->cardinal:bounded) 1226 ;true 1227 ). 1228 1229%-------------- 1230%remove_set(+Glb, +U, -DifU) 1231% Glb must be contained in U. DifU is the list difference for U\Glb. 1232%-- 1233remove_set([], U, U-[]). 1234remove_set([H|T], U, Ui-DU):- 1235 remove(H, U, _, Ui-U1,TU, true), 1236 remove_set(T, TU, U1-DU). 1237 1238%-------------- 1239%not_bounds(+U, +Glb1,+Glb2, +Poss1,+Poss2, -NewU, 1240% -NewGlb1DL,-NewPoss1DL, -NewGlb2DL,-NewPoss2DL) 1241% For the 'not' constraint between Set1::Glb1+Poss1 and Set2::Glb2+Poss2, 1242% U is the initial universe possibly already without some elements of Glb1 and Glb2. 1243% Each element of U must belong to Set1 or Set2. 1244% NewU contains the elements of U still possible in both sets. 1245% The new domains (Glb+Poss) for Set1 and Set2 are given in difference lists in 1246% NewGlb1DL,NewPoss1DL, NewGlb2DL, and NewPoss2DL. 1247%-- 1248not_bounds([], Glb1,Poss1, Glb2,Poss2, [], Glb1-[],Poss1-[], Glb2-[],Poss2-[]). 1249not_bounds([H|T], Glb1,Poss1, Glb2,Poss2, Uo, G1-DG1,P1-DP1, G2-DG2,P2-DP2):- 1250 remove(H, Glb1, _, G1-DG1a, TGlb1, ResG1), 1251 remove(H, Glb2, _, G2-DG2a, TGlb2, ResG2), 1252 remove(H, Poss1, _, P1-DP1a, TPoss1, ResP1), 1253 remove(H, Poss2, _, P2-DP2a, TPoss2, ResP2), 1254 (ResG1==true -> ResG2==fail, P1a=DP1a, P2a=DP2a, [H|G1a]=DG1a, G2a=DG2a, Uo=UT %%% H already in Set1 1255 ;ResG2==true -> ResG1==fail, P1a=DP1a, P2a=DP2a, G1a=DG1a, [H|G2a]=DG2a, Uo=UT %%% H already in Set2 1256 ;ResP1==true, ResP2==true -> [H|P1a]=DP1a, [H|P2a]=DP2a, G1a=DG1a, G2a=DG2a, Uo=[H|UT] %%% H possible in both 1257 ;ResP1==true -> P1a=DP1a, P2a=DP2a, [H|G1a]=DG1a, G2a=DG2a, Uo=UT %%% only possible in Set1 1258 ;ResP2==true -> P1a=DP1a, P2a=DP2a, G1a=DG1a, [H|G2a]=DG2a, Uo=UT %%% only possible in Set2 1259 ;fail %%% impossible 1260 ), not_bounds(T, TGlb1,TPoss1, TGlb2,TPoss2, UT, G1a-DG1,P1a-DP1, G2a-DG2,P2a-DP2). 1261